# 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).