begin
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
canceled;
theorem Th23:
theorem
canceled;
theorem Th25:
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 (Comput (ProgramPart s1),s1,j) in dom p &
IC (Comput (ProgramPart s2),s2,j) in dom p ) ) &
(Comput (ProgramPart s1),s1,k) . (IC SCM+FSA ) = (Comput (ProgramPart s2),s2,k) . (IC SCM+FSA ) &
(Comput (ProgramPart s1),s1,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Comput (ProgramPart s2),s2,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) holds
(
(Comput (ProgramPart s1),s1,i) . (IC SCM+FSA ) = (Comput (ProgramPart s2),s2,i) . (IC SCM+FSA ) &
(Comput (ProgramPart s1),s1,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Comput (ProgramPart s2),s2,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) )
theorem Th26:
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 (Comput (ProgramPart s1),s1,j) in dom p &
IC (Comput (ProgramPart s2),s2,j) in dom p ) ) &
(Comput (ProgramPart s1),s1,k) . (IC SCM+FSA ) = (Comput (ProgramPart s2),s2,k) . (IC SCM+FSA ) &
(Comput (ProgramPart s1),s1,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput (ProgramPart s2),s2,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) holds
(
(Comput (ProgramPart s1),s1,i) . (IC SCM+FSA ) = (Comput (ProgramPart s2),s2,i) . (IC SCM+FSA ) &
(Comput (ProgramPart s1),s1,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput (ProgramPart s2),s2,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )
theorem
canceled;
theorem
canceled;
theorem Th29:
theorem Th30:
theorem Th31:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem
for
ic being
Instruction of
SCM+FSA for
f being
FinSeq-Location for
a,
b being
Int-Location for
la being
Element of
NAT 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:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
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 2
by AMI_3:52;
Lm2:
intloc 0 <> intloc 4
by AMI_3:52;
Lm3:
intloc 0 <> intloc 5
by AMI_3:52;
Lm4:
intloc 0 <> intloc 6
by AMI_3:52;
Lm5:
intloc 1 <> intloc 2
by AMI_3:52;
Lm6:
intloc 1 <> intloc 3
by AMI_3:52;
Lm7:
intloc 1 <> intloc 4
by AMI_3:52;
Lm8:
intloc 1 <> intloc 5
by AMI_3:52;
Lm9:
intloc 1 <> intloc 6
by AMI_3:52;
Lm10:
intloc 2 <> intloc 3
by AMI_3:52;
Lm11:
intloc 2 <> intloc 4
by AMI_3:52;
Lm12:
intloc 2 <> intloc 5
by AMI_3:52;
Lm13:
intloc 2 <> intloc 6
by AMI_3:52;
Lm14:
intloc 3 <> intloc 4
by AMI_3:52;
Lm15:
intloc 3 <> intloc 5
by AMI_3:52;
Lm16:
intloc 3 <> intloc 6
by AMI_3:52;
Lm17:
intloc 4 <> intloc 5
by AMI_3:52;
Lm18:
intloc 4 <> intloc 6
by AMI_3:52;
Lm19:
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
(((((((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 :
Bubble-Sort-Algorithm = bubble-sort (fsloc 0 );
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:
theorem Th59:
definition
func Sorting-Function -> PartFunc of
(FinPartSt SCM+FSA ),
(FinPartSt SCM+FSA ) means :
Def3:
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 :
for b1 being PartFunc of (FinPartSt SCM+FSA ),(FinPartSt SCM+FSA ) holds
( b1 = Sorting-Function iff 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 ) ) );
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
Lm20:
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Bubble-Sort-Algorithm c= P holds
( P . 0 = (intloc 2) := (intloc 0 ) & P . 1 = goto 2 & P . 2 = (intloc 3) := (intloc 0 ) & P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0 ) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0 ) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0 ) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0 ) & P . 11 = goto 12 )
Lm21:
for s being 0 -started State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Bubble-Sort-Algorithm c= P holds
( (Comput P,s,1) . (IC SCM+FSA ) = 1 & (Comput P,s,1) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,1) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,2) . (IC SCM+FSA ) = 2 & (Comput P,s,2) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,2) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,3) . (IC SCM+FSA ) = 3 & (Comput P,s,3) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,3) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,4) . (IC SCM+FSA ) = 4 & (Comput P,s,4) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,4) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,5) . (IC SCM+FSA ) = 5 & (Comput P,s,5) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,5) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,6) . (IC SCM+FSA ) = 6 & (Comput P,s,6) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,6) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,7) . (IC SCM+FSA ) = 7 & (Comput P,s,7) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,7) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,8) . (IC SCM+FSA ) = 8 & (Comput P,s,8) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,8) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,9) . (IC SCM+FSA ) = 9 & (Comput P,s,9) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,9) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,10) . (IC SCM+FSA ) = 10 & (Comput P,s,10) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,10) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,11) . (IC SCM+FSA ) = 11 & (Comput P,s,11) . (intloc 0 ) = s . (intloc 0 ) & (Comput P,s,11) . (fsloc 0 ) = s . (fsloc 0 ) & (Comput P,s,11) . (intloc 1) = len (s . (fsloc 0 )) & (Comput P,s,11) . (intloc 2) = s . (intloc 0 ) & (Comput P,s,11) . (intloc 3) = s . (intloc 0 ) & (Comput P,s,11) . (intloc 4) = s . (intloc 0 ) & (Comput P,s,11) . (intloc 5) = s . (intloc 0 ) & (Comput P,s,11) . (intloc 6) = s . (intloc 0 ) )
Lm22:
not ((((((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 )) destroysdestroy intloc (1 + 1)
Lm23:
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
Lm24:
not ((((((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 )) destroysdestroy intloc (0 + 1)
Lm25:
not ((((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 )))) destroysdestroy intloc (0 + 1)
Lm26:
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
Lm27:
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 ) ) )
Lm28:
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))
Lm29:
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 ) )
Lm30:
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))) )
Lm31:
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 ) ) )
Lm32:
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 ) )
Lm33:
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:
theorem Th66:
theorem Th67:
theorem Th68:
theorem