\begin{frame}[t]
  \small
  
  \vspace{-1ex}
  
  \begin{example}
  \vspace{-2.5ex}
  \GREEN{\begin{xalignat*}{4}
  \m{0} + y & \to y &
  \m{s}(x) + y &\to \m{s}(x+y) &
  \m{0} \times y &\to \m{0} &
  \m{s}(x) \times y &\to (x \times y) + y 
  \end{xalignat*}}
  \vspace{-5ex}
  \begin{center}
  \GREEN{\begin{tikzpicture}[on grid,baseline=(1).baseline]
  \small
  \matrix[ampersand replacement=\&,row sep=3mm,column sep=0mm]{
  \& \& \& \node(0) {$\phantom{0}$};
  \& \node (1) {$\makebox[0mm][r]{$\BLACK{t ~= \qquad}$}\alert<2>{+}$};
  \& \& \& \& \& \\
  \& \node (2) {$\alert<2>{\m{s}}$}; \& \& \& \& \&
  \& \node (3) {$+$}; \& \& \& \\
  \& \node (4) {$\alert<3>{\times}$}; \& \& \&
  \& \node (5) {$\alert<5>{\times}$}; \&
  \& \& \& \node (6) {$\alert<4>{+}$}; \& \\
  \node (7) {$\alert<3>{0}$}; \& \& \node (8) {$0$}; \&
  \& \node (9) {$\alert<5>{0}$};
  \& \& \node (10) {$\alert<6>{+}$}; \& \& \node (11) {$\alert<4>{0}$}; \&
  \& \node (12) {$\m{s}$}; \\
  \& \& \& \& \& \node (13) {$\alert<6>{0}$}; \& \& \node (14) {$\m{s}$};
  \& \& \& \node (15) {$0$}; \\
  \& \& \& \& \& \& \& \node (16) {$0$}; \& \& \& \\ };
  \alert<2>{
  \draw (1) node[right] {\BLACK{\alert<2>{$\,{}^\epsilon$}}} -- (2);
  \draw (1) -- (3);
  \draw (2) -- (4);
  }
  \draw (3) -- (5);
  \draw (3) -- (6);
  \alert<3>{
  \draw (4) node[left] {\BLACK{\alert<3>{${}^{11}\,$}}} -- (7);
  \draw (4) -- (8);      
  }
  \alert<5>{
  \draw (5) node[left] {\BLACK{\alert<5>{${}^{21}\,$}}} -- (9);
  \draw (5) -- (10);
  }
  \alert<4>{
  \draw (6) node[right] {\BLACK{\alert<4>{$\,{}^{22}$}}} -- (11);
  \draw (6) -- (12);                                         
  }
  \alert<6>{
  \draw (10) node[right] {\BLACK{\alert<6>{$\,{}^{212}$}}} -- (13);
  \draw (10) -- (14);
  }
  \draw (12) -- (15);
  \draw (14) -- (16);
  \end{tikzpicture}
  $\stackrel{\BLACK{\alert<1>{21}}}{\longrightarrow}$
  \begin{tikzpicture}[on grid,baseline=(1).baseline]
  \small
  \matrix[ampersand replacement=\&,row sep=3mm,column sep=0mm]{
  \& \& \& \node (1) {$\alert<2>{+}\makebox[0mm][l]{$\BLACK{\qquad =~ u}$}$};
  \& \& \& \& \\
  \& \node (2) {$\alert<2>{\m{s}}$}; \& \& \&
  \& \node (3) {$\alert<7>{+}$}; \& \& \\
  \& \node (4) {$\alert<3>{\times}$}; \& \&
  \& \node (5) {$\alert<7>{0}$}; \& \& \node (6) {$\alert<4>{+}$}; \& \\
  \node (7) {$\alert<3>{0}$}; \& \& \node (8) {$0$}; \& \& \&
  \node (9) {$\alert<4>{0}$}; \& \& \node (10) {$\m{s}$}; \\
  \& \& \& \& \& \& \& \node (11) {$0$}; \\ };
  \alert<2>{
  \draw (1) node[right] {\BLACK{\alert<2>{$\,{}^\epsilon$}}} -- (2);
  \draw (1) -- (3);
  \draw (2) -- (4);
  }
  \alert<7>{
  \draw (3) node[right] {\BLACK{\alert<7>{$\,{}^2$}}} -- (5);
  \draw (3) -- (6);
  }
  \alert<3>{
  \draw (4) node[left]  {\BLACK{\alert<3>{${}^{11}\,$}}} -- (7);
  \draw (4) -- (8);                                             
  }
  \alert<4>{
  \draw (6) node[right] {\BLACK{\alert<4>{$\,{}^{22}$}}} -- (9);
  \draw (6) -- (10);
  }
  \draw (10) -- (11);
  \end{tikzpicture}}
  \end{center}
  \vspace{-2ex}
  \(
  \begin{array}{@{}l@{\hspace{3.2mm}}c|c|c|c|c|c|c}
  \text{redex positions in $s$\,:} & \epsilon & 11 & 2 &
  \multicolumn{2}{c|}{22} \\
  \text{redex positions in $t$\,:} & \alert<2>{\epsilon} &
  \alert<3>{11} & \phantom{2} & \alert<6>{212} & \alert<4>{22} &
  \alert<5>{21} \onslide<2-> \\
  \text{redex positions in $u$\,:} &
  \onslide<2->\alert<2>{\epsilon} & \onslide<3->\alert<3>{11} & & &
  \onslide<4->\alert<4>{22} & & \onslide<7->\alert<7>{2}
  \end{array}
  \)
  \\[2ex]
  \begin{center}
  \onslide<6->
  redex at position $212$ is \alert<6>{erased} \qquad\qquad
  \onslide<7->
  redex at position $2$ is \alert<7>{created}
  \end{center}
  \end{example}
\end{frame}