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