...
The conversion process always terminates (since each rewrite strictly
reduces the number of logical connectives in the expression) and yields
a unique answer independent of the order in which the rewrites are performed.
This property is called the Church-Rosser property, after the logicians
(Alonzo Church and Barkley Rosser) who invented the concept.
...