begin
Lm1:
card (Stop SCM+FSA) = 1
by AFINSQ_1:33;
Lm2:
(Stop SCM+FSA) . 0 = halt SCM+FSA
by AFINSQ_1:34;
Lm3:
0 in dom (Stop SCM+FSA)
by COMPOS_1:3;
set SA0 = Start-At (0,SCM+FSA);
theorem Th19:
for
P being
Instruction-Sequence of
SCM+FSA for
a being
Int-Location for
I being
Program of
for
s being
State of
SCM+FSA for
k being
Element of
NAT st
I is_closed_on s,
P &
I is_halting_on s,
P &
k < LifeSpan (
(P +* I),
(Initialize s)) &
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 &
DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
(
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 4 &
DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )
theorem Th20:
for
P being
Instruction-Sequence of
SCM+FSA for
a being
Int-Location for
I being
Program of
for
s being
State of
SCM+FSA st
I is_closed_on s,
P &
I is_halting_on s,
P &
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 4 holds
CurInstr (
(P +* (while=0 (a,I))),
(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))))
= goto ((card I) + 4)
theorem Th22:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I being
Program of
for
a being
read-write Int-Location st
I is_closed_on s,
P &
I is_halting_on s,
P &
s . a = 0 holds
(
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 & ( for
k being
Element of
NAT st
k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )
definition
let s be
State of
SCM+FSA;
let I be
Program of ;
let a be
read-write Int-Location;
let P be
Instruction-Sequence of
SCM+FSA;
deffunc H1(
Nat,
State of
SCM+FSA)
-> set =
Comput (
(P +* (while=0 (a,I))),
($2 +* (Start-At (0,SCM+FSA))),
((LifeSpan (((P +* (while=0 (a,I))) +* I),($2 +* (Start-At (0,SCM+FSA))))) + 3));
deffunc H2(
Nat,
State of
SCM+FSA)
-> Element of
product (the_Values_of SCM+FSA) =
down H1($1,$2);
func StepWhile=0 (
a,
I,
P,
s)
-> Function of
NAT,
(product (the_Values_of SCM+FSA)) means :
Def4:
(
it . 0 = s & ( for
i being
Nat holds
it . (i + 1) = Comput (
(P +* (while=0 (a,I))),
((it . i) +* (Start-At (0,SCM+FSA))),
((LifeSpan (((P +* (while=0 (a,I))) +* I),((it . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) );
existence
ex b1 being Function of NAT,(product (the_Values_of SCM+FSA)) st
( b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while=0 (a,I))),((b1 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while=0 (a,I))) +* I),((b1 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) )
uniqueness
for b1, b2 being Function of NAT,(product (the_Values_of SCM+FSA)) st b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while=0 (a,I))),((b1 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while=0 (a,I))) +* I),((b1 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Comput ((P +* (while=0 (a,I))),((b2 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while=0 (a,I))) +* I),((b2 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) holds
b1 = b2
end;
::
deftheorem Def4 defines
StepWhile=0 SCMFSA_9:def 4 :
for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location
for P being Instruction-Sequence of SCM+FSA
for b5 being Function of NAT,(product (the_Values_of SCM+FSA)) holds
( b5 = StepWhile=0 (a,I,P,s) iff ( b5 . 0 = s & ( for i being Nat holds b5 . (i + 1) = Comput ((P +* (while=0 (a,I))),((b5 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while=0 (a,I))) +* I),((b5 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) ) );
theorem Th26:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
Program of
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,I,P,s)) . k) = 0 &
(StepWhile=0 (a,I,P,s)) . k = Comput (
(P +* (while=0 (a,I))),
(Initialize s),
n) holds
(
(StepWhile=0 (a,I,P,s)) . k = Initialize ((StepWhile=0 (a,I,P,s)) . k) &
(StepWhile=0 (a,I,P,s)) . (k + 1) = Comput (
(P +* (while=0 (a,I))),
(Initialize s),
(n + ((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . k)))) + 3))) )
theorem Th27:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
Program of
for
a being
read-write Int-Location for
s being
State of
SCM+FSA st ( for
k being
Nat holds
(
I is_closed_on (StepWhile=0 (a,I,P,s)) . k,
P +* (while=0 (a,I)) &
I is_halting_on (StepWhile=0 (a,I,P,s)) . k,
P +* (while=0 (a,I)) ) ) & ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & (
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies
((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & (
((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) holds
(
while=0 (
a,
I)
is_halting_on s,
P &
while=0 (
a,
I)
is_closed_on s,
P )
theorem Th28:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
parahalting Program of
for
a being
read-write Int-Location for
s being
State of
SCM+FSA st ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & (
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies
((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & (
((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) holds
(
while=0 (
a,
I)
is_halting_on s,
P &
while=0 (
a,
I)
is_closed_on s,
P )
theorem Th39:
for
P being
Instruction-Sequence of
SCM+FSA for
a being
Int-Location for
I being
Program of
for
s being
State of
SCM+FSA for
k being
Element of
NAT st
I is_closed_on s,
P &
I is_halting_on s,
P &
k < LifeSpan (
(P +* I),
(Initialize s)) &
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 &
DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
(
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 4 &
DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(k + 1))) )
theorem Th40:
for
P being
Instruction-Sequence of
SCM+FSA for
a being
Int-Location for
I being
Program of
for
s being
State of
SCM+FSA st
I is_closed_on s,
P &
I is_halting_on s,
P &
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 4 holds
CurInstr (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))))
= goto ((card I) + 4)
theorem Th42:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I being
Program of
for
a being
read-write Int-Location st
I is_closed_on s,
P &
I is_halting_on s,
P &
s . a > 0 holds
(
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 & ( for
k being
Element of
NAT st
k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) )
definition
let s be
State of
SCM+FSA;
let I be
Program of ;
let a be
read-write Int-Location;
let P be
Instruction-Sequence of
SCM+FSA;
deffunc H1(
Nat,
State of
SCM+FSA)
-> set =
Comput (
(P +* (while>0 (a,I))),
($2 +* (Start-At (0,SCM+FSA))),
((LifeSpan (((P +* (while>0 (a,I))) +* I),($2 +* (Start-At (0,SCM+FSA))))) + 3));
deffunc H2(
Nat,
State of
SCM+FSA)
-> Element of
product (the_Values_of SCM+FSA) =
down H1($1,$2);
func StepWhile>0 (
a,
I,
P,
s)
-> Function of
NAT,
(product (the_Values_of SCM+FSA)) means :
Def5:
(
it . 0 = s & ( for
i being
Nat holds
it . (i + 1) = Comput (
(P +* (while>0 (a,I))),
((it . i) +* (Start-At (0,SCM+FSA))),
((LifeSpan (((P +* (while>0 (a,I))) +* I),((it . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) );
existence
ex b1 being Function of NAT,(product (the_Values_of SCM+FSA)) st
( b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b1 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b1 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) )
uniqueness
for b1, b2 being Function of NAT,(product (the_Values_of SCM+FSA)) st b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b1 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b1 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b2 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b2 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) holds
b1 = b2
end;
::
deftheorem Def5 defines
StepWhile>0 SCMFSA_9:def 5 :
for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location
for P being Instruction-Sequence of SCM+FSA
for b5 being Function of NAT,(product (the_Values_of SCM+FSA)) holds
( b5 = StepWhile>0 (a,I,P,s) iff ( b5 . 0 = s & ( for i being Nat holds b5 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b5 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b5 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) ) );
theorem Th45:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
Program of
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,I,P,s)) . k) = 0 &
(StepWhile>0 (a,I,P,s)) . k = Comput (
(P +* (while>0 (a,I))),
(Initialize s),
n) holds
(
(StepWhile>0 (a,I,P,s)) . k = Initialize ((StepWhile>0 (a,I,P,s)) . k) &
(StepWhile>0 (a,I,P,s)) . (k + 1) = Comput (
(P +* (while>0 (a,I))),
(Initialize s),
(n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,P,s)) . k)))) + 3))) )
theorem Th46:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
Program of
for
a being
read-write Int-Location for
s being
State of
SCM+FSA st ( for
k being
Nat holds
(
I is_closed_on (StepWhile>0 (a,I,P,s)) . k,
P +* (while>0 (a,I)) &
I is_halting_on (StepWhile>0 (a,I,P,s)) . k,
P +* (while>0 (a,I)) ) ) & ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile>0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,P,s)) . k) or
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) & (
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies
((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) & (
((StepWhile>0 (a,I,P,s)) . k) . a <= 0 implies
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) ) holds
(
while>0 (
a,
I)
is_halting_on s,
P &
while>0 (
a,
I)
is_closed_on s,
P )
theorem Th47:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
parahalting Program of
for
a being
read-write Int-Location for
s being
State of
SCM+FSA st ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile>0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,P,s)) . k) or
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) & (
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies
((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) & (
((StepWhile>0 (a,I,P,s)) . k) . a <= 0 implies
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) ) holds
(
while>0 (
a,
I)
is_halting_on s,
P &
while>0 (
a,
I)
is_closed_on s,
P )
:: WHILE>0 Statement