\begin{frame}
  \small
  
  \vspace{-1ex}
  
  \begin{definition}[Parallel Rewriting]
  \begin{enumerate}
  \item ~
  $\makebox[4mm][l]{${=}$} \subseteq \alert<1-3>{\parr}$
  \vspace{-.5ex}
  \item<2-> ~
  $\makebox[4mm][l]{$\xrightarrow{\epsilon}$} \subseteq \alert<2-3>{\parr}$
  \vspace{-.5ex}
  \item<3-> ~
  $f(\seq{s}) \alert<3>{\parr} f(\seq{t})$ if $s_i \parr t_i$ for each
  $1 \leqslant i \leqslant n$
  \end{enumerate}
  \end{definition}
  
  \begin{example}<4->
  \vspace{-3ex}
  \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{-6.5ex}
  \begin{center}
  \GREEN{\begin{tikzpicture}[on grid,baseline=(1).baseline]
  \small
  \matrix[ampersand replacement=\&,row sep=2.1mm,column sep=1mm,inner sep=.5mm]{
  \& \& \& \node (1) {$\makebox[0mm][r]{$\BLACK{s ~= \qquad}$}{+}$};
  \& \& \& \& \\
  \& \node (2) {${\m{s}}$}; \& \& \&
  \& \node (3) {$\alert<4->{\times}$}; \& \& \\
  \& \node (4) {$\alert<4->{\times}$}; \& \&
  \& \node (5) {$\alert<4->{\m{s}}$}; \& \& \node (6) {${+}$}; \& \\
  \node (7) {$\alert<4->{0}$}; \& \& \node (8) {$0$}; \& \& \node (9) {$0$};
  \& \node (10) {${0}$}; \& \& \node (11) {${\m{s}}$}; \\
  \& \& \& \& \& \& \& \node (12) {$0$}; \\ };
  \draw (1) node[right] {} -- (2);
  \draw (1) -- (3);
  \draw (2) -- (4);
  \alert<4->{
  \draw (3) node[right] {} -- (5);
  \draw (3) -- (6);
  \draw (5) -- (9);
  }
  \alert<4->{
  \draw (4) node[left] {} -- (7);
  }
  \draw (4) -- (8);
  \draw (6) node[right] {} -- (10);
  \draw (6) -- (11);
  \draw (11) -- (12);
  \end{tikzpicture}
  \onslide<5->{
  \raisebox{-1mm}{$\alert<5>{\parr}$}
  \begin{tikzpicture}[on grid,baseline=(1).baseline]
  \small
  \matrix[ampersand replacement=\&,row sep=2.1mm,column sep=1mm,inner sep=.5mm]{
  \& \& \& \node(0) {$\phantom{0}$};
  \& \node (1) {${+}\makebox[0mm][l]{$\BLACK{\qquad =~ t}$}$};
  \& \& \& \& \& \\
  \& \node (2) {${\m{s}}$}; \& \& \& \& \& \& \node (3) {$+$};
  \& \& \& \\
  \& \node (4) {$0$}; \& \& \& \&
  \node (5) {$\times$};
  \& \& \& \& \node (6) {${+}$}; \& \\
  \node (7) {}; \& \& \node (8) {}; \&
  \& \node (9) {${0}$}; \& \& \node (10) {${+}$}; \&
  \& \node (11) {${0}$}; \& \& \node (12) {$\m{s}$}; \\
  \& \& \& \& \& \node (13) {${0}$}; \& \& \node (14) {$\m{s}$};
  \& \& \& \node (15) {$0$}; \\
  \& \& \& \& \& \& \& \node (16) {$0$}; \& \& \& \\ };
  \draw (1) node[right] {} -- (2);
  \draw (1) -- (3);
  \draw (2) -- (4);
  \draw (3) -- (5);
  \draw (3) -- (6);
  \draw (5) node[left] {} -- (9);
  \draw (5) -- (10);
  \draw (6) node[right] {} -- (11);
  \draw (6) -- (12);
  \draw (10) node[right] {} -- (13);
  \draw (10) -- (14);
  \draw (12) -- (15);
  \draw (14) -- (16);
  \end{tikzpicture}}}
  \end{center}
  \vspace{-3ex}
  \end{example}

  \begin{lemma}<6->
  $s \parr t$
  \quad$\iff$\quad
  $s \to^* t$ by contracting redexes at pairwise parallel positions in $s$
  \end{lemma}
\end{frame}