\begin{frame}[t]
  \frametitle{Example: Ackermann function}
  
  \vspace{-1em}
  \begin{example}
  \vspace{-1em}
  \begin{align*}
    {\rm Ack}(0,y) &\to {\rm s}(y)\\
    {\rm Ack}({\rm s}(x),0) &\to {\rm Ack}(x,{\rm s}(0))\\
    {\rm Ack}({\rm s}(x),{\rm s}(y)) &\to {\rm Ack}(x,{\rm Ack}({\rm s}(x),y))
  \end{align*}
  \vspace{-3.5em}
  \pause
  
  \begin{align*}
  \DP(R) = \{\;
    \only<-4>{\alert<4>{{\rm Ack_\#}(0,y)} &\alert<4>{\to {\rm s_\#}(y)}\\}
    \only<-7>{{\rm Ack_\#}(\alert<6>{{\rm s}(x)},0) &\to {\rm Ack_\#}(\alert<6>{x},{\rm s}(0))\\}
    \only<-4>{\alert<4>{{\rm Ack_\#}({\rm s}(x),0)} &\alert<4>{\to {\rm s_\#}(0)}\\}
    \only<-4>{\alert<4>{{\rm Ack_\#}({\rm s}(x),0)} &\alert<4>{\to 0_\#}\\}
    \only<-7>{{\rm Ack_\#}(\alert<6>{{\rm s}(x)},{\rm s}(y)) &\to {\rm Ack_\#}(\alert<6>{x},{\rm Ack}({\rm s}(x),y))\\}
    {\rm Ack_\#}(\alert<6>{{\rm s}(x)},\alert<9>{{\rm s}(y)}) &\to {\rm Ack_\#}(\alert<6>{{\rm s}(x)},\alert<9>{y})
    \only<-4>{\\\alert<4>{{\rm Ack_\#}({\rm s}(x),{\rm s}(y))} &\to \alert<4>{{\rm s_\#}(x)}}
  \;\}
  \end{align*}
  \vspace{-1.5em}
  \pause
  
  \alt<-4>{
  We use the interpretation:
  \vspace{-.7em}
  \begin{gather*}
    \interpret{{\rm Ack_\#}}(x,y) = 1 \quad \interpret{{\rm Ack}}(x,y) = 0 \quad \interpret{{\rm s}}(x) = 0
    \quad \interpret{{\rm 0}} = 0 \quad {\rm s_\#}(x) = 0
  \end{gather*}
  \vspace{-1.5em}
  }{}
  \alt<5-7>{
  We use the subterm criterion:
  \vspace{-.7em}
  \begin{gather*}
    \pi({\rm Ack_\#}) = \alt<6->{1}{?}
  \end{gather*}
  \onslide<7>
  We can remove the first two DP-rules.
  \smallskip
  }{}
  \alt<8-11>{
  We use the subterm criterion:
  \vspace{-.7em}
  \begin{gather*}
    \pi({\rm Ack_\#}) = \alt<9->{2}{?}
  \end{gather*}
  \onslide<10->
  We can remove the remaining DP-rule.
  \medskip\onslide<11->
  
  Hence we have proven termination.
  }{}
  \end{example}
\end{frame}