\begin{frame}[t]
  \frametitle{Example 3}
  
  \vspace{-1em}
  \begin{example}
  \vspace{-1em}
  \begin{align*}
    {\rm A}(x,{\rm 0}) &\to x\\
    {\rm A}(x,{\rm s}(y)) &\to {\rm s}({\rm A}(x,y))
  \end{align*}
  \vspace{-1.5em}

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