let s be State of SCM+FSA ; :: thesis: for f being FinSeq-Location
for S being State of SCM+FSA st S = IExec (Selection-sort f),s holds
( S . f is_non_decreasing_on 1, len (S . f) & ex p being Permutation of (dom (s . f)) st S . f = (s . f) * p )
let f be FinSeq-Location ; :: thesis: for S being State of SCM+FSA st S = IExec (Selection-sort f),s holds
( S . f is_non_decreasing_on 1, len (S . f) & ex p being Permutation of (dom (s . f)) st S . f = (s . f) * p )
set minpos = 2 -ndRWNotIn ({} Int-Locations );
set cv = 1 -stRWNotIn ({} Int-Locations );
set D = Int-Locations \/ FinSeq-Locations ;
let S be State of SCM+FSA ; :: thesis: ( S = IExec (Selection-sort f),s implies ( S . f is_non_decreasing_on 1, len (S . f) & ex p being Permutation of (dom (s . f)) st S . f = (s . f) * p ) )
assume A1: S = IExec (Selection-sort f),s ; :: thesis: ( S . f is_non_decreasing_on 1, len (S . f) & ex p being Permutation of (dom (s . f)) st S . f = (s . f) * p )
set I22 = swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ));
set finish = 1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )));
set i1 = (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f;
set I21 = FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ));
set I2B = (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )));
set I2 = for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))));
set s1 = Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s);
A2: (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 ) = (Initialized s) . (intloc 0 ) by SCMFSA_2:100
.= 1 by SCMFSA6C:3 ;
1 -stRWNotIn ({} Int-Locations ) in {(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))} by TARSKI:def 2;
then ( 1 -stRWNotIn ({} Int-Locations ) <> 1 -stRWNotIn {(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))} & 1 -stRWNotIn ({} Int-Locations ) <> 2 -ndRWNotIn {(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))} ) by SFMASTR1:21;
then A3: not swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )) destroysdestroy 1 -stRWNotIn ({} Int-Locations ) by Th38;
set SF = StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s));
A4: (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = len ((Initialized s) . f) by SCMFSA_2:100
.= len (s . f) by SCMFSA6C:3 ;
then reconsider n = (((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))) - ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 ))) + 1 as Element of NAT by A2;
defpred S₁[ Element of NAT ] means ( $1 <= n implies ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . $1) . (1 -stRWNotIn ({} Int-Locations )) = $1 + ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 )) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . $1) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . $1) . f is_split_at $1 & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . $1) . f is_non_decreasing_on 1,$1 & ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . $1) . f = (s . f) * p ) );
defpred S₂[ Nat] means ( $1 < n implies ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . $1) . (intloc 0 ) = 1 & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . $1 & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . $1 ) );
A5: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A6: S₂[k] ; :: thesis: S₂[k + 1]
assume k + 1 < n ; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . (intloc 0 ) = 1 & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1) & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1) )
hence A7: ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . (intloc 0 ) = 1 by A6, Th24, NAT_1:13; :: thesis: ( (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1) & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1) )
(Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1))) . (intloc 0 ) = 1 by SCMFSA6C:3;
then A8: ( FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations )) is_closed_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) & FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations )) is_halting_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) ) by Th35;
A9: swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )) is_closed_on IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) by SCMFSA7B:24;
then A10: (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) by A8, SFMASTR1:3;
hence (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1) by A7, SFMASTR2:4; :: thesis: (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)
swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )) is_halting_on IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) by SCMFSA7B:25;
then (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) by A8, A9, SFMASTR1:4;
hence (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1) by A7, A10, SFMASTR2:5; :: thesis: verum

end;

A11: S₂[ 0 ]

proof

(Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 )) . (intloc 0 ) = 1 by SCMFSA6C:3;
then A12: ( FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations )) is_closed_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) & FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations )) is_halting_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) ) by Th35;
assume 0 < n ; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . (intloc 0 ) = 1 & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 )
thus A13: ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . (intloc 0 ) = 1 by A2, Th16; :: thesis: ( (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 )
A14: swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )) is_closed_on IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) by SCMFSA7B:24;
then A15: (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) by A12, SFMASTR1:3;
hence (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 by A13, SFMASTR2:4; :: thesis: (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0
swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )) is_halting_on IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) by SCMFSA7B:25;
then (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) by A12, A14, SFMASTR1:4;
hence (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 by A13, A15, SFMASTR2:5; :: thesis: verum

end;

A16: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A11, A5);
A17: ProperForUpBody 1 -stRWNotIn ({} Int-Locations ), intloc 0 ,1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))),(FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))), Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)

