\begin{frame}
  \frametitle{ILPO}
  
  \begin{claim}
  $\rewlex{\arel}$ is a reduction order, that is:
  \begin{itemize}
    \item $\rewlex{\arel}$ is well-founded, and
    \item closed under substitution and contexts
  \end{itemize}
  \end{claim}
  \pause
  \medskip
  
  The closure under substitutions and contexts is immediate since ${\reltra{\airew{\itrslex{\arel}}}}$ is.
  \pause\medskip
  
  \alert{Only required}: proof of termination of $\rewlex{\arel}$.
  
  \medskip\pause
  
  \begin{corollary}
    A TRS $\atrs$ is terminating if ${\atrs} \subseteq {\rewlex{\arel}}$.
  \end{corollary}
  \smallskip
  \pause
  
  {\bf Proof.} $\rewlex{\arel}$ is a reduction order with ${\atrs} \subseteq {\rewlex{\arel}}$.
\end{frame}