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