that substitution of a sub se  uence b  its cheaper permutation makes the entire se  uence cheaper.

## Le Mma  1

, where and are permutations of one another, and Let either is empty or has nsols(  )     . Then

cost ( ) A      cost (  ) A ( ) ( ) cost ( ) A     cost (  ) A ( ) ()
Proof: If and    are not empt ,

Cost(S)  Cost(S)  =  Cost(A B C)  Cost(A B C) = (5) (cost(A) + nsols(A) + cost(B) , + nsols(A) B) + cost(C) , c B) (COSI(A) + nsols(A) cosi(B) x + nsols(A) B) cosi(C) x B )
Theorem 1, and . produce the same solution sets. ence, the third terms in the parentheses above are e ual, and

$\left(\begin{array}{cccc}\end{array}\right)$$\left(\begin{array}{cccc}\end{array}\right)$$\left(\begin{array}{cccc}\end{array}\right)$$\left(\begin{array}{cccc}\end{array}\right)$$\left(\begin{array}{cccc}\end{array}\right)$$\left(\begin{array}{cccc}\end{array}\right)$$\left(\begin{array}{cccc}\end{array}\right)$$\left(\begin{array}{cccc}\end{array}\right)$$\left(\begin{array}{cccc}\end{array}\right)$$\left(\begin{array}{cccc}\end{array}\right)$$\left(\begin{array}{cccc}\end{array}\right)$\(\left(\begin{array}{cccc}\
ince nsols( )    , the sign of     ( )   ,     (  ) coincides with the sign of cost(  ) A If or is empt , the proof is similar. cest (   ) A
口 Definition: et le 2020 be an ordered seluence of subgoals ( 1 and 2 ama be empt  se  uences).   ith respect to  , the pair  ,  1  ,  2  is

$$\begin{array}{l l l l l l}{c n\,\mathrm{-}o r d e r e d,\;\mathrm{if}}&{{}}&{{}}&{{}{\left(\begin{array}{l}{{}}&{{1}}\end{array}\right)_{A}}}&{}&{{}}&{{}}&{{\left(\begin{array}{l}{{}}&{{2}}\end{array}\right)_{A}\begin{array}{l l l l l}{B_{1}}&{C_{1}}}\end{array}$$
cn-inverted, if   (1) A      (12) A  B1  C
e now show that two ad  acent mutually independent se  uences of subgoals in a minimal ordering must be cn ordered.

## Le Mma  2

Let 2 - 1 - , where , 1 , - 2 are mulually independent under land and the content of the content.

Let    either be empty or have nsols(  )     . Then

$$\begin{array}{l l l l l l l}{{(}&{{})}}&{{}}&{{(}&{{})}}&{{}}&{{}}&{{(}&{{})_{A}}}&{{}}&{{(}&{{})_{A}}}\\ {{(}&{{})}}&{{}}&{{}}&{{(}&{{})}}&{{}}&{{}}&{{}}&{{(}&{{})_{A}}}&{{}}&{{}}&{{(}&{{})_{A}}}\end{array}$$
$$49$$
