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