\begin{frame}[t]
  \small
  
  \vspace{-1ex}
  
  \begin{block}{Three Possibilities}
  \smallskip
  Knuth-Bendix completion procedure may
  \begin{enumerate}
  \addtocounter{enumi}{2}
  \item~
  not terminate \qquad (divergence)
  \smallskip
  \end{enumerate}
  \end{block}
  
  %AM 30.06 DONE add example
  
  \begin{example}<2->
  \begin{itemize}
  \item
  rewrite rules
  \vspace{-1ex}
  \GREEN{\begin{xalignat*}{2}
  \m{f}(\m{g}(x)) &\to \m{g}(\m{h}(x)) &
  \onslide<5->{\m{g}(\m{h}(\m{a}))} &\onslide<5->{\to \m{f}(\m{b})}
  \\
  \m{g}(\m{a}) &\to \m{b} &
  \onslide<7->{\m{g}(\m{h}(\m{h}(\m{a})))}
  &\onslide<7->{\to \m{f}(\m{f}(\m{b}))}
  \\
  &&
  \hspace{1cm}\onslide<9->{\m{g}(\m{h}(\m{h}(\m{h}(\m{a}))))}
  &\onslide<9->{\to \m{f}(\m{f}(\m{f}(\m{b})))}
  \\
  &&&\onslide<9->{\cdots}
  \end{xalignat*}}
  \vspace{-9ex}
  \item<3->
  LPO with precedence $\mG{a} > \mG{f} > \mG{g} > \mG{h} > \mG{b}$
  \item<4->
  critical pair\onslide<6->{s}
  \vspace{-1ex}
  \GREEN{\begin{align*}
  \m{f}(\m{b}) &\cp \m{g}(\m{h}(\m{a}))
  \\
  \onslide<6->{\m{f}(\m{f}(\m{b}))}
  &\onslide<6->{\cp \m{g}(\m{h}(\m{h}(\m{a})))}
  \\
  \onslide<8->{\m{f}(\m{f}(\m{f}(\m{b})))}
  &\onslide<8->{\cp \m{g}(\m{h}(\m{h}(\m{h}(\m{a}))))}
  \end{align*}}
  \vspace{-4ex}
  \end{itemize}
  \end{example}
\end{frame}