20/210
\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

$\EE \vdash \GREEN{\m{s(s(0)}+\m{s(0))} \approx \m{s(s(s(0)))}}$
$\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]}}}$
\onslide<2->
$\GREEN{\m{s(s(0)}+\m{s(0))} \alert<2>{\conv_{\EE}} \m{s(s(s(0)))}}$
$\GREEN{ \m{s(s(0)}+\m{s(0))} \leftrightarrow_{\EE} \m{s}(\m{s}(\m{0}+\m{s}(\m{0}))) \leftrightarrow_{\EE} \m{s}(\m{s}(\m{s}(\m{0}))) }$
\vspace{-3ex}
\end{example}
\end{frame}