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

...

A set of

-- Goguen & Meseguer.

Unifying
Functional, Object-Oriented and Relational Programming with
Logical Semantics

. 1987