rewrite rules

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