\documentclass{rtaloop}
\rtalabel{completion-ordering}

\begin{document}
\begin{solvedproblem}{Nachum Dershowitz, L. Marcus}{}{April 1991}

\begin{abstract}
Can completion be incomplete when the ordering is changed en route?
\end{abstract}

Huet's proof \cite{H81:jcss} of the ``completeness'' of completion is
predicated on the assumption that the ordering supplied to completion does not
change during the process. Assume that at step $i$ of completion, the ordering
used is able to order the current rewriting relation $\rightarrow_{R_i}$, but
not necessarily $\rightarrow_{R_k}$ for $k<i$ (since old rules may have been
deleted by completion). Is there an example showing that completion is then
incomplete (the persisting rules are not confluent)?

\begin{remark}
The answer is yes, even when completion terminates with finitely many rules
 \cite{Sattler95}.
\end{remark}

\end{solvedproblem}
\end{document}