\begin{frame} \small \begin{example}[Non-confluence] \[ \begin{array}{llcl} \rho_1:& F(G(x),y) &\to&x\\ \rho_2:& G(a) &\to &b \end{array} \]\pause $\textcolor{blue}{F(G(a)},x) \to_{\rho_1} a$ $F(\textcolor{red}{G(a)},x) \to_{\rho_2} F(b,x)$\pause \smallskip The term $a$ and $F(b,x)$ are normal forms, without a common reduct. \end{example} \pause \begin{example}[Confluence] \[\begin{array}{llcl} \rho_1:& F(x,y) &\to&x\\ \rho_2:& G(a) &\to &b \end{array}\]\pause $\textcolor{blue}{F}(G(a),x) \textcolor{blue}{\to_{\rho_1}} G(a)$ $F(\textcolor{red}{G(a)},x) \textcolor{red}{\to_{\rho_2}} F(b,x)$\pause \smallskip Now $G(a)$ and $F(b,x)$ can both be further reduced to the common reduct $b$:\pause \smallskip $\textcolor{blue}{F}(\textcolor{red}{G(a)},x) \textcolor{blue}{\to_{\rho_1}} \textcolor{red}{G(a)} \textcolor{red}{\to_{\rho_2}} b$\pause $\textcolor{blue}{F}(\textcolor{red}{G(a)},x) \textcolor{red}{\to_{\rho_2}} \textcolor{blue}{F}(b,x) \textcolor{blue}{\to_{\rho_1}} b$ \end{example} \end{frame}