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