Rewrite closure

In theoretical computer science, in particular in automated theorem proving and term rewriting, a binary relation (→) on the set of terms is called a rewrite relation if it is closed under contextual embedding and under instantiation; formally: if l→r implies u[lσ]_p→u[rσ]_p for all terms l, r, u, each path p of u, and each substitution σ. If (→) is also irreflexive and transitive, then it is called a rewrite ordering, or rewrite preorder. If the latter (→) is moreover well-founded, it is called a reduction ordering, or a reduction preorder. Given a binary relation R, its rewrite closure is the smallest rewrite relation containing R. A transitive and reflexive rewrite relation that contains the subterm ordering is called a simplification ordering.

Nachum Dershowitz; Jean-Pierre Jouannaud (1990). Jan van Leeuwen, ed. Rewrite Systems. Handbook of Theoretical Computer Science. B. Elsevier. pp. 243–320. 

...
Wikipedia