\begin{frame} \frametitle{Termination, Example 3} \begin{example} \vspace{-1em} \begin{align*} {\rm f}({\rm g}(x)) \to {\rm g}({\rm g}({\rm f}({\rm f}(x)))) \end{align*} \vspace{-1em} \pause Looks terminating: \begin{itemize} \item ${\rm f}$'s move to the right \item ${\rm g}$'s move to the left \end{itemize} \vspace{.5em} \pause But we have an infinite rewrite sequence: \vspace{-.5em} \begin{align*} &{\rm \alert{f}}({\rm \alert{g}}({\rm g}(x)))\\ \to\ &{\rm g}({\rm g}({\rm f}({\rm \alert{f}}({\rm \alert{g}}(x)))))\\ \to\ &{\rm g}({\rm g}({\rm \emph{f}}({\rm \emph{g}}({\rm \emph{g}}({\rm f}({\rm f}(x)))))))\\ \to\ &\ldots \end{align*} \vspace{-1.5em} \pause We need proofs of termination! \smallskip \end{example} \end{frame}