proof

let i be Element of NAT ; :: according to SFMASTR3:def 7 :: thesis: ( i < (((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))) - ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 ))) + 1 implies ( (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . i & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . i ) )
thus ( i < (((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))) - ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 ))) + 1 implies ( (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . i & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . i ) ) by A16; :: thesis: verum

end;

then A18: DataPart (IExec (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) = DataPart ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . n) by A2, Th31;
( for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) is_halting_on Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s) & for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) is_closed_on Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s) ) by A2, A17, Th32;
then A19: S . f = (IExec (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . f by A1, SFMASTR1:16
.= ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . n) . f by A18, SCMFSA6A:38 ;
not FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations )) destroysdestroy 1 -stRWNotIn ({} Int-Locations ) by Th33, SFMASTR1:22;
then A20: not (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) destroysdestroy 1 -stRWNotIn ({} Int-Locations ) by A3, SCMFSA8C:81;
A21: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A22: S₁[k] ; :: thesis: S₁[k + 1]

A23: now

assume A24: k < n ; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (intloc 0 ) = 1 & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) = k + ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 )) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) <= (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) = (IExec (((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) ';' (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) )
hence A25: ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (intloc 0 ) = 1 by A16; :: thesis: ( (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) & (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) = k + ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 )) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) <= (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) = (IExec (((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) ';' (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) )
A26: (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k by A16, A24;
hence (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_closed_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) by A25, SFMASTR2:4; :: thesis: ( (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) = k + ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 )) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) <= (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) = (IExec (((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) ';' (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) )
(FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on (StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k by A16, A24;
hence (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) is_halting_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) by A25, A26, SFMASTR2:5; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) = k + ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 )) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) <= (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) = (IExec (((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) ';' (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) )
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) = k + ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 )) by A22, A24; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) <= (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) = (IExec (((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) ';' (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) )
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by A22, A24; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) <= (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) = (IExec (((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) ';' (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) )
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stRWNotIn ({} Int-Locations )) <= (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by A2, A22, A24, NAT_1:13; :: thesis: ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) = (IExec (((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) ';' (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations )
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) = (IExec (((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) ';' (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) | (({(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))))) \/ FinSeq-Locations ) by A2, A17, A24, Th27; :: thesis: verum

end;

set F = ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f;
set F1 = ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f;
assume A27: k + 1 <= n ; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . (1 -stRWNotIn ({} Int-Locations )) = (k + 1) + ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 )) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f is_split_at k + 1 & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f is_non_decreasing_on 1,k + 1 & ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f = (s . f) * p )
then consider p being Permutation of (dom (s . f)) such that
A28: ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f = (s . f) * p by A22, NAT_1:13;
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . (1 -stRWNotIn ({} Int-Locations )) = (k + 1) + ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 )) by A20, A2, A17, A27, Th25; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f is_split_at k + 1 & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f is_non_decreasing_on 1,k + 1 & ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f = (s . f) * p )
A29: ( swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )) is_closed_on Initialized (IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) & swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )) is_halting_on Initialized (IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) ) by SCMFSA7B:24, SCMFSA7B:25;
A30: 1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) = 1 -stRWNotIn (UsedIntLoc (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by SFMASTR1:def 4;
set ma = min_at (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f),(k + 1),(len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f));
A31: dom (s . f) = Seg (len (s . f)) by FINSEQ_1:def 3;
then A32: len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) = len (s . f) by A28, FINSEQ_2:47;
A33: 1 <= k + 1 by NAT_1:12;
then A34: k + 1 <= min_at (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f),(k + 1),(len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f)) by A2, A4, A27, A32, GRAPH_2:63;
then A35: 1 <= min_at (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f),(k + 1),(len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f)) by A33, XXREAL_0:2;
min_at (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f),(k + 1),(len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f)) <= len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) by A2, A4, A27, A32, A33, GRAPH_2:63;
then A36: min_at (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f),(k + 1),(len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f)) in dom (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) by A35, FINSEQ_3:27;
A37: {(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))} c= UsedIntLoc (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) by Th41;
2 -ndRWNotIn ({} Int-Locations ) in {(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))} by TARSKI:def 2;
then A38: 1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) <> 2 -ndRWNotIn ({} Int-Locations ) by A30, A37, SFMASTR1:21;
1 -stRWNotIn ({} Int-Locations ) in {(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))} by TARSKI:def 2;
then A39: 1 -stRWNotIn ({} Int-Locations ) <> 1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) by A30, A37, SFMASTR1:21;
A40: 1 -stRWNotIn ({} Int-Locations ) <> 2 -ndRWNotIn ({} Int-Locations ) by SFMASTR1:22;
(Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . (intloc 0 ) = 1 by SCMFSA6C:3;
then A41: ( FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations )) is_closed_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) & FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations )) is_halting_on Initialized ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) ) by Th35;
A42: ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f = ((((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) +* (k + 1),((((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) . (min_at (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f),(k + 1),(len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f))))) +* (min_at (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f),(k + 1),(len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f))),((((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) . (k + 1))

proof

set S2 = IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k);
A43: len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) = abs (len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f)) by ABSVALUE:def 1;
( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) & k + 1 = abs (k + 1) ) by A4, A23, A27, A28, A31, ABSVALUE:def 1, FINSEQ_2:47, NAT_1:13;
then A44: (IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . (2 -ndRWNotIn ({} Int-Locations )) = min_at (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f),(k + 1),(len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f)) by A2, A23, A27, A38, A40, A33, A43, Th37, NAT_1:13;
then A45: 1 <= (IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . (2 -ndRWNotIn ({} Int-Locations )) by A33, A34, XXREAL_0:2;
A46: (IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . f = ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f by A23, A27, A38, A40, Th36, NAT_1:13;
then A47: (IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . (2 -ndRWNotIn ({} Int-Locations )) <= len ((IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . f) by A2, A4, A27, A32, A33, A44, GRAPH_2:63;
A48: ( (IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . (1 -stRWNotIn ({} Int-Locations )) = k + 1 & (IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . (intloc 0 ) = 1 ) by A2, A23, A27, A41, A38, A40, Th36, NAT_1:13, SCMFSA8C:96;
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f = (IExec (((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) ';' (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . f by A23, A27, NAT_1:13, SFMASTR2:7
.= (Exec (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 )),(IExec ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k))) . f by A23, A27, NAT_1:13, SFMASTR1:13
.= (IExec ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . f by SCMFSA_2:90
.= (IExec (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))),(IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k))) . f by A41, SFMASTR1:9
.= ((((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) +* (k + 1),((((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) . (min_at (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f),(k + 1),(len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f))))) +* (min_at (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f),(k + 1),(len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f))),((((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) . (k + 1)) by A2, A4, A27, A32, A33, A46, A44, A45, A47, A48, Th39 ; :: thesis: verum

end;

k + 1 in dom (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) by A2, A4, A27, A32, A33, FINSEQ_3:27;
then consider p1 being Permutation of (dom (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f)) such that
A49: ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f = (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) * p1 by A36, A42, FUNCT_7:113;
( {(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))} c= UsedIntLoc (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) & 1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) in {(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))} ) by Th34, ENUMSET1:def 1;
then 1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) in (UsedIntLoc (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations )))) \/ (UsedIntLoc (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by XBOOLE_0:def 3;
then 1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) in UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by SF_MASTR:31;
then 1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) in {(1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))} \/ (UsedIntLoc ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))) by XBOOLE_0:def 3;
hence ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (IExec (((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) ';' (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by A23, A27, NAT_1:13, SFMASTR2:7
.= (Exec (AddTo (1 -stRWNotIn ({} Int-Locations )),(intloc 0 )),(IExec ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k))) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by A23, A27, NAT_1:13, SFMASTR1:12
.= (IExec ((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by A39, SCMFSA_2:90
.= (IExec (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))),(IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k))) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by A41, SFMASTR1:8
.= (Initialized (IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k))) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by A30, A29, SFMASTR1:21, SFMASTR2:1
.= (IExec (FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))),((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by SCMFSA6C:3
.= (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by A23, A27, A38, A40, Th36, NAT_1:13 ;
:: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f is_split_at k + 1 & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f is_non_decreasing_on 1,k + 1 & ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f = (s . f) * p )
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f is_split_at k + 1 by A2, A4, A22, A27, A32, A42, GRAPH_2:66, NAT_1:13; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f is_non_decreasing_on 1,k + 1 & ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f = (s . f) * p )
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f is_non_decreasing_on 1,k + 1 by A2, A4, A22, A27, A32, A42, GRAPH_2:65, NAT_1:13; :: thesis: ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f = (s . f) * p
dom (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . k) . f) = dom (s . f) by A32, FINSEQ_3:31;
then reconsider p1 = p1 as Permutation of (dom (s . f)) ;
reconsider pp = p * p1 as Permutation of (dom (s . f)) ;
take pp ; :: thesis: ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f = (s . f) * pp
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . (k + 1)) . f = (s . f) * pp by A28, A49, RELAT_1:55; :: thesis: verum

end;

A50: dom (s . f) = Seg (len (s . f)) by FINSEQ_1:def 3;
A51: 1 -stRWNotIn ({} Int-Locations ) in {(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))} by TARSKI:def 2;
( 1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) = 1 -stRWNotIn (UsedIntLoc (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & {(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))} c= UsedIntLoc (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) ) by Th41, SFMASTR1:def 4;
then A52: 1 -stRWNotIn ({} Int-Locations ) <> 1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))) by A51, SFMASTR1:21;
A53: S₁[ 0 ]

