49/145
\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->{\m{a} \FromP{*} \m{c} \to \m{g}(\m{c}) \to^* \m{g}(\m{a})}$}

\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}