Unique normal forms for disjoint unions of conditional term rewriting systems
Aart Middeldorp · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1990
Abstract: "In [14] we have shown that every term rewriting system with the unique normal form property can be conservatively extended to a confluent term rewriting system with the same set of normal forms. This paper gives a simplified construction, which moreover yields a positive answer to a conjecture in [14] stating that the normal form property is a modular property of left-linear term rewriting systems. We further show that the main result of [14] -- the modularity of unique normal forms -- can be generalized to semi-equational conditional term rewriting systems; however, for join and normal conditional term rewriting systems the method of [14] fails."