proof

assume 0 <= n ; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . (1 -stRWNotIn ({} Int-Locations )) = 0 + ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 )) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f is_split_at 0 & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f is_non_decreasing_on 1, 0 & ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f = (s . f) * p )
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . (1 -stRWNotIn ({} Int-Locations )) = 0 + ((Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (intloc 0 )) by Th17; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f is_split_at 0 & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f is_non_decreasing_on 1, 0 & ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f = (s . f) * p )
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . (1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) by A52, Th19; :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f is_split_at 0 & ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f is_non_decreasing_on 1, 0 & ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f = (s . f) * p )
thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f is_split_at 0 :: thesis: ( ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f is_non_decreasing_on 1, 0 & ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f = (s . f) * p )

proof

let i, j be Element of NAT ; :: according to GRAPH_2:def 14 :: thesis: ( not 1 <= i or not i <= 0 or j <= 0 or not j <= len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) or (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . i <= (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . j )
assume that
A54: ( 1 <= i & i <= 0 ) and
0 < j and
j <= len (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) ; :: thesis: (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . i <= (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . j
thus (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . i <= (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . j by A54; :: thesis: verum

end;

thus ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f is_non_decreasing_on 1, 0 :: thesis: ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f = (s . f) * p

proof

let i, j be Element of NAT ; :: according to GRAPH_2:def 13 :: thesis: ( not 1 <= i or not i <= j or not j <= 0 or (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . i <= (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . j )
assume that
1 <= i and
A55: ( i <= j & j <= 0 ) ; :: thesis: (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . i <= (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . j
thus (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . i <= (((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f) . j by A55; :: thesis: verum

end;

dom (s . f) = Seg (len (s . f)) by FINSEQ_1:def 3;
then reconsider p = idseq (len (s . f)) as Permutation of (dom (s . f)) by FINSEQ_2:65;
take p ; :: thesis: ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f = (s . f) * p
((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f = (Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s)) . f by Th21
.= (Initialized s) . f by SCMFSA_2:100
.= s . f by SCMFSA6C:3 ;
hence ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . 0 ) . f = (s . f) * p by FINSEQ_2:64; :: thesis: verum

end;

A56: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A53, A21);
then ex p being Permutation of (dom (s . f)) st ((StepForUp (1 -stRWNotIn ({} Int-Locations )),(intloc 0 ),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(Exec ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f),(Initialized s))) . n) . f = (s . f) * p ;
then len (S . f) = n by A2, A4, A19, A50, FINSEQ_2:47;
hence S . f is_non_decreasing_on 1, len (S . f) by A56, A19; :: thesis: ex p being Permutation of (dom (s . f)) st S . f = (s . f) * p
thus ex p being Permutation of (dom (s . f)) st S . f = (s . f) * p by A56, A19; :: thesis: verum