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