... apply the ...
rewrite rules
, progressively
transforming [the terms] until a 'reduced' or 'normal form' is
reached where no further rules are applicable.
...
A set of
rewrite rules
is said to be 'terminating' if
every sequence of rewrites on ground terms eventually reaches normal
form, and is said to be
Church-Rosser
if any two rewrite
sequences starting from the same term ... can always be further
rewritten in such a way that they reach equal values .... It is a
basic result of term-rewriting theory that if a system of rewrite
rules is Church-Rosser and terminating, then every term has a
unique
normal form.
-- Goguen & Meseguer.
Unifying
Functional, Object-Oriented and Relational Programming with
Logical Semantics
. 1987