\begin{frame}
  \small
  
  \begin{block}{Confluence}
  \vspace{-3ex}
  \[
  \begin{tikzpicture}[on grid,baseline=(1).baseline,node distance=15mm]
  \node (0) {\alert<1>{\raisebox{-5ex}{%
  every two coinitial rewrite sequences can be joined}}};
  \node (1) [below=of 0]       {$\cdot$};
  \node (2) [below left=of 1]  {$\cdot$};
  \node (3) [below right=of 1] {$\cdot$};
  \node (4) [below right=of 2] {$\cdot$};
  \draw[->>] (1) -- (2);
  \draw[->>] (1) -- (3);
  \draw[dotted,->>] (2) -- (4);
  \draw[dotted,->>] (3) -- (4);
  \path (1) -- (4) node[midway] {CR};
  \end{tikzpicture}
  \]
  \begin{itemize}
  \item<2->~
  \dots~ yields uniqueness of normal forms
  \item<3->~
  \dots~ is decidable for terminating TRSs
  \item<4->~
  \dots~ what about nonterminating TRSs ?
  \smallskip
  \end{itemize}
  \end{block}
\end{frame}