Abstract

We prove a conjecture by Rusinowitch stating that the direct sum of two terminating term rewriting systems is terminating if one of the systems contains neither collapsing nor duplicating rules.

BibTeX Entry

@inproceedings{M-LICS89,
 author    = "Aart Middeldorp",
 title     = "A Sufficient Condition for the Termination of the Direct Sum
              of Term Rewriting Systems",
 booktitle = "Proceedings of the 4th Annual Symposium on Logic in Computer
              Science",
 pages     = "396--401",
 publisher = "IEEE Press",
 year      = 1989,
 doi       = "10.1109/LICS.1989.39194"
}