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