Database Reference
In-Depth Information
2. Find an atomic node in
t
RA
. If both paths from this node to their leafs are without
unary operations _
, then eliminate this binary node and unify these
two paths in a unique path, as specified by Definition
22
, and hence go to Step 1.
Otherwise, take in consideration the path with the unary operations _
a,name,e
a,
and continue with Step 3.
3. Here we consider the path of the current term
t
RA
such that it contains at least
one operation _
name,e
. Take into consideration such an operation, which
is closer to the leaf of this path, and unfold it along this path for only one step
toward the leaf, as specified by one of the cases in Definition
34
. Continue this
process up to the situation when _
a,name,e
a,name,e
reaches the leaf of this path. Then
go to Step 1.
