\begin{frame}
  \small
  
  \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<0->{\alert{\text{\ding{200}}}} &
  \onslide<0->{\GREEN{x+\m{p}(y)}}
  & \onslide<0->{\GREEN{\to}} & \onslide<0->{\GREEN{\m{p}(x+y)}} &
  \onslide<0->{\alert{\text{\ding{201}}}} &
  \onslide<0->{\GREEN{x-\m{p}(y)}}
  & \onslide<0->{\GREEN{\to}} & \onslide<0->{\GREEN{\m{s}(x-y)}}
  \end{array}
  \]\vspace{-2ex}
  \begin{itemize}
  \item
  added rewrite rules
  \[
  \GREEN{\begin{array}{lr@{~}c@{~}l@{\qquad}lr@{~}c@{~}l}
  \structure{\text{\ding{200}}} & x+\m{p}(y) & \to & \m{p}(x+y) &
  \structure{\text{\ding{201}}} & x-\m{p}(y) & \to & \m{s}(x-y)
  \end{array}}
  \]
  preserve termination
  (extend LPO precedence with $\GREEN{+} > \mG{p}$ and $\GREEN{-} > \mG{s}$)
  \item<2->
    rules $\structure{\text{\ding{198}}}$ and $\structure{\text{\ding{199}}}$ are now superfluous:
    \begin{itemize}
      \item $\m{s}(x+\m{p}(y)) \stackrel{\structure{\text{\ding{200}}}}{\to} \m{s}(\m{p}(x+y)) \stackrel{\structure{\text{\ding{197}}}}{\to} x+y$
      \item $\m{p}(x-\m{p}(y)) \stackrel{\structure{\text{\ding{201}}}}{\to} \m{p}(\m{s}(x-y)) \stackrel{\structure{\text{\ding{196}}}}{\to} x-y$
    \end{itemize}
    \pause[3]
    Thus \alert{we can drop the rules $\alert{\text{\ding{198}}}$ and $\alert{\text{\ding{199}}}$}.
  \end{itemize}
  \end{example}
\end{frame}