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