34/144
\begin{frame}
\small

\begin{example}[Addition on Natural Numbers in Decimal Notation]
\smallskip
\begin{tabular}{l@{\qquad}l}
\alert<1>{signature} &
\GREEN{$\m{0}$} ~ \GREEN{$\m{1}$} ~ $\cdots$ ~ \GREEN{$\m{9}$} ~
(constants) \quad \GREEN{$\m{+}$} ~ \GREEN{$\m{:}$} ~ (binary, infix) \\
\\[-1ex]
\onslide<2->\alert<2>{terms} &
\GREEN{$1+3$ \quad $2+(7:3)$ \quad $(2:(3:x))+((1+7):2)$} \\
\\[-1ex]
\onslide<3->\alert<3>{rewrite rules} &
\GREEN{$\begin{array}[t]{@{}r@{~}c@{~}lr@{~}c@{~}lc@{\quad}r@{~}c@{~}l@{}}
0+0 & \alert<0>{\to} & 0 &
1+0 & \alert<0>{\to} & 1 & \alert<0>{\cdots} &
9+0 & \alert<0>{\to} & 9 \\
0+1 & \alert<0>{\to} & 1 &
1+1 & \alert<0>{\to} & 2 & \alert<14,15>{\cdots} &
9+1 & \alert<0>{\to} & 1 : 0 \\
0+2 & \alert<0>{\to} & 2 &
1+2 & \alert<0>{\to} & 3 & \alert<0>{\cdots} &
9+2 & \alert<0>{\to} & 1 : 1 \\
0+3 & \alert<0>{\to} & 3 &
1+3 & \alert<0>{\to} & 4 & \alert<18,19>{\cdots} &
9+3 & \alert<0>{\to} & 1 : 2 \\
0+4 & \alert<0>{\to} & 4 &
1+4 & \alert<0>{\to} & 5 & \alert<0>{\cdots} &
9+4 & \alert<0>{\to} & 1 : 3 \\
0+5 & \alert<0>{\to} & 5 &
1+5 & \alert<0>{\to} & 6 & \alert<0>{\cdots} &
9+5 & \alert<0>{\to} & 1 : 4 \\
0+6 & \alert<0>{\to} & 6 &
1+6 & \alert<0>{\to} & 7 & \alert<0>{\cdots} &
9+6 & \alert<0>{\to} & 1 : 5 \\
0+7 & \alert<0>{\to} & 7 &
1+7 & \alert<0>{\to} & 8 & \alert<10,11>{\cdots} &
9+7 & \alert<0>{\to} & 1 : 6 \\
0+8 & \alert<0>{\to} & 8 &
1+8 & \alert<0>{\to} & 9 & \alert<0>{\cdots} &
9+8 & \alert<0>{\to} & 1 : 7 \\
0+9 & \alert<0>{\to} & 9 &
1+9 & \alert<0>{\to} & 1 : 0 & \alert<0>{\cdots} &
9+9 & \alert<0>{\to} & 1 : 8 \\
\multicolumn{7}{@{}l}{
\begin{array}{@{}r@{~}c@{~}l}
\alert<6,7>{x + (y : z)} & \alert<7>{\to} & \alert<7>{y : (x + z)}
\end{array}} & 0 : x & \alert<0>{\to} & x \\
\multicolumn{7}{@{}l}{
\begin{array}{@{}r@{~}c@{~}l}
\alert<5,8,9>{(x : y) + z} & \alert<9>{\to} & \alert<9>{x : (y + z)}
\end{array}} &
\makebox[0cm][r]{$\alert<12,13,16,17>{x : (y : z)}$} &
\alert<13,17>{\to} &
\alert<13,17>{(x + y) : z} \\
\end{array}$} \\
\\[-1ex]
\only{%
\onslide<4->\alert<4-20>{rewriting} &
\GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l}
\alert<5,6>{(2:3)+(7:7)}
& \onslide<7->{\to^{\only<-8>{\phantom{*}}\only<9->{\alert<9>{*}}}} &
\onslide<5->{\makebox[3cm][l]{$
\only<5>{\qquad
\alert{x \mapsto 2 \quad y \mapsto 3 \quad z \mapsto 7:7}}
\only<6>{\qquad
\alert{x \mapsto 2:3 \quad y \mapsto 7 \quad z \mapsto 7}}
\only<7,8>{\alert<7>{7:(\alert<8>{(2:3)+7})}}
\only<9,10>{7:(\alert<9>{2:(\alert<10>{3+7})})}
\only<11,12>{7:(\alert<12>{2:(\alert<11>{1:0})})}
\only<13,14>{7:(\alert<13>{(\alert<14>{2+1}):0})}
\only<15,16>{\alert<16>{7:(\alert<15>{3}:0)}}
\only<17,18>{\alert<17>{(\alert<18>{7+3}):0}}
\only<19,20>{(\alert<19>{1:0}):0}
$}}
\only<20->{\alert{\text{normal form}}}
\end{array}$}
}\only{%
\onslide<4->\alert<4-20>{rewriting} &
\GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l}
\alert<5,6>{(2:3)+(7:7)}
& \onslide<7->{\to^{\only<-8>{\phantom{*}}\only<9->{\alert<9>{*}}}} &
\onslide<5->{\makebox[3cm][l]{$
\only<19,20>{(\alert<19>{1:0}):0}
$}}
\onslide<20->{\alert{\text{normal form}}}
\end{array}$}
}
\end{tabular}
\end{example}

\end{frame}