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