Modularity of termination and confluence in combinations of rewrite systems with

Abstract

We prove that termination and confluence are modular properties in combinations of the typed) λ-calculus of order ω with (first or higher order) term rewrite systems, provided that the first order rewrite system is conservative (non-duplicating) aald the higher order rewrite system satisfies some suitable condi[ions (the general schema) and does not introduce critical pairs.