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