\documentclass{rtaloop}
\rtalabel{total-termination}


\begin{document}
\begin{problem}{Hans Zantema}{}{April 1995}
\begin{abstract}
  Is the union of two totally terminating rewrite systems, which do
  not share any symbols, totally terminating?
\end{abstract}
When there exists a monotonic well-ordering (\emph{monotonic} means
that replacing a subterm with a smaller one decreases the whole term)
of ground terms that shows termination of a rewrite system, the system
is called \emph{totally terminating}.  The union of two totally
terminating rewrite systems which do not share any symbols is totally
terminating if at least one of them does not contain a rule that has
more occurrences of some variable on the right than on the left
\cite{FZ93,FZ96}.  What if variables are duplicated?
\end{problem}
\end{document}