Term rewriting systems are reduction systems in which rewrite rules apply to terms. Terms are built up
from variables and constants using function symbols (or operations). Rules of term
rewriting systems have the form 
, where both 
and 
are terms, 
is not a variable, and every variable from 
occurs in 
as well.
A reduction step for term 
is defined as follows. If 
is a unifier for 
and 
, then 
is reduced to 
. If 
is a unifier for 
and 
where 
is a subterm of 
, then 
is reduced to a term obtained from 
by replacing 
with 
.
