14/53
\begin{frame}[fragile]
  \small
  
  \begin{example}
  \smallskip
  \newcommand{\sGREEN}[1]{\onslide<1->\GREEN{#1}\onslide<2->}
  \[
  \onslide<2->
  \renewcommand{\arraystretch}{1.15}
  \begin{array}{@{}c@{}r@{~}c@{~}l|r@{~}c@{~}l@{}c@{}}
  \text{\ding{192}} &
  \sGREEN{\begin{array}{r@{}} \m{0} + y \\ \m{s}(x) + y \end{array}} &
  \sGREEN{\begin{array}{@{}c@{}} \to \\ \to \end{array}} &
  \sGREEN{\begin{array}{@{}l} y \\ \m{s}(x + y) \end{array}} &
  \sGREEN{\begin{array}{r@{}}
  \m{0} \times y \\ \m{s}(x) \times y
  \end{array}} &
  \sGREEN{\begin{array}{@{}c@{}} \to \\ \to \end{array}} &
  \sGREEN{\begin{array}{@{}l} \m{0} \\ x \times y + y \end{array}} &
  \text{\ding{193}} \\
  \hline
  \text{\ding{194}} &
  \sGREEN{\begin{array}{r@{\:-\:}l@{}}
  \m{0} & y \\ x & \m{0} \\ \m{s}(x) & \m{s}(y)
  \end{array}} &
  \sGREEN{\begin{array}{@{}c@{}}
  \to \\ \to \\ \to
  \end{array}} &
  \sGREEN{\begin{array}{@{}l}
  \m{0} \\ x \\ x - y
  \end{array}} &
  \sGREEN{\begin{array}{l@{}}
  \m{fib}(\m{0}) \\ \m{fib}(\m{s}(\m{0})) \\ \m{fib}(\m{s}(\m{s}(x)))
  \end{array}} &
  \sGREEN{\begin{array}{@{}c@{}}
  \to \\ \to \\ \to
  \end{array}} &
  \sGREEN{\begin{array}{@{}l}
  \m{s}(\m{0}) \\ \m{s}(\m{0}) \\ \m{fib}(\m{s}(x)) + \m{fib}(x)
  \end{array}} &
  \text{\ding{195}} \\
  \hline
  \text{\ding{196}} &
  \sGREEN{\begin{array}{r@{}}
  \NIL \APPEND x \\ (x : y) \APPEND z
  \end{array}} &
  \sGREEN{\begin{array}{@{}c@{}} \to \\ \to \end{array}} &
  \sGREEN{\begin{array}{@{}l}
  x \\ x : (y \APPEND z)
  \end{array}} &
  \sGREEN{\begin{array}{r@{}}
  \m{0} \div \m{s}(y) \\ \m{s}(x) \div \m{s}(y)
  \end{array}} &
  \sGREEN{\begin{array}{@{}c@{}} \to \\ \to \end{array}} &
  \sGREEN{\begin{array}{@{}l}
  \m{0} \\ \m{s}((x - y) \div \m{s}(y))
  \end{array}} &
  \text{\ding{197}} \\
  \hline
  \text{\ding{198}} &
  \sGREEN{\begin{array}{r@{\:\wedge\:}l@{}}
  \TRUE & \FALSE \\ \FALSE & \TRUE \\ x & x
  \end{array}} &
  \sGREEN{\begin{array}{@{}c@{}}
  \to \\ \to \\ \to
  \end{array}} &
  \sGREEN{\begin{array}{@{}l}
  \FALSE \\ \FALSE \\ x
  \end{array}} &
  \sGREEN{\begin{array}{r@{\:<\:}l@{}}
  x & \m{0} \\ \m{0} & \m{s}(y) \\ \m{s}(x) & \m{s}(y)
  \end{array}} &
  \sGREEN{\begin{array}{@{}c@{}}
  \to \\ \to \\ \to
  \end{array}} &
  \sGREEN{\begin{array}{@{}l}
  \FALSE \\ \TRUE \\ x < y
  \end{array}} &
  \text{\ding{199}} \\
  \hline
  \text{\ding{200}} &
  \sGREEN{\begin{array}{l@{}}
  \SUM(\NIL) \\ \SUM(x : y)
  \end{array}} &
  \sGREEN{\begin{array}{@{}c@{}} \to \\ \to \end{array}} &
  \sGREEN{\begin{array}{@{}l} \m{0} \\ x + \SUM(y) \end{array}} &
  \sGREEN{\begin{array}{l@{}}
  \LENGTH(\NIL) \\ \LENGTH(x : y)
  \end{array}} &
  \sGREEN{\begin{array}{@{}c@{}} \to \\ \to \end{array}} &
  \sGREEN{\begin{array}{@{}l} \m{0} \\ \m{s}(\LENGTH(y)) \end{array}} &
  \text{\ding{201}}
  \end{array}
  \renewcommand{\arraystretch}{1}
  \]
  
  \newcommand{\DU}{\makebox[5mm]{%
  \begin{tabular}[t]{c}
  \ding{59} \\[-1ex]
  \scriptsize \alert{d} \\[-3ex]
  \end{tabular}}}
  \newcommand{\CSC}{\makebox[5mm]{%
  \begin{tabular}[t]{c}
  \ding{59} \\[-1ex]
  \scriptsize \alert{cs} \\[-3ex]
  \end{tabular}}}
  \newcommand{\HC}{\makebox[5mm]{%
  \begin{tabular}[t]{c}
  \ding{59} \\[-1ex]
  \scriptsize \alert{h}
  \end{tabular}}}
  
  \centerline{
  \ding{192} \onslide<3->{\HC}
  \ding{193} \onslide<4->{\CSC}
  \ding{194} \onslide<5->{\HC}
  \ding{195} \onslide<6->{\DU}
  \ding{196} \onslide<7->{\HC}
  \ding{197} \onslide<8->{\DU}
  \ding{198} \onslide<9->{\CSC}
  \ding{199} \onslide<10->{\HC}
  \ding{200} \onslide<11->{\CSC}
  \ding{201}
  }
  \end{example}
\end{frame}