

![0_image_0.png](0_image_0.png)

Lemma 7 Let be a node in the divisibility tree of 0, N
be a leading
( ( )). Let block of AND N
. If there is a permutation of the
, such that cost (
) (N)
cest( ) (N), then, N is MC-contradicting.

Proof:  et   s     ( o) be binder consistent with  N . If   is violated in   s,   s cannot be minimal ( orollar  ).   therwise,   occupies a continuous segment in  s, and its replacement b  a cheaper permutation reduces the cost of the global ordering ( emma 1).

Thus,  s cannot be minimal.

□
This check should be done onl  for leading blocks of nodes ver ordering of a leaf node that has not been re ected due to  emma   must be sorted b . onse uentl , it contains no cn inverted ad acent pair of subgoals, and no block of si e     can be formed.

ver ordering of an N node that has not been re ected due to oollar O I
emma   must have its blocks unbroken and in cn ascending order.

onse uentl ,
new blocks cannot be formed here either.

nodes, new blocks can be formed when we add a binder as the first element of l n an ordering, if the     value of the binder is greater than that of the subse  uent  block.

l new blocks start from the binder, and we must perform the permutation test onl on the leading ma block of an ordering.

## 4.5  Detection Of Mc- Equivalent  Orderings

1. In the previous subsection we presented su cient conditions for detecting contradicting to ordenngs. In this subsection we specif su cient conditions for identif ing e uivalent orderings. ecall that two orderings of a node are e uivalent if minimal consistenc of one implies minimal consistenc of the other. inding such su cient conditions will allow us to eliminate orderings without loss of validit  of the candidate set.    e start with defining a speciali ation of the e uivalence relation Mockwise equivalence.

then show that orderings whose ma  blocks are sorted b       are blockwise e  uivalent, and t herefore e uivalent.