112/145
\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}