\begin{frame}[t]
\small

\vspace{-1ex}

\begin{block}{Newman's Lemma}
\smallskip
$\text{SN}(\AA) ~\&~ \text{WCR}(\AA) \quad\Longrightarrow\quad
\text{CR}(\AA)$
\end{block}

\smallskip

\begin{proof}

\begin{tabular}{ll}
\tikzstyle{element}=[circle,text width=4.5pt,text height=4.5pt]
\begin{tikzpicture}
\alert<2>{
\node at (2,4) [element] (a)  {}; \node at (a)  {$a$};
}
\alert<2,4>{
\node at (1,3) [element] (b1) {}; \node at (b1) {$b_1$};
}
\alert<2,6-8>{
\node at (3,3) [element] (c1) {}; \node at (c1) {$c_1$};
}
\alert<2>{
\draw [->] (a) to (b1);
\draw [->] (a) to (c1);
}
\alert<4>{
\node at (0,2) [element] (b)  {}; \node at (b)  {$b$};
}
\alert<8>{
\node at (4,2) [element] (c)  {}; \node at (c)  {$c$};
}
\alert<4>{
\draw [->>] (b1) to (b);
}
\alert<8>{
\draw [->>] (c1) to (c);
}
\onslide<3->{\alert<3>{
\node at (2,3) {WCR};
}
\alert<3,4,6>{
\node at (2,2) [element] (d1) {}; \node at (d1) {$d_1$};
}
\alert<3,4>{
\draw [->>] (b1) to (d1);
}
\alert<3,6>{
\draw [->>] (c1) to (d1);
}}
\onslide<5->{\alert<5>{
\node at (1,2) {\makebox[0mm]{IH}};
}
\alert<5,6-8>{
\node at (1,1) [element] (d2) {}; \node at (d2) {$d_2$};
}
\alert<5,6>{
\draw [->>] (d1) to (d2);
}
\alert<5>{
\draw [->>] (b)  to (d2);
}}
\onslide<7->{\alert<7,8>{
\draw [bl,->>] (c1)  to (d2);
}}
\onslide<9->{\alert<9>{
\node at (2,0) [element] (d3) {}; \node at (d3) {$d_3$};
\draw [->>] (d2) to (d3);
\draw [->>] (c)  to (d3);
\node at (2.5,1.5) {\makebox[0mm]{IH}};
}}
\end{tikzpicture}
&
\onslide<5->{\raisebox{14ex}{
\begin{tabular}{l}
\alert<5>{induction hypothesis \qquad\qquad
\only{\only<5>{CR($b_1$)}\only<9>{\alert<9>{CR($c_1$)}}}
\only{\hspace{-1cm} CR($b_1$) \& CR($c_1$)}} \\[.5ex]

$\forall a'\colon$ if $a \to a'$ then CR($a'$)
\end{tabular}
}}
\end{tabular}
\end{proof}

\end{frame}