\begin{frame}
  \frametitle{Auxiliary TRS with \emph{numerical} control symbols}
  
  Given a terminating relation  $\arel$ on signature $\asig$,
  define TRS $\alert{\itrsllex{\arel}}$
  \medskip
  
  \begin{itemize}
  \item  Signature: $\setsum{\asig}{\askg{\ornome}}$, where  $\askg{\ornome} = \{\asymone^{\anat} \;\mid\;  \setin{\asymone}{\asig},\; n \in \nat\}$
     \smallskip
  
     \quad $\asymone^{\anat}$ is fresh and has same arity as  $\asymone$
  \medskip
  
  \item Reduction rules:
  \begin{changemargin}{-1cm}{-0cm}
     \vspace{-1.5em}
     \begin{align*}
     \symonea{\vec{\atrmvar}} &\mathrel{\sirulstr{\text{put}}} \lsymonea{\anat}{\vec{\atrmvar}}\\[.2em]
     \lsymonea{\anat}{\vec{\atrmvar}} &\mathrel{\sirulstr{\text{select}}} \aitrmvar{\aidx}\\[.2em]
     \lsymonea{\anat+1}{\vec{\atrmvar}} &\mathrel{\sirulstr{\text{copy}}} \symoneb{\lsymonea{\anat}{\vec{\atrmvar}},\ldots,\lsymonea{\anat}{\vec{\atrmvar}}}
        && \text{if } \rela{\asymone}{\bsymone}\\[.2em]
     \lsymonea{\anat+1}{\vec{\atrmvar},\symoneb{\vec{\btrmvar}},\vec{\ctrmvar}}
      &\mathrel{\sirulstr{\text{lex}}}
      \symonea{\vec{\atrmvar},\lsymoneb{\anat}{\vec{\btrmvar}},\alhs,\ldots,\alhs}
        && \text{where }\alhs \isdefd \lsymonea{\anat}{\vec{\atrmvar},\symoneb{\vec{\btrmvar}},\vec{\ctrmvar}}
     \end{align*}
     \vspace{-2em}
  \end{changemargin}
  \end{itemize}
\end{frame}