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