let s be State of SCM+FSA; :: thesis: for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA
for S being State of SCM+FSA st S = IExec ((Selection-sort f),p,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 p being Instruction-Sequence of SCM+FSA
for S being State of SCM+FSA st S = IExec ((Selection-sort f),p,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 p be Instruction-Sequence of SCM+FSA; :: thesis: for S being State of SCM+FSA st S = IExec ((Selection-sort f),p,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);
let S be State of SCM+FSA; :: thesis: ( S = IExec ((Selection-sort f),p,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),p,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));
set p1 = p;
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:74
.= 1 by SCMFSA_M:9 ;
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 SCMFSA_M:25;
then A3: not swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))) destroys 1 -stRWNotIn ({} Int-Locations) by Th30;
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))))),p,(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:74
.= len (s . f) by SCMFSA_M:37 ;
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₁[ 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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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_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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . $1,p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) ) );
A5: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be 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))))),p,(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_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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) )
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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1)) . (intloc 0) = 1 by A6, Th16, 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_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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0))))))
(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1))) . (intloc 0) = 1 by SCMFSA_M:9;
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_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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1)),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by Th27;
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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1))),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by SCMFSA7B:19;
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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1)),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by SFMASTR1:3, A8;
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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by A7, SCMFSA8B:42; :: thesis: verum

end;

A9: 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . 0)) . (intloc 0) = 1 by SCMFSA_M:9;
then A10: 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . 0),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by Th27;
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))))),p,(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_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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . 0,p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) )
thus A11: ((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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . 0) . (intloc 0) = 1 by A2, Th8; :: 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . 0,p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . 0)),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by SCMFSA7B:19;
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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . 0),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by SFMASTR1:3, A10;
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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . 0,p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by A11, SCMFSA8B:42; :: thesis: verum

end;

A12: for k being Nat holds S₂[k] from NAT_1:sch 2(A9, A5);
A13: 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)),p by A12;
then A14: 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))))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . n) by A2, Th23;
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)),p by A2, A13, Th24;
then A15: 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))))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . f by A1, SFMASTR1:15
.= ((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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . n) . f by A14, SCMFSA_M:2 ;
not FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations))) destroys 1 -stRWNotIn ({} Int-Locations) by Th25, SCMFSA_M:26;
then A16: 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)))) destroys 1 -stRWNotIn ({} Int-Locations) by A3, SCMFSA8C:52;
A17: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A18: S₁[k] ; :: thesis: S₁[k + 1]

A19: now :: thesis: ( k < 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))))),p,(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_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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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))))),p,(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))))),p,(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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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) ) )

