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