begin
set SA0 = Start-At (0,SCM+FSA);
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
p1,
p2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
i,
k being
Element of
NAT for
t being
FinPartState of
SCM+FSA for
p being
Program of
{INT,(INT *)} for
s1,
s2 being
State of
SCM+FSA st
k <= i &
p c= p1 &
p c= p2 &
dom t c= Int-Locations \/ FinSeq-Locations & ( for
j being
Element of
NAT holds
(
IC (Comput (p1,s1,j)) in dom p &
IC (Comput (p2,s2,j)) in dom p ) ) &
(Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) &
(Comput (p1,s1,k)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Comput (p2,s2,k)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) holds
(
(Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) &
(Comput (p1,s1,i)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) )
theorem Th26:
for
p1,
p2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
i,
k being
Element of
NAT for
p being
Program of
{INT,(INT *)} for
s1,
s2 being
State of
SCM+FSA st
k <= i &
p c= p1 &
p c= p2 & ( for
j being
Element of
NAT holds
(
IC (Comput (p1,s1,j)) in dom p &
IC (Comput (p2,s2,j)) in dom p ) ) &
(Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) &
(Comput (p1,s1,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput (p2,s2,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) holds
(
(Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) &
(Comput (p1,s1,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput (p2,s2,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )
theorem
canceled;
theorem
canceled;
theorem Th29:
theorem Th30:
theorem Th31:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th36:
theorem Th37:
theorem
canceled;
theorem
canceled;
theorem Th40:
theorem Th41:
theorem Th42:
theorem
canceled;
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem
canceled;
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 SCMFSA_2:128;
Lm2:
intloc 0 <> intloc 4
by SCMFSA_2:128;
Lm3:
intloc 0 <> intloc 5
by SCMFSA_2:128;
Lm4:
intloc 0 <> intloc 6
by SCMFSA_2:128;
Lm5:
intloc 1 <> intloc 2
by SCMFSA_2:128;
Lm6:
intloc 1 <> intloc 3
by SCMFSA_2:128;
Lm7:
intloc 1 <> intloc 4
by SCMFSA_2:128;
Lm8:
intloc 1 <> intloc 5
by SCMFSA_2:128;
Lm9:
intloc 1 <> intloc 6
by SCMFSA_2:128;
Lm10:
intloc 2 <> intloc 3
by SCMFSA_2:128;
Lm11:
intloc 2 <> intloc 4
by SCMFSA_2:128;
Lm12:
intloc 2 <> intloc 5
by SCMFSA_2:128;
Lm13:
intloc 2 <> intloc 6
by SCMFSA_2:128;
Lm14:
intloc 3 <> intloc 4
by SCMFSA_2:128;
Lm15:
intloc 3 <> intloc 5
by SCMFSA_2:128;
Lm16:
intloc 3 <> intloc 6
by SCMFSA_2:128;
Lm17:
intloc 4 <> intloc 5
by SCMFSA_2:128;
Lm18:
intloc 4 <> intloc 6
by SCMFSA_2:128;
Lm19:
intloc 5 <> intloc 6
by SCMFSA_2:128;
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
{INT,(INT *)} 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 {INT,(INT *)};
;
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 ) = 1 & (Comput (P,s,1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,2)) . (IC ) = 2 & (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,3)) . (IC ) = 3 & (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 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))) destroys 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 & 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 InitHalting )
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))) destroys 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)))))) destroys 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 & 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 InitHalting )
theorem
Lm27:
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))),p,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))),p,s)) . (fsloc 0) = s . (fsloc 0) ) )
Lm28:
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))),p,s)) . (intloc (2 + 1)) = s . (intloc (2 + 1))
Lm29:
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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)))),p,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)))),p,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)))),p,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)))),p,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)))),p,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)))),p,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)))),p,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)))),p,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)))),p,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)))),p,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)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )
Lm30:
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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)))))),p,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
for q being the Instructions of SCM+FSA -valued ManySortedSet of NAT 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)))))),q,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)))))),q,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)))))),q,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)))))),q,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)))))),q,t)) . (fsloc 0)) . i = (t . (fsloc 0)) . n ) ) )
Lm32:
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))),p,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))),p,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))),p,s)) . (fsloc 0) = s . (fsloc 0) )
Lm33:
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))))))))),p,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))))))))),p,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))))))))),p,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem