\begin{frame}
  \small
  
  \begin{theorem}
  Properties of $\overline{\atrs}$ for orthogonal TRSs $\atrs$:
  \begin{itemize}
    \item $\overline{\atrs}$ is orthogonal.
    \item $\overline{\atrs}$ is SN.
    \item $\overline{\atrs}$ is CR.
  \end{itemize}
  \end{theorem}
  \medskip\pause
  
  \begin{proof}
    The orthogonality of $\overline{\atrs}$ is immediate. Hence $\overline{\atrs}$ is CR.
    \bigskip\pause
    
    For SN we show that $\overline{\atrs}$ is ILPO terminating where $\overline{f} > g$ for every $f,g \in \FF$.
    \smallskip\pause
    
    Let $\ell = \overline{f}(\ell_1,\ldots,\ell_n)$ and $r \in \TT(\FF,\VV)$ with $\Var(r) \subseteq \Var{\ell}$.
    \smallskip\pause
    
    Then $\ell^* \to_{\mathit{ilpo}}^* r$ by induction on $r$:
    \begin{itemize}
    \pause
      \item If $r \in \Var(\ell)$, then we use $\to_{\mathit{put}}$ and $\to_{\mathit{select}}$.
    \pause
      \item If $r = g(r_1,\ldots,r_m)$, then we use $\ell^* \to_{\mathit{copy}} g(\ell^*,\ldots,\ell^*)$.\\\pause
            Moreover by the induction hypothesis $\ell^* \to_{\mathit{ilpo}}^* r_i$ for every $i$.
    \end{itemize}
    \vspace{-3ex}
  \end{proof}
\end{frame}