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] A9: S₂[ 0 ] 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] 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 ] 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