48/144
\begin{frame}
\small

\begin{example}[Binary Trees]
\smallskip
\begin{tabular}{l@{\qquad}l}
\alert<1-2>{signature} &
\GREEN{$0$} ~ \GREEN{$1$} ~ $\cdots$ ~ \GREEN{$9$} ~
(constants) \quad \GREEN{$\m{+}$} ~ \GREEN{$\m{:}$} ~ (binary, infix)
\\[.5ex]
& \onslide<2->{\GREEN{$\m{leaf}$} ~ \GREEN{\m{sum}} ~ (unary) ~ 
\GREEN{$\m{node}$} ~ (binary)} \\
\onslide<3-> \\
\alert<3>{terms} &
\GREEN{$\m{leaf}((1:0):0)$ \quad 
$\m{node}(\m{leaf}(1),\m{leaf}(2))$ \quad
$\m{leaf}(\m{node}(1,\m{leaf}(2)))$} \\  
\onslide<4-> \\
\alert<4>{rewrite rules} &
\GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l}
& \makebox[0mm]{$\cdots$} & \\
\m{sum}(\m{leaf}(x)) & \to & x \\[.5ex]
\m{sum}(\m{node}(x,y)) & \to & \m{sum}(x) + \m{sum}(y)
\end{array}$} \\
\onslide<5-> \\
\alert<5-8>{rewriting} &
\GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l}
\makebox[2cm][l]{$
\alert<6>{\m{sum}(\m{node}(\m{leaf}(2:3),\m{leaf}(7:7)))}$}
\\[.5ex]
& \onslide<6->{\to^{\phantom{*}}} &
\onslide<6->{\alert<7>{\m{sum}(\m{leaf}(2:3))} +
\alert<7>{\m{sum}(\m{leaf}(7:7))}}
\\[.5ex]
& \onslide<7->{\to^*} &
\onslide<7->{\alert<8>{(2:3) + (7:7)}}
\\[.5ex]
& \onslide<8->{\to^*} &
\onslide<8->{(1:0):0}
\end{array}$}
\end{tabular}
\end{example}

\end{frame}