\begin{frame}
  \small
  
  \vspace{-1ex}
  
  \begin{example}[cont'd]
  \[
  \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<0->{\alert{\text{\ding{198}}}} &
  \onslide<0->{\GREEN{\m{s}(x+\m{p}(y))}}
  & \onslide<0->{\GREEN{\to}} & \onslide<0->{\GREEN{x+y}} &
  \onslide<0->{\alert{\text{\ding{199}}}} &
  \onslide<0->{\GREEN{\m{p}(x-\m{p}(y))}}
  & \onslide<0->{\GREEN{\to}} & \onslide<0->{\GREEN{x-y}} 
  \\
  \onslide<5->{\alert{\text{\ding{200}}}} &
  \onslide<5->{\GREEN{x+\m{p}(y)}}
  & \onslide<5->{\GREEN{\to}} & \onslide<5->{\GREEN{\m{p}(x+y)}} &
  \onslide<6->{\alert{\text{\ding{201}}}} &
  \onslide<6->{\GREEN{x-\m{p}(y)}}
  & \onslide<6->{\GREEN{\to}} & \onslide<6->{\GREEN{\m{s}(x-y)}}
  \end{array}
  \]\vspace{-2ex}
  \begin{itemize}
  \item
    added rewrite rules $\structure{\text{\ding{198}}}$ and $\structure{\text{\ding{199}}}$ preserve termination \onslide<2-> and do not change $\xleftrightarrow{*}$
  \item<3->
  new critical pairs \\
  \begin{tabbing}
  \begin{tikzpicture}[on grid,baseline=(1).baseline,node distance=17mm]
  \node (1) {\MG{\ol{\m{p}(\ul{\m{s}(x+\m{p}(y))})}}};
  \node (2) [below left=of 1]  {\MGr{\m{p}(x+y)}};
  \node (3) [below right=of 1] {\MGl{x+\m{p}(y)}};
  \draw[->] (1) -- (2) node[midway,left]  {\ssd{198}};
  \draw[->] (1) -- (3) node[midway,right] {\ssd{196}};
  \onslide<5->{\alert{
  \draw[->] (3) -- (2) node[midway,below] {\scriptsize \ding{200}};
  }}
  \end{tikzpicture}
  \qquad\qquad\qquad \=
  \begin{tikzpicture}[on grid,baseline=(1).baseline,node distance=17mm]
  \node (1) {\MG{\ol{\m{s}(x+\ul{\m{p}(\m{s}(y))})}}};
  \node (2) [below left=of 1]  {\MGr{\m{s}(x+y)}};
  \node (3) [below right=of 1] {\MGl{x+\m{s}(y)}};
  \draw[->] (1) -- (2) node[midway,left]  {\ssd{196}};
  \draw[->] (1) -- (3) node[midway,right] {\ssd{198}};
  \onslide<4->{
  \draw[->] (3) -- (2) node[midway,below] {\ssd{193}};
  }
  \end{tikzpicture}
  \\[2ex]
  \begin{tikzpicture}[on grid,baseline=(1).baseline,node distance=17mm]
  \node (1) {\MG{\ol{\m{s}(\ul{\m{p}(x-\m{p}(y))})}}};
  \node (2) [below left=of 1]  {\MGr{\m{s}(x-y)}};
  \node (3) [below right=of 1] {\MGl{x-\m{p}(y)}};
  \draw[->] (1) -- (2) node[midway,left]  {\ssd{199}};
  \draw[->] (1) -- (3) node[midway,right] {\ssd{197}};
  \onslide<6->{\alert{
  \draw[->] (3) -- (2) node[midway,below] {\scriptsize \ding{201}};
  }}
  \end{tikzpicture}
  \>
  \begin{tikzpicture}[on grid,baseline=(1).baseline,node distance=17mm]
  \node (1) {\MG{\ol{\m{p}(x-\ul{\m{p}(\m{s}(y))})}}};
  \node (2) [below left=of 1]  {\MGr{\m{p}(x-y)}};
  \node (3) [below right=of 1] {\MGl{x-\m{s}(y)}};
  \draw[->] (1) -- (2) node[midway,left]  {\ssd{196}};
  \draw[->] (1) -- (3) node[midway,right] {\ssd{199}};
  \onslide<4->{
  \draw[->] (3) -- (2) node[midway,below] {\ssd{195}};
  }
  \end{tikzpicture}
  \end{tabbing}
  \end{itemize}
  \end{example}
\end{frame}