Definitional trees are used to guide the search
for a redex within the computation
of 
(also instrumenting the possible variable instantiations).
From the definition of , it is immediate to see that the pattern
of a branch node 
is simply augmented
by a flat term 
, which is placed at the inductive
position o of ,
in order to attain
the patterns of the (root nodes of the) sons 
, for 
.
On the other hand, the decision about the
definitional tree to be considered in the next step, only
depends on the constructor symbol 
rather than on the entire
pattern of the son .
Thus, we have developed an optimized representation of the definitional
trees which moves the pattern matching information to the exact
place where it is needed.
Given a TRS 
, an incremental definitional tree 
with pattern is an expression of the form:
is a variant of a
rule 
.
, 
are constructors for n>0,
and each 
is an incremental definitional tree with
pattern 
where
k is the arity of the constructor
and 
are new variables.
The pattern of an incremental definitional tree, which is not explicitly included in its syntactic structure, can be easily obtained as follows:
Standard and incremental definitional trees are related by
means of a function 
which maps standard
definitional trees to incremental definitional trees:
Figure 2: Incremental definitional tree for the function first
Note that it is
immediate to redefine
in terms of incremental definitional trees,
although we don't include this definition in the paper.