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