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