\begin{frame}
  \small
  
  \begin{block}{Confluence via Critical Pairs}
  \smallskip
  \alert<1>{Control interference} of rewrite rules:
  \begin{itemize}
  \item<2->
  Critical Pair Lemma (lecture 5): 
  
  \alert<2>{$\text{WCR} \quad\Longleftrightarrow\quad
  {\cp} \:\subseteq\: {\join}$} \quad (all critical pairs are convergent)
  \item<3->
  Combine with Newman's Lemma:
  
  \alert<3>{$\text{SN} \quad\&\quad {\cp} \:\subseteq\: {\join}
  \quad\Longrightarrow\quad \text{CR}$}
%   \item<4->
%   Observe from preceding examples:
%   
%   \alert<4>{
%   ${\cp} \:=\: \varnothing \quad\not\Longrightarrow\quad \text{CR}$}
  \smallskip
  \end{itemize}
  \end{block}
  
  \medskip
  \onslide<4->
  Observe from preceding examples:
  \begin{block}<4->{Confluence via Orthogonality}
  \smallskip
  \alert<4>{Forbid interference} of rewrite rules
  \begin{itemize}
  \item<5->
  \alert<5>{no critical pairs}
  \item<6->
  \alert<6>{no equality checks} (duplicated variables in the left-hand sides)
  \smallskip
  \end{itemize}
  \end{block}
\end{frame}