13/76
\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}