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