\begin{frame} \small \begin{examples}[Non-Confluence] \smallskip \begin{itemize} \item<2-> no confluence because of critical pairs \onslide<3-> \GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l} \makebox[15mm][r]{\m{a}} & \to & \m{b} \\ [.5ex] \m{a} & \to & \makebox[15mm][l]{\m{c}} \end{array} \qquad \onslide<4->{\m{b} \from \m{a} \to \m{c}}$} \item<5-> no critical pairs but no confluence (Klop 1978) \onslide<5-> \GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l} \makebox[15mm][r]{$\m{f}(\alert<9>{x},\alert<9>{x})$} & \to & \m{a} \\[.5ex] \m{g}(x) & \to & \makebox[15mm][l]{$\m{f}(x,\m{g}(x))$} \\[.5ex] \m{c} & \to & \m{g}(\m{c}) \end{array} \qquad \onslide<6->{ \begin{array}[t]{@{}l} \m{c} \to \m{g}(\m{c}) \to \m{f}(\m{c},\m{g}(\m{c})) \to \m{f}(\m{g}(\m{c}),\m{g}(\m{c})) \to \m{a} \\[.5ex] \m{a} \FromP{*} \m{c} \to \m{g}(\m{c}) \to^* \m{g}(\m{a}) \end{array} }$} \item<7-> no critical pairs but no confluence (Huet 1980) \GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l} \makebox[15mm][r]{$\m{f}(\alert<9>{x},\alert<9>{x})$} & \to & \m{a} \\[.5ex] \m{f}(\alert<9>{x},\m{g}(\alert<9>{x})) & \to & \makebox[15mm][l]{$\m{b}$} \\[.5ex] \m{c} & \to & \m{g}(\m{c}) \end{array} \qquad \onslide<8->{\m{a} \from \m{f(c,c)} \to \m{f(c,g(c))} \to \m{b}}$} \end{itemize} \end{examples} \end{frame}