\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}