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