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