71/73
\begin{frame}
  \small

  \begin{example}
  We determine the most general common instance of
  \begin{align*}
    s &= f(s(x),y) & t &= f(x,s(0))
  \end{align*}
  \vspace{-3ex}
  \begin{itemize}
  \pause
    \item we rename the variables in $t$ with $\gamma = \{x \mapsto z\}$
    \begin{align*}
      t' = t\gamma = f(z,s(0))
    \end{align*}
  \vspace{-3ex}
  \pause
    \item the mgu of $s$ and $t'$ is 
      \begin{align*}
        \sigma = \{x \mapsto x,\; y \mapsto s(0),\; z \mapsto s(x)\}
      \end{align*}
  \end{itemize}
  \pause
  Hence the mgci of $s$ and $t$ is 
  \begin{align*}
    f(s(x),s(0))
  \end{align*}
  \pause  
  That is, $s\sigma = t(\gamma\sigma)$, or:
  \begin{align*}
    s[x \mapsto x,\;y \mapsto s(x)] = t[x \mapsto s(x)]
  \end{align*}
  \end{example}
\end{frame}