:: Bubble Sort on SCM+FSA
:: by JingChao Chen and Yatsuka Nakamura
::
:: Received June 17, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem :: SCMBSORT:1
canceled;
theorem :: SCMBSORT:2
canceled;
theorem Th3: :: SCMBSORT:3
theorem :: SCMBSORT:4
canceled;
theorem :: SCMBSORT:5
canceled;
theorem :: SCMBSORT:6
canceled;
theorem :: SCMBSORT:7
canceled;
theorem Th8: :: SCMBSORT:8
theorem Th9: :: SCMBSORT:9
theorem Th10: :: SCMBSORT:10
theorem Th11: :: SCMBSORT:11
theorem Th12: :: SCMBSORT:12
theorem :: SCMBSORT:13
canceled;
theorem :: SCMBSORT:14
canceled;
theorem :: SCMBSORT:15
canceled;
theorem Th16: :: SCMBSORT:16
theorem Th17: :: SCMBSORT:17
theorem Th18: :: SCMBSORT:18
theorem Th19: :: SCMBSORT:19
theorem Th20: :: SCMBSORT:20
theorem Th21: :: SCMBSORT:21
theorem :: SCMBSORT:22
canceled;
theorem Th23: :: SCMBSORT:23
theorem :: SCMBSORT:24
canceled;
theorem Th25: :: SCMBSORT:25
for
i,
k being
Element of
NAT for
t being
FinPartState of
SCM+FSA for
p being
Program of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
k <= i &
p c= s1 &
p c= s2 &
dom t c= Int-Locations \/ FinSeq-Locations & ( for
j being
Element of
NAT holds
(
IC (Computation s1,j) in dom p &
IC (Computation s2,j) in dom p ) ) &
(Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) &
(Computation s1,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) holds
(
(Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) &
(Computation s1,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) )
theorem Th26: :: SCMBSORT:26
for
i,
k being
Element of
NAT for
p being
Program of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
k <= i &
p c= s1 &
p c= s2 & ( for
j being
Element of
NAT holds
(
IC (Computation s1,j) in dom p &
IC (Computation s2,j) in dom p ) ) &
(Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) &
(Computation s1,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) holds
(
(Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) &
(Computation s1,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )
theorem :: SCMBSORT:27
canceled;
theorem :: SCMBSORT:28
canceled;
theorem Th29: :: SCMBSORT:29
theorem Th30: :: SCMBSORT:30
theorem Th31: :: SCMBSORT:31
theorem :: SCMBSORT:32
canceled;
theorem :: SCMBSORT:33
canceled;
theorem :: SCMBSORT:34
canceled;
theorem :: SCMBSORT:35
theorem Th36: :: SCMBSORT:36
theorem Th37: :: SCMBSORT:37
theorem :: SCMBSORT:38
theorem Th39: :: SCMBSORT:39
theorem Th40: :: SCMBSORT:40
theorem Th41: :: SCMBSORT:41
theorem Th42: :: SCMBSORT:42
theorem :: SCMBSORT:43
theorem Th44: :: SCMBSORT:44
theorem Th45: :: SCMBSORT:45
theorem Th46: :: SCMBSORT:46
theorem Th47: :: SCMBSORT:47
theorem Th48: :: SCMBSORT:48
theorem :: SCMBSORT:49
for
ic being
Instruction of
SCM+FSA for
f being
FinSeq-Location for
a,
b being
Int-Location for
la being
Instruction-Location of
SCM+FSA st (
ic = a := b or
ic = AddTo a,
b or
ic = SubFrom a,
b or
ic = MultBy a,
b or
ic = Divide a,
b or
ic = goto la or
ic = a =0_goto la or
ic = a >0_goto la or
ic = b := f,
a or
ic = f,
a := b or
ic = a :=len f or
ic = f :=<0,...,0> a ) holds
ic <> halt SCM+FSA by SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53, SCMFSA_2:124;
theorem Th50: :: SCMBSORT:50
theorem Th51: :: SCMBSORT:51
theorem Th52: :: SCMBSORT:52
theorem Th53: :: SCMBSORT:53
theorem Th54: :: SCMBSORT:54
theorem Th55: :: SCMBSORT:55
theorem Th56: :: SCMBSORT:56
theorem Th57: :: SCMBSORT:57
set a0 = intloc 0 ;
set a1 = intloc 1;
set a2 = intloc 2;
set a3 = intloc 3;
set a4 = intloc 4;
set a5 = intloc 5;
set a6 = intloc 6;
Lm1:
( intloc 0 <> intloc 1 & intloc 0 <> intloc 2 & intloc 0 <> intloc 3 & intloc 0 <> intloc 4 & intloc 0 <> intloc 5 & intloc 0 <> intloc 6 & intloc 1 <> intloc 2 & intloc 1 <> intloc 3 & intloc 1 <> intloc 4 & intloc 1 <> intloc 5 & intloc 1 <> intloc 6 & intloc 2 <> intloc 3 & intloc 2 <> intloc 4 & intloc 2 <> intloc 5 & intloc 2 <> intloc 6 & intloc 3 <> intloc 4 & intloc 3 <> intloc 5 & intloc 3 <> intloc 6 & intloc 4 <> intloc 5 & intloc 4 <> intloc 6 & intloc 5 <> intloc 6 )
by AMI_3:52;
set initializeWorkMem = (((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ));
definition
let f be
FinSeq-Location ;
func bubble-sort f -> Program of
SCM+FSA equals :: SCMBSORT:def 1
(((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) ';' ((intloc 1) :=len f)) ';' (Times (intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom (intloc 2),(intloc 0 ))) ';' ((intloc 3) :=len f)) ';' (Times (intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 3))) ';' ((intloc 6) := f,(intloc 4))) ';' (SubFrom (intloc 6),(intloc 5))) ';' (if>0 (intloc 6),((((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6))) ';' (f,(intloc 4) := (intloc 5))),(Stop SCM+FSA ))))));
correctness
coherence
(((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) ';' ((intloc 1) :=len f)) ';' (Times (intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom (intloc 2),(intloc 0 ))) ';' ((intloc 3) :=len f)) ';' (Times (intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 3))) ';' ((intloc 6) := f,(intloc 4))) ';' (SubFrom (intloc 6),(intloc 5))) ';' (if>0 (intloc 6),((((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6))) ';' (f,(intloc 4) := (intloc 5))),(Stop SCM+FSA )))))) is Program of SCM+FSA ;
;
end;
:: deftheorem defines bubble-sort SCMBSORT:def 1 :
for
f being
FinSeq-Location holds
bubble-sort f = (((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) ';' ((intloc 1) :=len f)) ';' (Times (intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom (intloc 2),(intloc 0 ))) ';' ((intloc 3) :=len f)) ';' (Times (intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 3))) ';' ((intloc 6) := f,(intloc 4))) ';' (SubFrom (intloc 6),(intloc 5))) ';' (if>0 (intloc 6),((((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6))) ';' (f,(intloc 4) := (intloc 5))),(Stop SCM+FSA ))))));
:: deftheorem defines Bubble-Sort-Algorithm SCMBSORT:def 2 :
set b1 = intloc (0 + 1);
set b2 = intloc (1 + 1);
set b3 = intloc (2 + 1);
set b4 = intloc (3 + 1);
set b5 = intloc (4 + 1);
set b6 = intloc (5 + 1);
set f0 = fsloc 0 ;
set i1 = (intloc (3 + 1)) := (intloc (2 + 1));
set i2 = SubFrom (intloc (2 + 1)),(intloc 0 );
set i3 = (intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1));
set i4 = (intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1));
set i5 = SubFrom (intloc (5 + 1)),(intloc (4 + 1));
set i6 = (fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1));
set i7 = (fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1));
set SS = Stop SCM+FSA ;
set ifc = if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA );
set body2 = ((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ));
set T2 = Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )));
set j1 = (intloc (1 + 1)) := (intloc (0 + 1));
set j2 = SubFrom (intloc (1 + 1)),(intloc 0 );
set j3 = (intloc (2 + 1)) :=len (fsloc 0 );
set Sb = (((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ));
set body1 = ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))) ';' (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))));
set T1 = Times (intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))) ';' (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))));
set w2 = (intloc (1 + 1)) := (intloc 0 );
set w3 = (intloc (2 + 1)) := (intloc 0 );
set w4 = (intloc (3 + 1)) := (intloc 0 );
set w5 = (intloc (4 + 1)) := (intloc 0 );
set w6 = (intloc (5 + 1)) := (intloc 0 );
set w7 = (intloc (0 + 1)) :=len (fsloc 0 );
theorem Th58: :: SCMBSORT:58
theorem Th59: :: SCMBSORT:59
definition
func Sorting-Function -> PartFunc of
(FinPartSt SCM+FSA ),
(FinPartSt SCM+FSA ) means :
Def3:
:: SCMBSORT:def 3
for
p,
q being
FinPartState of
SCM+FSA holds
(
[p,q] in it iff ex
t being
FinSequence of
INT ex
u being
FinSequence of
REAL st
(
t,
u are_fiberwise_equipotent &
u is
FinSequence of
INT &
u is
non-increasing &
p = (fsloc 0 ) .--> t &
q = (fsloc 0 ) .--> u ) );
existence
ex b1 being PartFunc of (FinPartSt SCM+FSA ),(FinPartSt SCM+FSA ) st
for p, q being FinPartState of SCM+FSA holds
( [p,q] in b1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0 ) .--> t & q = (fsloc 0 ) .--> u ) )
uniqueness
for b1, b2 being PartFunc of (FinPartSt SCM+FSA ),(FinPartSt SCM+FSA ) st ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in b1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0 ) .--> t & q = (fsloc 0 ) .--> u ) ) ) & ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in b2 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0 ) .--> t & q = (fsloc 0 ) .--> u ) ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines Sorting-Function SCMBSORT:def 3 :
theorem Th60: :: SCMBSORT:60
theorem Th61: :: SCMBSORT:61
theorem Th62: :: SCMBSORT:62
theorem Th63: :: SCMBSORT:63
Lm2:
for s being State of SCM+FSA st Bubble-Sort-Algorithm c= s holds
( s . (insloc 0 ) = (intloc 2) := (intloc 0 ) & s . (insloc 1) = goto (insloc 2) & s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
Lm3:
for s being State of SCM+FSA st Bubble-Sort-Algorithm c= s & s starts_at 0 holds
( (Computation s,1) . (IC SCM+FSA ) = insloc 1 & (Computation s,1) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,1) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,2) . (IC SCM+FSA ) = insloc 2 & (Computation s,2) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,2) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,3) . (IC SCM+FSA ) = insloc 3 & (Computation s,3) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,3) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,4) . (IC SCM+FSA ) = insloc 4 & (Computation s,4) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,4) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,5) . (IC SCM+FSA ) = insloc 5 & (Computation s,5) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,5) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,6) . (IC SCM+FSA ) = insloc 6 & (Computation s,6) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,6) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,7) . (IC SCM+FSA ) = insloc 7 & (Computation s,7) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,7) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,8) . (IC SCM+FSA ) = insloc 8 & (Computation s,8) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,8) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,9) . (IC SCM+FSA ) = insloc 9 & (Computation s,9) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,9) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,10) . (IC SCM+FSA ) = insloc 10 & (Computation s,10) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,10) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,11) . (IC SCM+FSA ) = insloc 11 & (Computation s,11) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,11) . (fsloc 0 ) = s . (fsloc 0 ) & (Computation s,11) . (intloc 1) = len (s . (fsloc 0 )) & (Computation s,11) . (intloc 2) = s . (intloc 0 ) & (Computation s,11) . (intloc 3) = s . (intloc 0 ) & (Computation s,11) . (intloc 4) = s . (intloc 0 ) & (Computation s,11) . (intloc 5) = s . (intloc 0 ) & (Computation s,11) . (intloc 6) = s . (intloc 0 ) )
Lm4:
((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )) does_not_destroy intloc (1 + 1)
Lm5:
Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) is good InitHalting Program of SCM+FSA
Lm6:
((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )) does_not_destroy intloc (0 + 1)
Lm7:
((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))) ';' (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))) does_not_destroy intloc (0 + 1)
Lm8:
((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))) ';' (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))) is good InitHalting Program of SCM+FSA
by Lm5;
Lm9:
Times (intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))) ';' (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))))) is good InitHalting Program of SCM+FSA
theorem Th64: :: SCMBSORT:64
Lm10:
for s being State of SCM+FSA holds
( ( s . (intloc (5 + 1)) > 0 implies (IExec (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )),s) . (fsloc 0 ) = ((s . (fsloc 0 )) +* (abs (s . (intloc (2 + 1)))),((s . (fsloc 0 )) /. (abs (s . (intloc (3 + 1)))))) +* (abs (s . (intloc (3 + 1)))),(s . (intloc (4 + 1))) ) & ( s . (intloc (5 + 1)) <= 0 implies (IExec (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )),s) . (fsloc 0 ) = s . (fsloc 0 ) ) )
Lm11:
for s being State of SCM+FSA holds (IExec (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )),s) . (intloc (2 + 1)) = s . (intloc (2 + 1))
Lm12:
for s being State of SCM+FSA st s . (intloc (2 + 1)) <= len (s . (fsloc 0 )) & s . (intloc (2 + 1)) >= 2 holds
( (IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 1 & s . (fsloc 0 ),(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (fsloc 0 ) are_fiberwise_equipotent & ( (s . (fsloc 0 )) . (s . (intloc (2 + 1))) = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (fsloc 0 )) . (s . (intloc (2 + 1))) or (s . (fsloc 0 )) . (s . (intloc (2 + 1))) = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (fsloc 0 )) . ((s . (intloc (2 + 1))) - 1) ) & ( (s . (fsloc 0 )) . (s . (intloc (2 + 1))) = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (fsloc 0 )) . (s . (intloc (2 + 1))) or (s . (fsloc 0 )) . ((s . (intloc (2 + 1))) - 1) = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (fsloc 0 )) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0 )) . (s . (intloc (2 + 1))) = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (fsloc 0 )) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0 )) . ((s . (intloc (2 + 1))) - 1) = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (fsloc 0 )) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0 )) holds
(s . (fsloc 0 )) . k = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (fsloc 0 )) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (fsloc 0 )) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),s) . (fsloc 0 )) . (s . (intloc (2 + 1))) & x1 >= x2 ) )
Lm13:
for s being State of SCM+FSA st s . (intloc (1 + 1)) >= 0 & s . (intloc (1 + 1)) < s . (intloc (2 + 1)) & s . (intloc (2 + 1)) <= len (s . (fsloc 0 )) holds
ex k being Element of NAT st
( k <= s . (intloc (2 + 1)) & k >= (s . (intloc (2 + 1))) - (s . (intloc (1 + 1))) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),s) . (fsloc 0 )) . k = (s . (fsloc 0 )) . (s . (intloc (2 + 1))) )
Lm14:
for k being Element of NAT
for t being State of SCM+FSA st k = t . (intloc (1 + 1)) & k < t . (intloc (2 + 1)) & t . (intloc (2 + 1)) <= len (t . (fsloc 0 )) holds
( t . (fsloc 0 ),(IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 ) are_fiberwise_equipotent & ( for m being Element of NAT st ( ( m < (t . (intloc (2 + 1))) - k & m >= 1 ) or ( m > t . (intloc (2 + 1)) & m in dom (t . (fsloc 0 )) ) ) holds
(t . (fsloc 0 )) . m = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m ) & ( for m being Element of NAT st m >= (t . (intloc (2 + 1))) - k & m <= t . (intloc (2 + 1)) holds
ex x1, x2 being Integer st
( x1 = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . ((t . (intloc (2 + 1))) - k) & x2 = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m & x1 >= x2 ) ) & ( for i being Element of NAT st i >= (t . (intloc (2 + 1))) - k & i <= t . (intloc (2 + 1)) holds
ex n being Element of NAT st
( n >= (t . (intloc (2 + 1))) - k & n <= t . (intloc (2 + 1)) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . i = (t . (fsloc 0 )) . n ) ) )
Lm15:
for s being State of SCM+FSA holds
( (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (intloc (1 + 1)) = (s . (intloc (0 + 1))) - 1 & (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (intloc (2 + 1)) = len (s . (fsloc 0 )) & (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (fsloc 0 ) = s . (fsloc 0 ) )
Lm16:
for s being State of SCM+FSA st s . (intloc (0 + 1)) = len (s . (fsloc 0 )) holds
( s . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))) ';' (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))))),s) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))) ';' (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))))),s) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))) ';' (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))))),s) . (fsloc 0 )) . j holds
x1 >= x2 ) )
theorem Th65: :: SCMBSORT:65
theorem Th66: :: SCMBSORT:66
theorem Th67: :: SCMBSORT:67
theorem Th68: :: SCMBSORT:68
theorem :: SCMBSORT:69