\begin{frame} \small \begin{theorem} \begin{itemize}[<+->] \item there are no infinite derivations \[ \makebox[6cm][l]{$s \approx t \Rightarrow_{\sigma_1} E_1 \Rightarrow_{\sigma_2} E_2 \Rightarrow_{\sigma_3} \cdots$} \] \item if $s$ and $t$ are unifiable then for every maximal derivation \[ \makebox[6cm][l]{$s \approx t \Rightarrow_{\alert<4>{\sigma_1}} E_1 \Rightarrow_{\alert<4>{\sigma_2}} E_2 \Rightarrow_{\alert<4>{\sigma_3}} \cdots \Rightarrow_{\alert<4>{\sigma_n}} \alert<3>{E_n}$} \] \vspace{-5ex} \begin{itemize} \item $\alert<3>{E_n = \Box}$ \medskip \item<4-> $\alert<4>{\sigma_1\sigma_2\sigma_3 \cdots \sigma_n}$ is mgu of $s$ and $t$ \smallskip \end{itemize} \end{itemize} \end{theorem} \bigskip \begin{block}<5->{Optional Failure Rules} \smallskip \[ \frac{E_1,\:f(\seq{s}) \approx g(\seq[m]{t}),\:E_2}{\bot} \qquad \underset{\raisebox{-1ex}{\small if $x \ne t$ and $x \in \Var(t)$}}{ \frac{E_1,\:x \approx t,\:E_2}{\bot} \quad \frac{E_1,\:t \approx x,\:E_2}{\bot} } \] \end{block} \end{frame}