\begin{frame} \frametitle{Example 1} \begin{example} $${\rm f}({\rm g}(x)) \to {\rm f}({\rm f}(x))$$ Find a polynomial interpretation over $\nat$ which proves termination: \begin{align*} \interpret{{\rm f}}(x) &= \alt<2->{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) = a > 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} = \interpret{{\rm f}}(\interpret{{\rm g}}(\alpha(x))) = \alpha(x)+1 > \alpha(x) = \interpret{{\rm f}({\rm f}(x)),\alpha} \end{align*} \vspace{-2em} \end{itemize} \onslide<7-> Hence we have proven termination. \smallskip \end{example} \end{frame}