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