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