\begin{frame}[t] \frametitle{Example, Ackermann Function} \vspace{-2ex} \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{-1.5em} Find an order $\arel$ on $\asig$ which proves termination. \pause \medskip \centerline{${\rm Ack} \arel {\rm s}$} \medskip \pause We get the following derivations: \vspace{-.5em} \begin{align*} \alt<1-12>{ {\rm Ack}(0,y) &\pause\myairew{\text{put}} \mrk{\rm Ack}(0,y) \pause \myairew{\text{copy}} {\rm s}(\mrk{\rm Ack}(0,y)) \pause \myairew{\text{select}} {\rm s}(y)\\ \pause {\rm Ack}({\rm s}(x),0) &\pause\myairew{\text{put}} \mrk{\rm Ack}({\rm s}(x),0) \pause \myairew{\text{lex}} {\rm Ack}(\mrk{\rm s}(x),\mrk{\rm Ack}({\rm s}(x),0))\\ &\pause\myairew{\text{select}} {\rm Ack}(x,\mrk{\rm Ack}({\rm s}(x),0)) \pause \myairew{\text{copy}} {\rm Ack}(x,{\rm s}(\mrk{\rm Ack}({\rm s}(x),0))) \\ &\pause \myairew{\text{select}} {\rm Ack}(x,{\rm s}(0)) }{ \pause\pause\pause\pause\pause\pause\pause\pause\pause\pause {\rm Ack}({\rm s}(x),{\rm s}(y)) &\pause\myairew{\text{put}} \mrk{\rm Ack}({\rm s}(x),{\rm s}(y))\\ &\pause\myairew{\text{lex}} {\rm Ack}(\mrk{\rm s}(x),\mrk{\rm Ack}({\rm s}(x),{\rm s}(y)))\\ &\pause\myairew{\text{select}} {\rm Ack}(x,\mrk{\rm Ack}({\rm s}(x),{\rm s}(y)))\\ &\pause\myairew{\text{lex}} {\rm Ack}(x,{\rm Ack}({\rm s}(x),\mrk{\rm s}(y)))\\ &\pause\myairew{\text{select}} {\rm Ack}(x,{\rm Ack}({\rm s}(x),y)) % } \end{align*} \vspace{-1.5em} \onslide<18>{Hence we have proven termination.} \end{example} \end{frame}