\documentclass{rtaloop}
\rtalabel{UNarrow}

\begin{document}
\begin{solvedproblem}{Aart Middeldorp}{\cite{M89:rta}}{April 1991}

\begin{abstract}
Is \emph{unicity of normal forms with respect to reduction} a
modular property of left-linear term-rewriting systems?
\end{abstract}

If $R$ and $S$ are two term-rewriting systems with disjoint vocabularies, such
that for each of $R$ and $S$ any two convertible normal forms must be
identical, then their union $R \cup S$ also enjoys this property
\cite{M89:rta}. Accordingly, we say that unicity of normal forms (UN) is a
``modular'' property of term-rewriting systems. ``Unicity of normal forms with
respect to reduction'' (UN$^\rightarrow$) is the weaker property that any two
normal forms of the same term must be identical. For non-left-linear systems,
this property is not modular. The question remains: Is $UN^\rightarrow$ a
modular property of left-linear term-rewriting systems?

\begin{remark}
A positive solution is given in \cite{Mar93}.
\end{remark}

\end{solvedproblem}
\end{document}