128/205
\begin{frame}[t]
  \small
  
  \vspace{-1ex}
  
  \begin{block}{Three Possibilities}
  \smallskip
  Knuth-Bendix completion procedure may
  \begin{enumerate}
  \addtocounter{enumi}{1}
  \item~
  terminate with failure \strut
  \smallskip
  \end{enumerate}
  \end{block}
  
  \smallskip
  
  \begin{example}<2->
  \begin{itemize}
  \item
  rewrite rules
  \GREEN{\begin{xalignat*}{2}
  \m{f}(x,y) &\to \m{g}(x) &
  \m{f}(x,y) &\to \m{h}(y)
  \end{xalignat*}}
  \vspace{-3ex}
  \item<3->
  two critical pairs
  \[
  \GREEN{\m{g}(x) \cp \m{h}(y)}
  \qquad\qquad
  \GREEN{\m{h}(y) \cp \m{g}(x)}
  \]
  \item<4->
  no orientation possible \quad$\Longrightarrow$\quad failure
  \smallskip
  \end{itemize}
  \end{example}
\end{frame}