\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{itemize} \item Here $(\airew{\itrsllex{\arel}})^\anat$ is the lexicographic order on $n$-tuples \pause \item No label $\ell$ counts as $\infty$ with $\infty > n$. \end{itemize} \pause\bigskip In general a term is SN if all one-step reducts are SN.\\ \pause \begin{itemize} \item [$\Rightarrow$] We check all one step reducts of $\lsymonea{\ell}{t_1,\ldots,t_n}$. \end{itemize} \end{frame}