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