\begin{frame}
  \frametitle{Example}
  
  \begin{example}
  \vspace{-1em}
  \begin{align*}
  {\rm f}({\rm f}(x)) &\to {\rm g}(x) &
  {\rm f}({\rm g}(x)) &\to {\rm g}({\rm f}(x))
  \end{align*}
  \vspace{-1.5em}
  \pause
  
  We use the following interpretation:
  \vspace{-.5em}
  \begin{align*}
    \interpret{{\rm f}}(x) &= x+1 & \interpret{{\rm g}}(x) &= x+1
  \end{align*}
  \vspace{-1.5em}
  \pause
  
  We get the following interpretation of rules:
  \vspace{-.5em}
  \begin{align*}
      \interpret{{\rm f}({\rm f}(x)),\alpha}
      = \alpha(x)+2
      &> \alpha(x)+1
      = \interpret{{\rm g}(x),\alpha}\\
      \interpret{{\rm f}({\rm g}(x)),\alpha} 
      = \alpha(x)+2
      &\ge \alpha(x)+2
      = \interpret{{\rm g}({\rm f}(x)),\alpha}
  \end{align*}
  \vspace{-1.5em}
  \pause
  
  The first rule is strictly decreasing, hence we can remove it.\\[1em]
  \pause
  
  Thus for termination it sufficies to show $\SN({\rm f}({\rm g}(x)) \to {\rm g}({\rm f}(x)))$.
  \medskip
  \pause
  
  We have already shown this a few slides ago.\\
  Hence we have proven termination.
  \end{example}
\end{frame}