LP, the Larch Prover -- Confluence

A set of rewrite rules is called confluent (or Church-Rosser) if, whenever a term t can be rewritten in two ways to terms u and v, there is another term w such that u and v both rewrite to w. A set of rewrite rules is confluent if it is both terminating and locally confluent, i.e., if whenever a term t can be rewritten two ways, each in a single step, to terms u and v, there is another term w such that u and v both rewrite to w (Newman, 1942).