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