← All problems
Unverified
Is the union of two totally terminating rewrite systems, which do not share any symbols, totally terminating?
The source page states the original problem together with its recorded qualifications and progress updates as follows.
When there exists a monotonic well-ordering (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 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 [Zantema, 1995]. What if variables are duplicated?
