\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}