\begin{frame}
  \small
  
  \begin{example}
  \[
  \GREEN{\begin{array}{r@{~}c@{~}l@{\qquad}r@{~}c@{~}l@{\qquad}r@{~}c@{~}l}
  \alert<2>{\m{e} \cdot x} & \to & x &
  \alert<3>{x^- \cdot x} & \to & \m{e} &
  \alert<4>{\alert<2-3>{(x \cdot y)} \cdot z} & \to & x \cdot (y \cdot z)
  \end{array}}
  \]
  \onslide<2->
  overlaps
  \begin{itemize}
  \item
  $\langle\,
  \GREEN{\m{e} \cdot x \to x},
  \,1,\,
  \GREEN{(x \cdot y) \cdot z \to x \cdot (y \cdot z)}
  \,\rangle$
  \item<3->
  $\langle\,
  \GREEN{x^- \cdot x \to \m{e}},
  \,1,\,
  \GREEN{(x \cdot y) \cdot z \to x \cdot (y \cdot z)}
  \,\rangle$
  \item<4->
  $\langle\,
  \GREEN{(x \cdot y) \cdot z \to x \cdot (y \cdot z)},
  \,1,\,
  \GREEN{(x \cdot y) \cdot z \to x \cdot (y \cdot z)}
  \,\rangle$
  \end{itemize}
  \onslide<5->
  critical pairs
  \begin{itemize}
  \item<6->
  \makebox[9cm][l]{$\GREEN{y \cdot z} \leftarrow (\m{e} \cdot y) \cdot z \rightarrow \GREEN{\m{e} \cdot (y \cdot z)}$}
  \onslide<9->{convergent}
  \item<7->
  \makebox[9cm][l]{$\GREEN{\m{e} \cdot z} \leftarrow (x^- \cdot x) \cdot z \rightarrow \GREEN{x^- \cdot (x \cdot z)}$}
  \onslide<10->{\makebox[0mm][r]{\alert{not} }convergent}
  \item<8->
  \makebox[9cm][l]{$\GREEN{(u \cdot (v \cdot w)) \cdot z} \leftarrow ((u \cdot v) \cdot w) \cdot z\rightarrow
  \GREEN{(u \cdot v) \cdot (w \cdot z)}$}
  \onslide<11->{convergent}
  \end{itemize}
  \end{example}
  
  \smallskip
  
  \begin{block}<12->{Theorem (Knuth \& Bendix 1970)}
  \smallskip
  A \alert{terminating} TRS is confluent \quad$\iff$\quad
  all critical pairs are convergent.
  %$\text{\alert<2>{SN}} \quad\Longrightarrow\quad
  %\left[\:{\cp} \:\subseteq\: {\join}
  %\quad\iff\quad \text{CR}\:\right]$
  \end{block}
\end{frame}