 For instance, in Terese the Church-Rosser property and confluence are defined to be synonymous and identical to the definition of confluence presented here; Church-Rosser as defined here remains unnamed, but is given as an equivalent property; this departure from other texts is deliberate.Because of the above corollary, one may define a normal form "y" of "x" as an irreducible "y" with the property that formula_27.This definition, found in Book and Otto, is equivalent to the common one given here in a confluent system, but it is more inclusive in a non-confluent ARS.