We assume familiarity with basic notions of term rewriting
[DJ90] and functional logic programming
[Han94].
We consider a signature 
partitioned into a set
of constructors and a set 
of (defined)
functions or operations.
operation
The set of
terms and constructor terms with variables
(e.g., x,y,z) from 
are denoted by 
and 
, respectively.
We write 
for the list of objects
.
The set of variables occurring in a term t is denoted by 
.
A term is linear if it does not contain multiple occurrences
of one variable. root(t) denotes the symbol at the root of the term t.
If 
( 
), the term t is said
operation-rooted (constructor-rooted).
A pattern is a linear term of the form 
where 
is n-ary and 
.
A position p in a term t is represented by a sequence of
natural numbers ( 
denotes the empty sequence, i.e., the
root position). 
denotes the set of
positions of t.
Positions are ordered by the prefix ordering: 
, if there
exists p' such that p.p' =q.
denotes the subterm of t at position
p, and 
denotes the result of
replacing by the term s
(see [DJ90] for details).
is the set of positions of operation-rooted subterms of t.
We denote by 
the
substitution 
with
for 
(with 
if 
), and 
for all other variables x.
The identity substitution is denoted by id.
Substitutions are extended to morphisms on terms by
for every term 
.
Given terms t,s, we write 
if 
and say that t is a prefix of s (said strict if t<s).
A unifier of two terms s and t
is a substitution with 
.
A set of rewrite rules 
such that 
,
, and
is called a term rewriting system
(TRS). The terms
l and r are called the left-hand side (lhs) and the
right-hand side (rhs) of the rule,
respectively.
A TRS 
is left-linear if l is linear for all 
.
A TRS is constructor based (CB) if each lhs l is a pattern.
Two (possibly renamed) rules and 
overlap,
if there is a non-variable
position 
and a most-general unifier such that
. The pair
is called a critical
pair.
A left-linear TRS without critical pairs is
called orthogonal.
A rewrite step is an application of a rewrite rule to a term, i.e.,
if there exists 
,
a rewrite rule 
and a substitution
with 
and 
.
The instantiated lhs 
is called a redex.
To evaluate terms containing variables, narrowing
non-deterministically
instantiates the variables such that a rewrite step is possible. Formally,
is a narrowing step
if p is a non-variable position in t and 
.
We denote by 
a sequence of narrowing
steps 
with 
.