Sharing Constructors Nachum Dershowitz

WADT'99

It is disconcerting that confluence is only modular for rewrite systems that do not even share constructors and that termination is only modular for disjoint confluent systems that are also left-linear. We present some new results/proofs regarding modularity of constructor-sharing combinations, including modularity of confluence (joint work with M. Fernandez and J.-P. Jouannaud) and modularity of left-linear convergence.