\begin{frame}
  \frametitle{Efficient Completion}
  
  \begin{block}{Removal of Redundant Rules}
  In every step of the we are allowed to \alert{remove redundant rules from $R$}.
  \medskip
  
  That is, rules $\ell \to r \in R$ such that:
  $$\ell \to^*_{R'} r$$
  where $R' = R \setminus \{\ell \to r\}$.
  \end{block}
  
  \pause\bigskip
  \begin{block}{Observation}
  \begin{itemize}
  \item
  \makebox[4cm][l]{less rewrite rules}
  \makebox[5mm]{$\Longrightarrow$} \quad \alert{less critical pairs}
  \end{itemize}
  \end{block}
\end{frame}