\begin{frame}[t]
  \frametitle{Termination of $\trsllex$ \`a la Buchholz}
  
  \vspace{-1ex}
  \begin{block}{}
  Prove the implication 
  $$\mbox{$t_1,\ldots,t_n$ are terminating} 
    \;\implies\; \lsymonea{\ell}{t_1,\ldots,t_n} \text{ is terminating}$$
  by induction on triple  $\langle \asymone, \vec{t}, \ell\rangle$ 
  in ordering 
  $\langle\arel, (\airew{\itrsllex{\arel}})^\anat, \sorngt\rangle$.
  \end{block}
  \medskip\pause
  
  \begin{changemargin}{1cm}{0cm}
  \begin{itemize}
  \alt<1-4>{
    \item [Case 1.]
          Internal step $\lsymonea{\ell}{\ldots,t_i,\ldots} \to  \lsymonea{\ell}{\ldots,t_i',\ldots}$.\\
          \smallskip
          The triple decreases in the second component.
          \medskip
  \pause
    \item [Case 2.] $\lsymonea{}{t_1,\ldots,t_n} \myairew{\text{put}}  \lsymonea{\anat}{t_1,\ldots,t_n}$.\\
          \smallskip
          We have a decrease in the third component.
          \medskip
  \pause
    \item [Case 3.] $\lsymonea{\anat}{t_1,\ldots,t_n} \myairew{\text{select}}  t_i$.\\
          \smallskip
          By assumption $t_i$ is SN.
          \medskip
  }{
    \item [Case 4.] $\lsymonea{\anat+1}{\vec{t}} \myairew{\text{copy}}  \symoneb{\lsymonea{\anat}{\vec{t}},\ldots,\lsymonea{\anat}{\vec{t}}}$.\\
          \smallskip
          By IH the arguments $\lsymonea{\anat}{\vec{t}}$ of $\bsymone$ are SN since $\anat + 1 > \anat$.\\
          Again by IH the term $\symoneb{\ldots}$ itself is SN, since $\asymone \arel \bsymone$.
          \medskip
  \pause \pause \pause \pause
    \item [Case 5.] $\lsymonea{\anat+1}{\vec{t},\symoneb{\vec{s}},\vec{r}}
                     \myairew{\text{lex}}
                     \symonea{\vec{t},\lsymoneb{\anat}{\vec{s}},\alhs,\ldots,\alhs}$, 
                    $\alhs \isdefd \lsymonea{\anat}{\vec{t},\symoneb{\vec{\btrmvar}},\vec{r}}$.\\
          \smallskip
          By assumption the arguments $\vec{t}$ and $\symoneb{\vec{s}}$ are SN.\\
          By IH we get $l$ is SN.\\
          Since $\symoneb{\vec{s}} \myairew{\text{put}} \lsymoneb{\anat}{\vec{s}}$ we get
          \begin{itemize}
          \item $\lsymoneb{\anat}{\vec{s}}$ is SN, and
          \item the triple decreases in the second component.
          \end{itemize}
          Thus by IH $\symonea{\vec{t},\lsymoneb{\anat}{\vec{s}},\alhs,\ldots,\alhs}$ is SN.
  }
  \onslide<6>{}
  \end{itemize}
  \end{changemargin}
\end{frame}