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