\begin{frame}
  \frametitle{Finally!}
  
  We have constructed a complete rewrite system:
  \begin{itemize}
    \item all critical pairs are convergent
    \item the system is terminating
  \end{itemize}
  \bigskip
  
  \begin{block}{}
  \begin{center}
  $\begin{array}{llcl}
  (1)&e\cdot x&\to&x\\
  (2)&I(x)\cdot x&\to&e\\
  (3)&(x\cdot y)\cdot z &\to& x\cdot (y\cdot z)\\
  (4)&I(x)\cdot (x\cdot z)&\to& z\\
  (8)&y\cdot e&\to& y\\
  (9)& I(I(y)) &\to& y\\
  (10)&I(e)&\to& e\\
  (11)&y\cdot I(y)&\to& e\\
  (12)&y\cdot (I(y) \cdot x) &\to& x\\
  (15)& I(x\cdot y)  &\to&   I(y)\cdot I(x)
  \end{array}$
  \end{center}
  \end{block}
\end{frame}