121/210
\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/}%
\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}