\begin{frame}
  \begin{remark}
  \begin{itemize}
    \item \makebox[4cm][l]{$\SNi \not\Rightarrow \SN \onslide<2->{ \vee \WN}$} \GREEN{$a \to c(a)$}\\
          \makebox[4cm][l]{} \GREEN{Here, $a \ired c^\omega$ which is a normal form.}
  \pause\pause
    \item \makebox[4cm][l]{$\SN \mathrel{\onslide<4->{\not\Rightarrow}} \SNi \onslide<5->{\vee \WNi}$} \pause \GREEN{$I(x) \to x$}\\
          \makebox[4cm][l]{} \GREEN{Here, $I(I(I(\ldots)))$ rewrites only to itself.}
  \pause\pause
    \item \makebox[4cm][l]{$\CRi \mathrel{\onslide<7->{\not\Rightarrow}} \CR$} \pause \GREEN{$a\to b,\; a\to c,\; b \to d(b),\; c \to d(c)$}
          \makebox[4cm][l]{} \GREEN{Here, $\neg (b \join c)$, but $b \ired d^\omega \iredi c$.}
  \pause
    \item \makebox[4cm][l]{$\CR \mathrel{\onslide<9->{\not\Rightarrow}} \CRi$} \pause \GREEN{$A(x) \to x,\; B(x) \to x$}\\
          \makebox[4cm][l]{} \GREEN{Here, $A^\omega \iredi (AB)^\omega \ired B^\omega$.}
  \end{itemize}
  \end{remark}
  \pause
  
  \begin{remark}
  The example $A(x) \to x,\; B(x) \to x$ shows: not every orthogonal TRSs is $\CRi$.
  \pause\medskip
  
  Even one collapsing rule is sufficient to violate $\CRi$.\\
  \pause
  Take $R = \{\;f(x,y) \to y\;\}$.
  Then
  \begin{align*}
    f(x,f(x,f(x,\ldots))) \iredi f(x,f(y,f(x,f(y,\ldots)))) \ired f(y,f(y,f(y,\ldots)))
  \end{align*}
  \end{remark}
\end{frame}