\begin{frame}
  \small
  
  \begin{block}{Knuth--Bendix Completion Procedure (Simple Version)}
  \vspace{-2ex}
  \mbox{} \hfill
  \smash{\raisebox{-15ex}{\href{http://www-cs-faculty.stanford.edu/~uno/}%
  {\includegraphics[height=12ex]{../graphics/knuth-extra}}}} \qquad
  \begin{tabbing}
  \emph{input} \qquad \= ES $\EE$ and reduction order $>$ \\
  \emph{output} \> \alert{complete TRS $\RR$ such that
  $\xleftrightarrow[\EE]{*} ~=~ \xleftrightarrow[\RR]{*}$} \\[2ex]
  $\RR := \varnothing$ \quad $C := \EE$ \\[.2ex]
  \structure{while} $C \neq \varnothing$ \structure{do} \\[.2ex]
  \qquad \= choose $s \approx t \in C$ \quad
  $C := C \setminus \{ s \approx t \}$ \\[.2ex]
  \> compute $\RR$-normal forms \alert{$s'$} and \alert{$t'$} of $s$
  and $t$ \\[.2ex]
  \> \structure{if} $s' \neq t'$ \structure{then} \\[.2ex]
  \> \qquad \= \structure{if} $s' > t'$ \structure{then} \\[.2ex]
  \> \> \qquad \= $\alert{\alpha} := s'$ \quad $\alert{\beta} := t'$
  \\[.2ex]
  \> \> \structure{else if} $t' > s'$ \structure{then} \\[.2ex]
  \> \> \> $\alert{\alpha} := t'$ \quad $\alert{\beta} := s'$ \\[.2ex]
  \> \> \structure{else} \\
  \> \> \> \alert{\emph{failure}} \quad\quad\textcolor{gray}{(try another reduction order $>$)}\\[.2ex]
  \> \> $\RR := \RR \cup \{ \alert{\alpha} \to \alert{\beta} \}$
  \\[.2ex]
  \> \> $C := C \cup \{ e \in \CP(\RR) \mid
  \text{\alert{$\alpha \to \beta$} was used to generate $e$} \}$
  \end{tabbing}
  \end{block}
\end{frame}