is an  N  node, and   and  
If are dependent under  (  ), then   and belong to the same element of a
( ( ) ( )), and
( )
cntradiction.

If is an node and ( ), then must be the bidder of ), but then ( ) ( ) and ( ) a contradiction again.  
The lemma relates to subgoal independence inside divisibilit trees. eshall sometimes nneed to argue about independence inside ordered se uences of subgoals.  The following corollar provides the necessar connecting link.

Corollary 2 Let  o be a set of subgoals,  
ordering of  o: 
independent of  2     (  ) under   1 be a node in the divisibility tree of  o,  o an 1 and  ( )   .

2. Then  (  ) is mutually Proof:  et are independent under  (  ), b  the
( ),
2 and preceding lemma. ince ( ) 
( ) is independent of ever subgoal of 2 ( ) under 1 therefore, ( ) and 2 
( )
are mutuall  independent under   1.

□

## 4.2 Valid Orderings In Divisibility Trees

The aim of our ordering algorithm is to find a minimal ordering of a given set of subgoals.

e construct orderings following a divide and con uer polic - larger sets are split into smaller ones, and orderings of the smaller sets are combined to produce an ordering of the larger set. To implement this polic , we perform a post order traversal of the divisibilit tree corresponding to the given set of subgoals under an empt  initial binding set.

hen ordenngs of child nodes are combined to produce an ordenng of the parent node, the inner order of their subgoals is not changed smaller orderings are consistent with larger orderings.

Definition:   et    and G       be sets of subgoals.    n ordering s of    are consistent (denoted         ( G    s)), if the order of subgoals of G in    G and in s is the same.

The divide and con uer process described above seems analogous to erge ort (Knuth, 197 ). There, the set of numbers is split into two (or more) subsets, each subset is inde pendentl ordered to a se uence consistent with the global order, and these se uences are merged. Is it possible to use a similar method for subgoal ordering    ssume that a set of subgoals is partitioned into two mutuall  independent subsets, A and   .    an we build an algorithm that, given A, produces its ordering consistent with a minimal ordering of
, independentl   of         nfortunatel , the answer is negative.    n ordering of A ma A
be consistent with a minimal ordering of A    1 but at the same time not be consistent with a minimal ordering of A 2 for some 1 -
1.2 ore ample, let A
specified in igure 9. The single minimal ordering of A
single minimal ordering of A 2 is an 1 ( 2 ) . There is no ordering of A consistent with both these minimal global orderings.