\begin{frame} \frametitle{Example: ${\rm f}({\rm f}(x)) \to {\rm f}({\rm g}({\rm f}(x)))$} \begin{example} \pause \vspace{-1em} \begin{align*} \DP(R) = \{\; &{\rm f}_\#({\rm f}(x)) \to{\rm f}_\#({\rm g}({\rm f}(x))),\\ &{\rm f}_\#({\rm f}(x)) \to {\rm g}_\#({\rm f}(x)),\\ &{\rm f}_\#({\rm f}(x)) \to {\rm f}_\#(x) \;\} \end{align*} \vspace{-3.5em} \pause \begin{align*} \interpret{{\rm f}}(x) &= \alt<4->{x+1}{???} & \interpret{{\rm f}_\#}(x) &= \alt<4->{x+1}{???} & \interpret{{\rm g}}(x) &= \alt<4->{0}{???} & \interpret{{\rm g}_\#}(x) &= \alt<4->{0}{???} \end{align*} \pause\pause \vspace{-1.5em} \begin{itemize} \alt<-6>{ \item \gemph{Are the functions $[f]$ monotone w.r.t. $\ge$?}\\\pause Yes, since whenever $a \ge b$, then \\\quad $\interpret{{\rm f}}(a) = a + 1 \ge b + 1 = \interpret{{\rm f}}(b)$, \\\quad $\interpret{{\rm g}}(a) = 0 \ge 0 = \interpret{{\rm g}}(b)$,\\[1em] }{ \pause\pause \item \gemph{Does $\interpret{\ell,\alpha} > \interpret{r,\alpha}$ for all $\ell \to r \in \DP(R)$ hold?} \pause \vspace{-.8em} \begin{align*} \interpret{{\rm f}_\#({\rm f}(x)),\alpha} = \alpha(x)+2 &> 1 = \interpret{{\rm f}_\#({\rm g}({\rm f}(x))),\alpha}\\ \interpret{{\rm f}_\#({\rm f}(x)),\alpha} = \alpha(x)+2 &> 0 = \interpret{{\rm g}_\#({\rm f}(x)),\alpha}\\ \interpret{{\rm f}_\#({\rm f}(x)),\alpha} = \alpha(x)+2 &> \alpha(x)+1 = \interpret{{\rm f}_\#(x),\alpha} \end{align*} \vspace{-1.8em} \pause \item \gemph{Does $\interpret{\ell,\alpha} \ge \interpret{r,\alpha}$ for all $\ell \to r \in R$ hold?} \pause \vspace{-.8em} \begin{align*} \interpret{{\rm f}({\rm f}(x)),\alpha} = \alpha(x)+2 \ge 1 = \interpret{{\rm f}({\rm g}({\rm f}(x))),\alpha} \end{align*} \vspace{-2.3em} } \end{itemize} \onslide<11>{Hence we have proven termination.} \end{example} \end{frame}