This is known as algebraic inconsistency . Other names for this property are diamond and amalgamation . What we prove in practice is local confluence , that any two one- step reductions may be brought back together. If it only takes one step on each side to do this then the following result still holds. Usually more than one step is needed, so the paths to be reconciled may just get longer.
Confluence is a property of the presentation of a system of rules.
In particular for each term there is at most one irreducible form to which it is equivalent, and distinct irreducible forms are inequivalent, so we call them normal . A sequence of soldiers, which we write with semi-colons between them, is called a parade if each can see only those facing in the same direction and of the same or lower rank. Since the total rank decreases, any conflict of forces terminates, and the result is a parade. The term-rewriting approach would show that the reduction rules are confluent. In fact exactly the same calculations are needed either way, and we deduce that any conflict has a foregone conclusion.