Termination for direct sums of left-linear complete term rewriting systems
Yoshihito Toyama, Jan Willem Klop, Hendrik Pieter Barendregt · Journal of the ACM · 1995
A term rewriting system is called complete if it is confluent and terminating.We prove that completeness of TRSS is a "modular" property (meaning that it stays preserved under direct sums), provided the constituent TRSS are left-linear.Here, the direct sum RO S3R ~is the union of TRSS R., RI with disjoint signature.The proof hinges crucially upon the (non)deterministic collapsing behavior of terms from the sum TRS.