begin
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem Th6:
theorem Th7:
theorem
canceled;
theorem
canceled;
theorem Th10:
theorem Th11:
for
P1,
P2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s1,
s2 being
State of
SCM+FSA for
I being
InitHalting Program of
SCM+FSA st
Initialized I c= s1 &
Initialized I c= s2 &
I c= P1 &
I c= P2 &
s1,
s2 equal_outside NAT holds
for
k being
Element of
NAT holds
(
Comput (
P1,
s1,
k),
Comput (
P2,
s2,
k)
equal_outside NAT &
CurInstr (
P1,
(Comput (P1,s1,k)))
= CurInstr (
P2,
(Comput (P2,s2,k))) )
theorem Th12:
theorem Th13:
theorem Th14:
begin
theorem
canceled;
theorem Th16:
theorem
for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
a being
Int-Location for
I being
Program of
SCM+FSA for
s being
State of
SCM+FSA for
k being
Element of
NAT st
I is_closed_onInit s,
P &
I is_halting_onInit s,
P &
k < LifeSpan (
(P +* I),
(s +* (Initialized I))) &
IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),(1 + k))) = (IC (Comput ((P +* I),(s +* (Initialized I)),k))) + 4 &
DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialized I)),k)) holds
(
IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialized I)),(k + 1)))) + 4 &
DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialized I)),(k + 1))) )
theorem
for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
a being
Int-Location for
I being
Program of
SCM+FSA for
s being
State of
SCM+FSA st
I is_closed_onInit s,
P &
I is_halting_onInit s,
P &
IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),(1 + (LifeSpan ((P +* I),(s +* (Initialized I))))))) = (IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))) + 4 holds
CurInstr (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),(1 + (LifeSpan ((P +* I),(s +* (Initialized I))))))))
= goto ((card I) + 4)
theorem Th19:
for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA for
a being
read-write Int-Location st
I is_closed_onInit s,
P &
I is_halting_onInit s,
P &
s . a > 0 holds
(
IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) = 0 & ( for
k being
Element of
NAT st
k <= (LifeSpan ((P +* I),(s +* (Initialized I)))) + 3 holds
IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),k)) in dom (while>0 (a,I)) ) )
theorem
theorem Th21:
for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA for
a being
read-write Int-Location st
I is_closed_onInit s,
P &
I is_halting_onInit s,
P &
s . a > 0 holds
(
IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) = 0 &
DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) = DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) )
theorem
for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I being
InitHalting Program of
SCM+FSA for
a being
read-write Int-Location st
s . a > 0 holds
ex
s2 being
State of
SCM+FSA ex
k being
Element of
NAT st
(
s2 = s +* (Initialized (while>0 (a,I))) &
k = (LifeSpan ((P +* I),(s +* (Initialized I)))) + 3 &
IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for
b being
Int-Location holds
(Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for
f being
FinSeq-Location holds
(Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) )
definition
let s be
State of
SCM+FSA;
let I be
Program of
SCM+FSA;
let a be
read-write Int-Location ;
let P be the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
deffunc H1(
Nat,
Element of
product the
Object-Kind of
SCM+FSA)
-> set =
Comput (
(P +* (while>0 (a,I))),
($2 +* (Initialized (while>0 (a,I)))),
((LifeSpan (((P +* (while>0 (a,I))) +* I),($2 +* (Initialized I)))) + 3));
deffunc H2(
Nat,
Element of
product the
Object-Kind of
SCM+FSA)
-> Element of
product the
Object-Kind of
SCM+FSA =
down H1($1,$2);
func StepWhile>0 (
a,
P,
s,
I)
-> Function of
NAT,
(product the Object-Kind of SCM+FSA) means :
Def1:
(
it . 0 = s & ( for
i being
Nat holds
it . (i + 1) = Comput (
(P +* (while>0 (a,I))),
((it . i) +* (Initialized (while>0 (a,I)))),
((LifeSpan (((P +* (while>0 (a,I))) +* I),((it . i) +* (Initialized I)))) + 3)) ) );
existence
ex b1 being Function of NAT,(product the Object-Kind of SCM+FSA) st
( b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b1 . i) +* (Initialized (while>0 (a,I)))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b1 . i) +* (Initialized I)))) + 3)) ) )
uniqueness
for b1, b2 being Function of NAT,(product the Object-Kind of SCM+FSA) st b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b1 . i) +* (Initialized (while>0 (a,I)))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b1 . i) +* (Initialized I)))) + 3)) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b2 . i) +* (Initialized (while>0 (a,I)))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b2 . i) +* (Initialized I)))) + 3)) ) holds
b1 = b2
end;
:: deftheorem Def1 defines StepWhile>0 SCMISORT:def 1 :
for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for b5 being Function of NAT,(product the Object-Kind of SCM+FSA) holds
( b5 = StepWhile>0 (a,P,s,I) iff ( b5 . 0 = s & ( for i being Nat holds b5 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b5 . i) +* (Initialized (while>0 (a,I)))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b5 . i) +* (Initialized I)))) + 3)) ) ) );
theorem
canceled;
theorem
canceled;
theorem
theorem Th26:
theorem Th27:
for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
I being
Program of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA for
k,
n being
Element of
NAT st
IC ((StepWhile>0 (a,P,s,I)) . k) = 0 &
(StepWhile>0 (a,P,s,I)) . k = Comput (
(P +* (while>0 (a,I))),
(s +* (Initialized (while>0 (a,I)))),
n) &
((StepWhile>0 (a,P,s,I)) . k) . (intloc 0) = 1 holds
(
(StepWhile>0 (a,P,s,I)) . k = ((StepWhile>0 (a,P,s,I)) . k) +* (Initialized (while>0 (a,I))) &
(StepWhile>0 (a,P,s,I)) . (k + 1) = Comput (
(P +* (while>0 (a,I))),
(s +* (Initialized (while>0 (a,I)))),
(n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,P,s,I)) . k) +* (Initialized I)))) + 3))) )
theorem
for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
I being
Program of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st ex
f being
Function of
(product the Object-Kind of SCM+FSA),
NAT st
for
k being
Element of
NAT holds
( (
f . ((StepWhile>0 (a,P,s,I)) . k) <> 0 implies (
f . ((StepWhile>0 (a,P,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,P,s,I)) . k) &
I is_closed_onInit (StepWhile>0 (a,P,s,I)) . k,
P +* (while>0 (a,I)) &
I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,
P +* (while>0 (a,I)) ) ) &
((StepWhile>0 (a,P,s,I)) . (k + 1)) . (intloc 0) = 1 & (
f . ((StepWhile>0 (a,P,s,I)) . k) = 0 implies
((StepWhile>0 (a,P,s,I)) . k) . a <= 0 ) & (
((StepWhile>0 (a,P,s,I)) . k) . a <= 0 implies
f . ((StepWhile>0 (a,P,s,I)) . k) = 0 ) ) holds
(
while>0 (
a,
I)
is_halting_onInit s,
P &
while>0 (
a,
I)
is_closed_onInit s,
P )
theorem Th29:
theorem Th30:
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
begin
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;
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 insert-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)) ';' (SubFrom ((intloc 1),(intloc 0)))) ';' (Times ((intloc 1),(((((((((intloc 2) :=len f) ';' (SubFrom ((intloc 2),(intloc 1)))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo ((intloc 3),(intloc 0)))) ';' ((intloc 6) := (f,(intloc 3)))) ';' (SubFrom ((intloc 4),(intloc 4)))) ';' (while>0 ((intloc 2),((((intloc 5) := (f,(intloc 2))) ';' (SubFrom ((intloc 5),(intloc 6)))) ';' (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ';' (SubFrom ((intloc 2),(intloc 0)))))))))) ';' (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 2)))) ';' ((intloc 6) := (f,(intloc 3)))) ';' ((f,(intloc 2)) := (intloc 6))) ';' ((f,(intloc 3)) := (intloc 5))))))));
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)) ';' (SubFrom ((intloc 1),(intloc 0)))) ';' (Times ((intloc 1),(((((((((intloc 2) :=len f) ';' (SubFrom ((intloc 2),(intloc 1)))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo ((intloc 3),(intloc 0)))) ';' ((intloc 6) := (f,(intloc 3)))) ';' (SubFrom ((intloc 4),(intloc 4)))) ';' (while>0 ((intloc 2),((((intloc 5) := (f,(intloc 2))) ';' (SubFrom ((intloc 5),(intloc 6)))) ';' (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ';' (SubFrom ((intloc 2),(intloc 0)))))))))) ';' (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 2)))) ';' ((intloc 6) := (f,(intloc 3)))) ';' ((f,(intloc 2)) := (intloc 6))) ';' ((f,(intloc 3)) := (intloc 5)))))))) is Program of SCM+FSA
;
end;
:: deftheorem defines insert-sort SCMISORT:def 2 :
for f being FinSeq-Location holds insert-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)) ';' (SubFrom ((intloc 1),(intloc 0)))) ';' (Times ((intloc 1),(((((((((intloc 2) :=len f) ';' (SubFrom ((intloc 2),(intloc 1)))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo ((intloc 3),(intloc 0)))) ';' ((intloc 6) := (f,(intloc 3)))) ';' (SubFrom ((intloc 4),(intloc 4)))) ';' (while>0 ((intloc 2),((((intloc 5) := (f,(intloc 2))) ';' (SubFrom ((intloc 5),(intloc 6)))) ';' (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ';' (SubFrom ((intloc 2),(intloc 0)))))))))) ';' (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 2)))) ';' ((intloc 6) := (f,(intloc 3)))) ';' ((f,(intloc 2)) := (intloc 6))) ';' ((f,(intloc 3)) := (intloc 5))))))));
:: deftheorem defines Insert-Sort-Algorithm SCMISORT:def 3 :
Insert-Sort-Algorithm = insert-sort (fsloc 0);
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
Lm1:
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Insert-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 )
set f0 = 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 i1 = (intloc (1 + 1)) := (intloc (2 + 1));
set i2 = SubFrom ((intloc (2 + 1)),(intloc 0));
set i3 = (intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)));
set i4 = (intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1)));
set i5 = ((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1));
set i6 = ((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1));
set body3 = ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)));
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 T3 = Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))));
set m0 = SubFrom ((intloc (1 + 1)),(intloc (1 + 1)));
set m1 = Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))));
set m2 = AddTo ((intloc (3 + 1)),(intloc 0));
set m3 = SubFrom ((intloc (1 + 1)),(intloc 0));
set IF = if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))));
set n1 = (intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)));
set n2 = SubFrom ((intloc (4 + 1)),(intloc (5 + 1)));
set body2 = (((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))));
set t1 = (intloc (1 + 1)) :=len (fsloc 0);
set t2 = SubFrom ((intloc (1 + 1)),(intloc (0 + 1)));
set t3 = (intloc (2 + 1)) := (intloc (1 + 1));
set t4 = AddTo ((intloc (2 + 1)),(intloc 0));
set t5 = (intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1)));
set t6 = SubFrom ((intloc (3 + 1)),(intloc (3 + 1)));
set Wg = while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))));
set t16 = ((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))));
set body1 = ((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ';' (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))))))) ';' (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))))));
set WM = (((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) ';' ((intloc 6) := (intloc 0));
set j1 = (intloc (0 + 1)) :=len (fsloc 0);
set j2 = SubFrom ((intloc (0 + 1)),(intloc 0));
Lm2:
for s being 0 -started State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Insert-Sort-Algorithm c= P holds
( ( for k being Element of NAT st k > 0 & k < 12 holds
( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (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) )
Lm3:
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA holds
( ( s . (intloc (4 + 1)) > 0 implies (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (1 + 1)) = 0 ) & ( s . (intloc (4 + 1)) <= 0 implies (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 ) )
Lm4:
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds
( (IExec (((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (intloc (1 + 1)) < s . (intloc (1 + 1)) or (IExec (((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (intloc (1 + 1)) <= 0 )
then Lm5:
while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))))) is InitHalting good Program of SCM+FSA
by Th30;
Lm6:
not ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))) destroys intloc (3 + 1)
Lm7:
not ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))) destroys intloc (0 + 1)
Lm8:
not (((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))) destroys intloc (0 + 1)
Lm9:
not ((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ';' (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))))))) ';' (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))) destroys intloc (0 + 1)
Lm10:
Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))))) is InitHalting good Program of SCM+FSA
Lm11:
((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ';' (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))))))) ';' (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))) is InitHalting good Program of SCM+FSA
Lm12:
Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ';' (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))))))) ';' (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))))) is InitHalting good Program of SCM+FSA
theorem
Lm13:
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA holds (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (fsloc 0) = s . (fsloc 0)
Lm14:
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA holds
( ( s . (intloc (4 + 1)) > 0 implies (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) & ( s . (intloc (4 + 1)) <= 0 implies (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) )
Lm15:
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a being read-write Int-Location
for s being State of SCM+FSA st a <> intloc (3 + 1) & a <> intloc (1 + 1) holds
(IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . a = s . a
Lm16:
for t being State of SCM+FSA
for Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT st t . (intloc (1 + 1)) >= 1 & t . (intloc (1 + 1)) <= len (t . (fsloc 0)) holds
( (IExec (((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))),Q,t)) . (intloc (2 + 1)) = t . (intloc (2 + 1)) & (IExec (((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))),Q,t)) . (intloc (5 + 1)) = t . (intloc (5 + 1)) & (IExec (((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))),Q,t)) . (fsloc 0) = t . (fsloc 0) & ex x1 being Integer st
( x1 = (t . (fsloc 0)) . (t . (intloc (1 + 1))) & ( x1 - (t . (intloc (5 + 1))) > 0 implies ( (IExec (((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))),Q,t)) . (intloc (1 + 1)) = 0 & (IExec (((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))),Q,t)) . (intloc (3 + 1)) = t . (intloc (3 + 1)) ) ) & ( x1 - (t . (intloc (5 + 1))) <= 0 implies ( (IExec (((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))),Q,t)) . (intloc (1 + 1)) = (t . (intloc (1 + 1))) - 1 & (IExec (((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))),Q,t)) . (intloc (3 + 1)) = (t . (intloc (3 + 1))) + 1 ) ) ) )
Lm17:
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for k being Element of NAT
for s being State of SCM+FSA st s . (intloc (1 + 1)) = k & s . (intloc (1 + 1)) <= len (s . (fsloc 0)) holds
( s . (fsloc 0) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (fsloc 0) & s . (intloc (2 + 1)) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (2 + 1)) & ( k = 0 or ex n being Element of NAT ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k & ( k - n >= 1 implies ( x1 = (s . (fsloc 0)) . (k - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Element of NAT st i > k - n & i < k + 1 holds
ex x2 being Integer st
( x2 = (s . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )
Lm18:
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 (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 1 & (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . (fsloc 0) = ((s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs ((s . (intloc (2 + 1))) - 1))))) +* ((abs ((s . (intloc (2 + 1))) - 1)),((s . (fsloc 0)) /. (abs (s . (intloc (2 + 1)))))) )
Lm19:
for k being Element of NAT
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st s . (intloc (3 + 1)) = k & k < s . (intloc (2 + 1)) & s . (intloc (2 + 1)) <= len (s . (fsloc 0)) holds
( s . (fsloc 0),(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . (fsloc 0) are_fiberwise_equipotent & (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - k & ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - k) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - k < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - k holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )
Lm20:
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds
( (IExec ((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (1 + 1)) = (len (s . (fsloc 0))) - (s . (intloc (0 + 1))) & (IExec ((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (2 + 1)) = ((len (s . (fsloc 0))) - (s . (intloc (0 + 1)))) + 1 & (IExec ((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (fsloc 0) = s . (fsloc 0) & (IExec ((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (3 + 1)) = 0 & (IExec ((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (5 + 1)) = (s . (fsloc 0)) /. (abs (((len (s . (fsloc 0))) - (s . (intloc (0 + 1)))) + 1)) )
set T1 = Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ';' (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))))))) ';' (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))))))));
Lm21:
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st s . (intloc (0 + 1)) = (len (s . (fsloc 0))) - 1 holds
( s . (fsloc 0),(IExec ((Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ';' (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))))))) ';' (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))))))))),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)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ';' (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))))))) ';' (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))))))))),P,s)) . (fsloc 0)) . i & x2 = ((IExec ((Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0)) ';' (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ';' (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ';' (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ';' (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ';' (SubFrom ((intloc (1 + 1)),(intloc 0)))))))))) ';' (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem