
## Le Mma  1 0

Let  o be a set of subgoals and   be a node in the divisibility tree of  o  Let  N
1 2 2 be an ordering of ( ), where 1 and 2 are cn-equal max-blocks: ( 1) (N) Q
( 2) (N) Q A1' Let     be an ancestor of    and    M  be an ordering of   (   ) consistent with   N, where 1 and 2 are not violated. Then either 1 and 2 are both max-blocks in  M and all max-blocks that stand between them are cn-equal to them, or   1 and   2 belong to the same max-block in Proof:     induction on the distance between   and   .  If
, then i and are ma  blocks, and the lemma holds.  et descend ant is . . . . . inductive h  pothesis, the lemma holds for . . . and . . . . et . M be the protection of Mone a mand 2 are not violated in M since the are not violated in M
If 1 and 2 are both ma blocks in M, then b the inductive h pothesis all ma blocks that stand between them are cn e ual to them. If    is an     node, no new subgoals can enter between 1 and 2. If 2 is an N node, the insertion of new subgoals is possible, but if it violates blocks, or places ma  blocks not ordered b  cn, then M is contradicting, b orollar or emma . o, if M is not contradicting, then all new ma  blocks inserted between   1 and   2 must be c n e  ual to them both.

sume that 1 and 2 are not both ma blocks in M. ithout loss of generalit ,
let 1 be member of a larger ma block in M. e show that 2 must also participate in the same ma   block.

ince 1 oined a larger block, there must e ist another block, ad acent to 1, such that their pair is cn inverted. et stand to the left of 1 (in the opposite case, the proof is similar) 
2 . The pair compis cn inverted, i.e.,
l 
( ) (M) X     (1) (M) X B   rom emma9,  (1991) (M) X     (1) (M) X B!

and we must add to the block 1 all blocks from 1 because the are all c n e ual to 1. Iso, 2 (1) (M) x B (2) (M) x B A,, and 2 must also be added to the block. Thus, 1 and 2 belong to the same ma block in M. If 1 and 2 belong to the same ma  block in  M, then this block is either violated in M, or not. In the former case, M is contradicting, b corollar . In the latter case, 1 and 2 belong to the same ma block in M
If M is contradicting, then M is contradicting too (the proof is eas ). 

Now we can prove  emma

## Le Mma 8

et o be a set of subgoals, be a node in the divisibilit tree of o and N
1 