\documentclass{rtaloop}
\rtalabel{unicity}

\begin{document}
\begin{solvedproblem}{Aart Middeldorp}{\cite{M90:vrije}}{April 1991}

\begin{abstract}
Is unicity of normal forms a modular property of standard conditional systems?
\end{abstract}


A conditional term-rewriting system has rules of the form $p \Rightarrow l
\rightarrow r$, which are only applied to instances of $l$ for which the
condition $p$ holds. A ``standard'' (or ``join'') conditional system is one in
which the condition $p$ is a conjunction of conditions $u \downarrow v$,
meaning that $u$ and $v$ have a common reduct (are ``joinable''). Is unicity
of normal forms (UN) a modular property of standard conditional systems? See
also \cite{Mid93}.

\begin{remark}
This has been answered in the negative by giving a
counterexample \cite{scheffermann:pr309}.
\end{remark}

\end{solvedproblem}
\end{document}