\begin{frame} \small \begin{example} \smallskip ES $\EE$ \[ \GREEN{\begin{array}{r@{~}c@{~}l} \m{0}+y & \approx & y \\[.5ex] \m{s}(x)+y & \approx & \m{s}(x+y) \end{array}} \] \medskip \onslide<2-> $\EE \vdash \GREEN{\m{s(s(0)}+\m{s(0))} \approx \m{s(s(s(0)))}}$ \onslide<3-> \[ \frac{ \makebox[0pt][r]{\structure{$\mathtt{[a]}$}\:} \frac{}{\textstyle \GREEN{\m{s}(0)+\m{s(0)} \approx \m{s}(0+\m{s}(0))}% \rule[-1.5ex]{0pt}{4ex}} \quad \tfrac{ \tfrac{}{\textstyle \GREEN{\m{0}+\m{s(0)} \approx \m{s(0)}}\rule[-1.5ex]{0pt}{4ex}} \makebox[0pt][l]{\:\structure{$\mathtt{[a]}$}} }{\textstyle \GREEN{\m{s}(0+s\m{(0))} \approx \m{s(s(0))}}\rule[-1.5ex]{0pt}{4ex}} \makebox[0pt][l]{\:\structure{$\mathtt{[c]}$}} }{ \frac{\textstyle \GREEN{\m{s(0)}+\m{s(0)} \approx \m{s(s(0))}}\rule[-1.5ex]{0pt}{4ex} }{\textstyle \GREEN{\m{s}(\m{s}(0)+\m{s}(0)) \approx \m{s(s(s(0)))}}% \rule[-1.5ex]{0pt}{4ex}} \makebox[0pt][l]{\:\structure{$\mathtt{[c]}$}}} \makebox[0pt][l]{\:\structure{$\mathtt{[t]}$}} \] \end{example} \end{frame}