\begin{frame}
  \small
  
  \begin{example}
  \smallskip
  \[
  \GREEN{
  \begin{array}{rcl}
  \m{f}(\m{g}(x,\m{a},\m{b})) & \to & x \\
  \m{g}(\m{f}(\m{h}(\m{c},\m{d})),x,y) & \to & \m{h}(\m{k}(x),\m{k}(y)) \\
  \m{k}(\m{a}) & \to & \m{c} \\
  \m{k}(\m{b}) & \to & \m{d}
  \end{array}
  }
  \]
  \smallskip\pause
  
  The only critical pair is:
  $$
  \m{f}(\m{h}(\m{k}(\m{a}),\m{k}(\m{b}))) \quad\from\quad
  \m{f}(\m{g}(\m{f}(\m{h}(\m{c},\m{d})),\m{a},\m{b})) 
  \quad\to\quad \m{f}(\m{h}(\m{c},\m{d}))
  $$
  \pause
  Since $\atrs$ is left-linear and
  $\m{f}(\m{h}(\m{k}(\m{a}),\m{k}(\m{b}))) \parr \m{f}(\m{h}(\m{c},\m{d}))$,
  the system is confluent.
  \end{example}
\end{frame}