361/365
\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}