\begin{frame} \small \vspace{-1ex} \begin{definition}[Projection] \smallskip \( \begin{array}{@{}r@{\colon~}r@{\:\parr\:}ll} A & s & t_1 & \text{by contracting redexes at positions in $P_A$} \\[1ex] B & s & t_2 & \text{by contracting redexes at positions in $P_B$} \end{array} \) \smallskip \begin{itemize} \item<2-> $\alert<2>{B \project A}\colon~ t_1 \parr u_1$ by contracting redexes at positions in $P_B \project A$ \item<3-> $\alert<3>{A \project B}\colon~ t_2 \parr u_2$ by contracting redexes at positions in $P_A \project B$ \item<4-> $\alert<4>{A \sqcup B} = A; B \project A$ and $\alert<4>{B \sqcup A} = B; A \project B$ \end{itemize} \end{definition} \begin{block}<5->{Parallel Moves Lemma} For every orthogonal TRS:\vspace{-2ex} \begin{center} \begin{tikzpicture}[on grid,baseline=(1).baseline] \node (1) {$\strut s$}; \node (c) [below=of 1] {}; \node (2) [left=of c] {$t_1$}; \node (3) [right=of c] {$t_2$}; \draw[->] (1) -- (2) node[midway,sloped] {$\|$}; \draw[->] (1) -- (3) node[midway,sloped] {$\|$}; \node (6) at (-1.0,-0.25) {$A$}; \node (7) at (1.0,-0.25) {$B$}; \alt<6->{ \node (4) [below=of c] {$\strut u$}; \draw[->] (2) -- (4) node[midway,sloped] {$\|$}; \draw[->] (3) -- (4) node[midway,sloped] {$\|$}; \node (8) at (-1.25,-2.25) {$B \project A$}; \node (9) at (1.25,-2.25) {$A \project B$}; }{ \node (4a) [below=of 2] {$\strut u_1$}; \node (4b) [below=of 3] {$\strut u_2$}; \draw[->] (2) -- (4a) node[midway,sloped] {$\|$} node[midway,left] {$B \project A~~$}; \draw[->] (3) -- (4b) node[midway,sloped] {$\|$} node[midway,right] {$~~A \project B$}; \node (d) [below=of c] {\alert{?}}; } \onslide<7->{ \draw[->,thick,red] (1) .. controls (-4,0) and (-4,-2.5) .. (4); \draw[->,thick,red] (1) .. controls (4,0) and (4,-2.5) .. (4); \node at (-4,-1.25) {$\alert{A \sqcup B}$}; \node at (4,-1.25) {$\alert{B \sqcup A}$}; } \end{tikzpicture} \end{center} \end{block} \end{frame}