\begin{frame} \small \begin{definition}[Matching Problem] \smallskip \begin{tabular}{ll} instance: & terms $s$, $t$ \\[.5ex] question: & $\exists$ subsitution $\sigma\colon ~ s\sigma = t$ ? \end{tabular} \end{definition} \bigskip \begin{block}{Matching Algorithm} \smallskip \begin{enumerate} \item~ start with $\{ s \mapsto t \}$ \item<2->~ repeatedly apply following tranformation rules \begin{alignat*}{2} \{ f(\seq{s}) \mapsto f(\seq{t}) \} \cup S &~\Rightarrow~ \makebox[5mm][l]{$\{ s_1 \mapsto t_1, \dots, s_n \mapsto t_n \} \cup S$} \\[1ex] \onslide<3->{\{ f(\seq{s}) \mapsto g(\seq{t}) \} \cup S} &\onslide<3->{~\Rightarrow~ \bot} &&\onslide<3->{\text{if $f \neq g$}} \\[1ex] \onslide<4->{\{ f(\seq{s}) \mapsto x \} \cup S} &\onslide<4->{~\Rightarrow~ \bot} \\[1ex] \onslide<5->{\{ x \mapsto t \} \cup S} &\onslide<5->{~\Rightarrow~ \bot} &&\onslide<5->{\text{if $S$ contains $x \mapsto t'$ with $t \neq t'$}} \end{alignat*} \vspace{-3ex} \end{enumerate} \end{block} \end{frame}