assume A20: 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))))),p,(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_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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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))))),p,(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))))),p,(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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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 A21: ((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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . (intloc 0) = 1 by A12; :: 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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))))),p,(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))))),p,(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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by A12, A20;
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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by A21, SCMFSA8B:42; :: 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))))),p,(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))))),p,(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))))),p,(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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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))))),p,(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 A18, A20; :: 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))))),p,(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))))),p,(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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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))))),p,(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 A18, A20; :: 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))))),p,(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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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))))),p,(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, A18, A20, 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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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, A13, A20, Th19; :: 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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1)) . f;
assume A22: 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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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 pp being Permutation of (dom (s . f)) such that
A23: ((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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f = (s . f) * pp by A18, 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))))),p,(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 A16, A2, A13, A22, 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))))),p,(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))))),p,(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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1)) . f = (s . f) * p )
A24: 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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k))),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by SCMFSA7B:19;
A25: 1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))) = 1 -stRWNotIn (UsedILoc (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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f)));
A26: dom (s . f) = Seg (len (s . f)) by FINSEQ_1:def 3;
then A27: 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f) = len (s . f) by A23, FINSEQ_2:43;
A28: 1 <= k + 1 by NAT_1:12;
then A29: 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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f))) by A2, A4, A22, A27, FINSEQ_6:161;
then A30: 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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f))) by A28, 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))))),p,(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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f) by A2, A4, A22, A27, A28, FINSEQ_6:161;
then A31: 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))))),p,(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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f) by A30, FINSEQ_3:25;
A32: {(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))} c= UsedILoc (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))) by Th33;
2 -ndRWNotIn ({} Int-Locations) in {(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))} by TARSKI:def 2;
then A33: 1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))) <> 2 -ndRWNotIn ({} Int-Locations) by A25, A32, SCMFSA_M:25;
1 -stRWNotIn ({} Int-Locations) in {(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))} by TARSKI:def 2;
then A34: 1 -stRWNotIn ({} Int-Locations) <> 1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))) by A25, A32, SCMFSA_M:25;
A35: 1 -stRWNotIn ({} Int-Locations) <> 2 -ndRWNotIn ({} Int-Locations) by SCMFSA_M:26;
(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k)) . (intloc 0) = 1 by SCMFSA_M:9;
then A36: 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k),p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))))),(intloc 0)))))) by Th27;
A37: ((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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k));
A38: 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))))),p,(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))))),p,(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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f) & k + 1 = |.(k + 1).| ) by A4, A19, A22, A23, A26, ABSVALUE:def 1, FINSEQ_2:43, NAT_1:13;
then A39: (IExec ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f))) by A2, A19, A22, A33, A35, A28, A38, Th29, NAT_1:13;
then A40: 1 <= (IExec ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k))) . (2 -ndRWNotIn ({} Int-Locations)) by A28, A29, XXREAL_0:2;
A41: (IExec ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f by A19, A22, A33, A35, Th28, NAT_1:13;
then A42: (IExec ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k))) . f) by A2, A4, A22, A27, A28, A39, FINSEQ_6:161;
A43: ( (IExec ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k))) . (intloc 0) = 1 ) by A2, A19, A22, A36, A33, A35, Th28, NAT_1:13, SCMFSA8C:67;
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))))),p,(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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k))) . f by A19, A22, NAT_1:13, SCMFSA_M:28
.= (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))))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k))))) . f by A19, A22, 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))))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k))) . f by SCMFSA_2:64
.= (IExec ((swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k))))) . f by A36, SFMASTR1:8
.= ((((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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f) . (k + 1))) by A2, A4, A22, A27, A28, A41, A39, A40, A42, A43, Th31 ; :: 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f) by A2, A4, A22, A27, A28, FINSEQ_3:25;
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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f)) such that
A44: ((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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f) * p1 by A31, A37, FUNCT_7:111;
( {(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations))} c= UsedILoc (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 Th26, ENUMSET1:def 1;
then 1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))) in (UsedILoc (FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations))))) \/ (UsedILoc (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 UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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:27;
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)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (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))))),p,(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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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 A19, A22, NAT_1:13, SCMFSA_M:28
.= (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))))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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 A19, A22, NAT_1:13, SFMASTR1:11
.= (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))))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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 A34, SCMFSA_2:64
.= (IExec ((swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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 A36, SFMASTR1:7
.= (Initialized (IExec ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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 A25, A24, SCMFSA_M:25, 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)))),(p +* (while>0 ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (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))))) ";" (AddTo ((1 -stRWNotIn ({} Int-Locations)),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))} \/ (UsedILoc ((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} 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))))),p,(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 SCMFSA_M:37
.= (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 A19, A22, A33, A35, Th28, 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))))),p,(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))))),p,(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))))),p,(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))))),p,(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, A18, A22, A27, A37, FINSEQ_6:164, 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))))),p,(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))))),p,(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))))),p,(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, A18, A22, A27, A37, FINSEQ_6:163, 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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . k) . f) = dom (s . f) by A27, FINSEQ_3:29;
then reconsider p1 = p1 as Permutation of (dom (s . f)) ;
reconsider ppp = pp * p1 as Permutation of (dom (s . f)) ;
take ppp ; :: 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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1)) . f = (s . f) * ppp
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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . (k + 1)) . f = (s . f) * ppp by A23, A44, RELAT_1:36; :: thesis: verum

end;

A45: dom (s . f) = Seg (len (s . f)) by FINSEQ_1:def 3;
A46: 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 (UsedILoc (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) & {(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))} c= UsedILoc (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))) ) by Th33, SFMASTR1:def 4;
then A47: 1 -stRWNotIn ({} Int-Locations) <> 1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))) by A46, SCMFSA_M:25;
A48: 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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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 Th9; :: 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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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 A47, Th11; :: 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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(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))))),p,(Exec (((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f),(Initialized s))))) . 0) . f = (s . f) * p
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:55;
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))))),p,(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))))),p,(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 Th13
.= (Initialized s) . f by SCMFSA_2:74
.= s . f by SCMFSA_M:37 ;
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))))),p,(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:54; :: thesis: verum

end;

A49: for k being Nat holds S₁[k] from NAT_1:sch 2(A48, A17);
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))))),p,(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, A15, A45, FINSEQ_2:43;
hence S . f is_non_decreasing_on 1, len (S . f) by A49, A15; :: 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 A49, A15; :: thesis: verum