Which is the coarsest relation such that its union with any rewrite relation preserves termination?
The source page states the original problem together with its recorded qualifications and progress updates as follows.
Any rewrite relation commutes with the strict-subterm relation; hence, the union of the latter with an arbitrary terminating rewrite relation is terminating, and also fully invariant (closed under instantiation). Which is the coarsest (maximal) relation with these properties? (A relation is said to be coarser than a relation if implies ).
The answer is not the subterm relation''. Is *encompassment* (containment'', the combination of subterm and subsumption) the coarsest
relation which preserves termination (without full invariance)?
Recorded progress.
The coarsest relation we know of which could answer the first question is the variant of subterm that allows multiple occurrences of variables to be renamed apart.
