\begin{frame}
  \small
  
  \begin{example}[cont'd]
  \smallskip
  TRS
  $\RR = \{ \sd{192}, \sd{193}, \sd{194}, \sd{195}, \sd{196}, \sd{197} \}$
  \hfill \onslide<2->{TRS $\SS = \{ \sd{192}, \sd{193}, \sd{194}, \sd{195},
  \sd{196}, \sd{197}, \sda{200}, \sda{201} \}$}
  \[
  \begin{array}{lr@{~}c@{~}l@{\qquad}lr@{~}c@{~}l}
  \structure{\text{\ding{192}}} & \GREEN{x+\m{0}}
  & \GREEN{\to} & \GREEN{x} &
  \structure{\text{\ding{193}}} & \GREEN{x+\m{s}(y)}
  & \GREEN{\to} & \GREEN{\m{s}(x+y)}
  \\
  \structure{\text{\ding{194}}} & \GREEN{x-\m{0}}
  & \GREEN{\to} & \GREEN{x} &
  \structure{\text{\ding{195}}} & \GREEN{x-\m{s}(y)}
  & \GREEN{\to} & \GREEN{\m{p}(x-y)}
  \\
  \structure{\text{\ding{196}}} & \GREEN{\m{p}(\m{s}(x))}
  & \GREEN{\to} & \GREEN{x} &
  \structure{\text{\ding{197}}} & \GREEN{\m{s}(\m{p}(x))}
  & \GREEN{\to} & \GREEN{x}
  \\
%   \onslide<2->{\alert{\text{\ding{198}}}} &
%   \onslide<2->{\GREEN{\m{s}(x+\m{p}(y))}}
%   & \onslide<2->{\GREEN{\to}} & \onslide<2->{\GREEN{x+y}} &
%   \onslide<2->{\alert{\text{\ding{199}}}} &
%   \onslide<2->{\GREEN{\m{p}(x-\m{p}(y))}}
%   & \onslide<2->{\GREEN{\to}} & \onslide<2->{\GREEN{x-y}} \\
  \onslide<2->{\alert{\text{\ding{200}}}} &
  \onslide<2->{\GREEN{x+\m{p}(y)}}
  & \onslide<2->{\GREEN{\to}} & \onslide<2->{\GREEN{\m{p}(x+y)}} &
  \onslide<2->{\alert{\text{\ding{201}}}} &
  \onslide<2->{\GREEN{x-\m{p}(y)}}
  & \onslide<2->{\GREEN{\to}} & \onslide<2->{\GREEN{\m{s}(x-y)}}
  \end{array}
  \]
  \begin{itemize}
  \item<3->
  \makebox[3cm][l]{$\SS$ is SN}
  LPO with precedence $\GREEN{+} > \mG{s}, \mG{p}$ and
  $\GREEN{-} > \mG{s}, \mG{p}$
  \item<4->
  \makebox[3cm][l]{$\SS$ is WCR}
  all critical pairs of $\SS$ are convergent
  \item<5->
  $\xleftrightarrow[\SS]{*} ~=~ \xleftrightarrow[\RR]{*}$
  \end{itemize}
  \end{example}
\end{frame}