22/251
\begin{frame}
\small

\begin{example}[Addition on Natural Numbers in Unary Notation]
\smallskip
\begin{tabular}{l@{\qquad}l}
\alert<1>{signature} &
$\mG{0}$ ~ (constants) \quad $\mG{s}$ ~ (unary) \quad
$\mG{+}$ ~ (binary, infix) \\
\\[-1ex]
\onslide<2->\alert<2>{terms} &
\GREEN{$\m{s}(\m{s}(\m{0}))$ \quad
$\m{s}(\m{0})+ \m{s}(\m{s}(\m{0}))$ \quad $\m{s}(x)+y$} \\
\\[-1ex]
\onslide<3->\alert<3>{rewrite rules} &
\GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l@{}}
\alert<8>{\m{0}+y} & \alert<9>{\to} & \alert<9>{y} \\[.5ex]
\alert<6>{\m{s}(x)+y} & \alert<7>{\to} & \alert<7>{\m{s}(x+y)}
\end{array}$} \\
\\[-1ex]
\onslide<4->\alert<4->{rewriting} &
\GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l}
\alert<5,6>{\m{s}(\m{0})+\m{s}(\m{s}(\m{0}))}
& \onslide<7->{\to} &
\onslide<7->{\alert<7>{\m{s}(\alert<8>{\m{0}+\m{s}(\m{s}(\m{0}))})}}
\onslide<6->{\makebox[3cm][l]{$\qquad
\alert<6-8>{\onslide<6,7>{x \mapsto \m{0}} \quad
y \mapsto \m{s}(\m{s}(\m{0}))}$}} \\[.5ex]
& \onslide<9->{\to} &
\onslide<9->{\m{s}(\alert<9>{\m{s}(\m{s}(\m{0}))})}
\end{array}$}
\end{tabular}
\end{example}

\end{frame}