\begin{frame}
  \small
  
  \begin{definition}
  \smallskip
  $A\colon s_1 \to^* t_1$ and $B\colon s_2 \to^* t_2$
  are \alert{permutation equivalent} ($\alert<2>{A \simeq B}$) if
  \begin{enumerate}
  \item ~
  $s_1 = s_2$
  \vspace{-1ex}
  \item ~
  $t_1 = t_2$
  \vspace{-1ex}
  \item ~
  $p \project A = p \project B$ for all redex positions $p$ in $s_1$
  \end{enumerate}
  \end{definition}

%   \pause
%   \begin{definition}
%   $A\colon s \to^* t_1$ and $B\colon s \to^* t_2$ are \alert{permutation equivalent} ($\alert{A \simeq B}$)if \
%   $$ A \project B = \varnothing \text{ and } B \project A = \varnothing$$
%   \end{definition}

  \pause
  \begin{block}{Parallel Moves Lemma (with Permutation Equivalence)}
  \vspace{-1.5ex}
  \begin{center}
  \begin{tikzpicture}[on grid,baseline=(1).baseline]
  \node (1)              {$\strut s$};
  \onslide<3->{
  \node (c) [below=of 1] {$\alert<3>{\simeq}$};
  }
  \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$};
  \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$};
  \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}
  \vspace{-3ex}
  \end{block}
\end{frame}