\documentclass{rtaloop}
\rtalabel{union-orderings}


\begin{document}
\begin{problem}{Jean-Pierre Jouannaud}{}{April 1995}

\begin{abstract}
Extend combination results on rewrite orderings to systems involving
$\beta\eta$ reductions.
\end{abstract}

A collection of rewrite orderings operating on disjoint signatures can
be extended to an ordering operating on the union of the signatures,
while still preserving part of the properties \cite{Rubio94}. Such
constructions can be used for proving modular termination properties
of rewrite systems.  Do they extend to the case where one of the
starting orderings is given by $\beta\eta$ reductions on typed lambda
terms?
\end{problem}
\end{document}