\begin{frame}<1-3>[label=relationships]
\small
\settowidth{\xx}{$\Longleftarrow$}%
\begin{block}{Lemmata}
\begin{enumerate}[<+->]
\item
\makebox[8mm][r]{SN}
\quad$\Longrightarrow$\quad
\makebox[3cm][l]{WN}
\item
\makebox[8mm][r]{SN}
\quad$\mathrel{\makebox[0cm][l]{$\Longleftarrow$}%
\raisebox{-.5pt}{\makebox[\xx]{\alert{\Large $\,\times$}}}}$\quad
\makebox[3cm][l]{WN}
\onslide<3->
\smash{\GREEN{\begin{tikzpicture}[on grid,baseline=-.5ex]
\node (1) {$\e{\m{a}}$};
\node (2) [right=of 1] {$\e{\m{b}}$};
\draw[->] (1) edge[out=205,in=155,loop] ();
\draw[->] (1) edge (2);
\end{tikzpicture}}}
\smallskip
\item<4->
\onslide<9->{\alert<9>{\makebox[8mm][r]{CR}
\quad$\Longrightarrow$\quad}}
\makebox[8mm][l]{NF}
$\Longrightarrow$\quad
\makebox[8mm][l]{\UN}
$\Longrightarrow$\quad
\makebox[8mm][l]{\UNrew}
\smallskip
\item<5->
\makebox[8mm][r]{\UN}
\quad$\mathrel{\makebox[0cm][l]{$\Longleftarrow$}%
\raisebox{-.5pt}{\makebox[\xx]{\alert{\Large $\,\times$}}}}$\quad
\makebox[3cm][l]{\UNrew}
\onslide<6->
\smash{\GREEN{\begin{tikzpicture}[on grid,baseline=-0.5ex,node distance=9mm]
\node (1) {$\e{\m{a}}$};
\node (2) [right=of 1,yshift=2mm] {$\e{\m{b}}$};
\node (3) [right=of 2,yshift=-2mm,inner sep=.1mm] {$\e{\m{c}}$};
\node (4) [right=of 3,yshift=2mm] {$\e{\m{d}}$};
\node (5) [right=of 4,yshift=-2mm] {$\e{\m{e}}$};
\draw[->] (3) edge[out=65,in=115,looseness=4] (3);
\draw[->] (2) edge (1);
\draw[->,shorten >= 1mm] (2) edge (3);
\draw[->,shorten >= 1mm] (4) edge (3);
\draw[->] (4) edge (5);
\end{tikzpicture}}}
\smallskip
\item<7->
\makebox[8mm][r]{NF}
\quad$\mathrel{\makebox[0cm][l]{$\Longleftarrow$}%
\raisebox{-.5pt}{\makebox[\xx]{\alert{\Large $\,\times$}}}}$\quad
\makebox[3cm][l]{\UN}
\onslide<8->
\smash{\GREEN{\begin{tikzpicture}[on grid,baseline=-0.5ex]
\node (1) {$\e{\m{a}}$};
\node (2) [right=of 1] {$\e{\m{b}}$};
\node (3) [right=of 2] {$\e{\m{c}}$};
\draw[->] (1) edge[out=205,in=155,loop] ();
\draw[->] (2) edge (1);
\draw[->] (2) edge (3);
\end{tikzpicture}}}
\smallskip
\item<10->
\makebox[8mm][r]{CR}
\quad$\mathrel{\makebox[0cm][l]{$\Longleftarrow$}%
\raisebox{-.5pt}{\makebox[\xx]{\alert{\Large $\,\times$}}}}$\quad
\makebox[3cm][l]{NF}
\onslide<11->
\smash{\GREEN{\begin{tikzpicture}[on grid,baseline=-0.5ex]
\node (1) {$\e{\m{a}}$};
\node (2) [right=of 1] {$\e{\m{b}}$};
\node (3) [right=of 2] {$\e{\m{c}}$};
\draw[->] (1) edge[out=205,in=155,loop] ();
\draw[->] (2) edge (1);
\draw[->] (2) edge (3);
\draw[->] (3) edge[out=-25,in=25,loop] ();
\end{tikzpicture}}}
\smallskip
\item<12->
\makebox[8mm][r]{CR}
\quad$\Longleftrightarrow$\quad
${\conv} \:\subseteq\: {\join}$
\onslide<13->
\quad$\Longleftrightarrow$\quad
${\conv} \:=\: {\join}$
\quad$\Longleftrightarrow$\quad
${\leftarrow \cdot \to^*} \:\subseteq\: {\join}$
\smallskip
\item<14->
\makebox[8mm][r]{WN} ~\&\: \makebox[7mm][l]{UN$^\to$}
\quad$\Longrightarrow$\quad
\makebox[3cm][l]{CR}
\smallskip
\item<15->
\makebox[8mm][r]{CR}
\quad$\Longrightarrow$\quad
\makebox[3cm][l]{WCR}
\smallskip
\item<16->
\makebox[8mm][r]{CR}
\quad$\mathrel{\makebox[0cm][l]{$\Longleftarrow$}%
\raisebox{-.5pt}{\makebox[\xx]{\alert{\Large $\,\times$}}}}$\quad
\makebox[3cm][l]{WCR}
\onslide<17->
\smash{\GREEN{\begin{tikzpicture}[on grid,baseline=-0.5ex]
\node (1) {$\e{\m{a}}$};
\node (2) [right=of 1] {$\e{\m{b}}$};
\node (3) [right=of 2] {$\e{\m{c}}$};
\node (4) [right=of 3] {$\e{\m{d}}$};
\draw[->] (2) edge (1);
\draw[->] (2) edge[bend left] (3);
\draw[->] (3) edge[bend left] (2);
\draw[->] (3) edge (4);
\end{tikzpicture}}}
\smallskip
\item<18->
\makebox[8mm][r]{SN} ~\&\: \makebox[7mm][l]{WCR}
\quad$\Longrightarrow$\quad
\makebox[17mm][l]{CR}
\onslide<19->
\alert{Newman's Lemma}
\smallskip
\end{enumerate}
\end{block}
\end{frame}
\mode{
\againframe{UN}
\againframe<4-8>{relationships}
\againframe{CR}
\againframe{CReq}
\againframe{CReq:proof1}
\input{../induction}
\againframe{CReq:proof2}
\againframe{CReq2}
\againframe{CReq2:proof}
\againframe<9-14>{relationships}
\againframe{WCR}
\againframe<15->{relationships}
}