\begin{frame}
  \frametitle{ILPO\ldots The star TRS $\itrslex{\arel}$}
  
  Given a terminating relation  $\arel$ on signature $\asig$,
  define TRS $\alert{\itrslex{\arel}}$
  \pause
  
  \begin{itemize}
   \item  Signature: $\setsum{\asig}{\asjg}$, where  $\asjg = \{\asxmone \;\mid\;  \setin{\asymone}{\asig}\}$
     \smallskip
  
     \quad  $\asxmone$ is fresh and has the same arity as  $\asymone$
  
  \pause
   \item Reduction rules (four types, for arbitrary $\asymone$, $\bsymone \in \asig$):
  \begin{changemargin}{-1cm}{-0cm}
     \vspace{-1.5em}
     \begin{align*}
     \onslide<4->\symonea{\vec{\atrmvar}} &\onslide<4->\mathrel{\sirulstr{\text{put}}} \sxmonea{\vec{\atrmvar}}\\[.2em]
     \onslide<5->\sxmonea{\vec{\atrmvar}} &\onslide<5->\mathrel{\sirulstr{\text{select}}} \aitrmvar{\aidx}\\[.2em]
     \onslide<6->\sxmonea{\vec{\atrmvar}} &\onslide<6->\mathrel{\sirulstr{\text{copy}}} \symoneb{\sxmonea{\vec{\atrmvar}},\ldots,\sxmonea{\vec{\atrmvar}}}
        &&\onslide<6-> \text{if } \rela{\asymone}{\bsymone}\\[.2em]
     \onslide<7->\sxmonea{\vec{\atrmvar},\symoneb{\vec{\btrmvar}},\vec{\ctrmvar}}
      &\onslide<7->\mathrel{\sirulstr{\text{lex}}}
      \symonea{\vec{\atrmvar},\sxmoneb{\vec{\btrmvar}},\alhs,\ldots,\alhs}
        &&\onslide<7-> \text{where }\alhs \isdefd \sxmonea{\vec{\atrmvar},\symoneb{\vec{\btrmvar}},\vec{\ctrmvar}}
     \end{align*}
     \vspace{-2em}
  \end{changemargin}
  \end{itemize}
  \onslide<8->
  \begin{definition}[ILPO]
  $\rewlex{\arel}$ is the restriction of ${\reltra{\airew{\itrslex{\arel}}}}$ to terms over $\asig$, i.e.
  \vspace{-.5em}
  $$t \mathrel{\rewlex{\arel}} s \iff
    t \reltra{\airew{\itrslex{\arel}}} s \;\;\wedge\;\; t,s \in \trmover{\setsum{\asig}{\aTrmvar}}$$
  \vspace{-1.5em}
  \end{definition}

\end{frame}