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