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