\begin{frame} \frametitle{Example 2} \begin{example} $${\rm f}({\rm g}(x)) \to {\rm g}({\rm f}(x))$$ Find a polynomial interpretation over $\nat$ which proves termination: \begin{align*} \interpret{{\rm f}}(x) &= \alt<2->{2\cdot x}{???} & \interpret{{\rm g}}(x) &= \alt<2->{x+1}{???} \end{align*} \vspace{-2em} \begin{itemize} \item<3-> \gemph{Are the functions $[f]$ monotone?}\\\smallskip \onslide<4-> Yes, since whenever $a > b$, then \\\quad $\interpret{{\rm f}}(a) = 2\cdot a > 2\cdot b = \interpret{{\rm f}}(b)$, \\\quad $\interpret{{\rm g}}(a) = a+1 > b+1 = \interpret{{\rm g}}(b)$,\\[1em] \item<5-> \gemph{Does $\interpret{\ell,\alpha} > \interpret{r,\alpha}$ hold?}\\\smallskip \onslide<6-> Yes since, \vspace{-.8em} \begin{align*} \interpret{{\rm f}({\rm g}(x)),\alpha} = 2\cdot(\alpha(x)+1) > 2\cdot \alpha(x) + 1 = \interpret{{\rm g}({\rm f}(x)),\alpha} \end{align*} \vspace{-2em} \end{itemize} \onslide<7-> Hence we have proven termination. \end{example} \end{frame}