\begin{frame}[t]
  \frametitle{Removing Redundant Reduction Rules}

  \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\\
  (5)&I(e)\cdot z&\to& z\\
  (6)& I(I(y))\cdot e &\to& y\\
  (7)& I(I(y))\cdot x &\to&  y\cdot x\\
  (8)&y\cdot e&\to& y\\
  (9)& I(I(y)) &\to& y
  \end{array}$
  \end{center}
  \end{block}
    
  \bigskip\pause
  Rule (7) is now no longer necessary:\pause
  \begin{center}
  $I(I(y))\cdot x \; \to_9 \;  y\cdot x$
  \end{center}\pause
  
  Likewise for rule (6):
  \begin{center}
  $I(I(y))\cdot e \; \to_{9}\; y\cdot e \; \to_{8}\; y$
  \end{center}
  
  \pause\vspace{-1ex}
  \begin{block}{}
  We remove the rules (6) and (7).
  \end{block}
\end{frame}