\begin{frame}
  \frametitle{Results for (Weakly) Orthogonal TRSs}
  
  \begin{theorem}
  Every weakly orthogonal TRS \alert{without collapsing rules} is $\CRi$.
  \end{theorem}
  \pause\medskip
  
  \begin{definition}
  A TRS $\atrs$ is $\UNi$ if  $s \iredi \cdot \ired t \Rightarrow s = t$ for all normal forms $s,t \in \iter$.
  \end{definition}
  \pause
  
  \begin{theorem}
  Every orthogonal TRS is $\UNi$.
  \end{theorem}
  \pause
  
  \begin{example}
  Weakly orthogonal TRSs are not necessarily $\UNi$:
  \vspace{-1ex}
  \begin{align*}
    S(P(x)) &\to x & P(S(x)) &\to x
  \end{align*}
  Then
  \vspace{-2ex}
  \begin{align*}
    S^\omega \iredi S^1(P^2(S^3(P^4(\ldots)))) \ired P^\omega
  \end{align*}
  \vspace{-4ex}
  \end{example}
\end{frame}