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