begin
LL:
card (Stop SCM+FSA) = 1
by COMPOS_1:46;
KK:
(Stop SCM+FSA) . 0 = halt SCM+FSA
by AFINSQ_1:38;
JJ:
0 in dom (Stop SCM+FSA)
by COMPOS_1:45;
theorem Th1:
theorem Th2:
definition
let a be
Int-Location ;
let I be
Program of
SCM+FSA;
func while=0 (
a,
I)
-> Program of
SCM+FSA equals
(if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0));
correctness
coherence
(if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)) is Program of SCM+FSA;
func while>0 (
a,
I)
-> Program of
SCM+FSA equals
(if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0));
correctness
coherence
(if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)) is Program of SCM+FSA;
end;
:: deftheorem defines while=0 SCMFSA_9:def 1 :
for a being Int-Location
for I being Program of SCM+FSA holds while=0 (a,I) = (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0));
:: deftheorem defines while>0 SCMFSA_9:def 2 :
for a being Int-Location
for I being Program of SCM+FSA holds while>0 (a,I) = (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0));
theorem Th3:
:: deftheorem defines while<0 SCMFSA_9:def 3 :
for a being Int-Location
for I being Program of SCM+FSA holds while<0 (a,I) = (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) +* (((card I) + 4) .--> (goto 0));
theorem Th4:
theorem Th5:
theorem
theorem
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem Th19:
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_on s &
I is_halting_on s &
k < LifeSpan (
(ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),
(s +* (I +* (Start-At (0,SCM+FSA))))) &
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + k))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) + 4 &
DataPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + k))) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) holds
(
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + k) + 1))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) + 4 &
DataPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + k) + 1))) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) )
theorem Th20:
for
a being
Int-Location for
I being
Program of
SCM+FSA for
s being
State of
SCM+FSA st
I is_closed_on s &
I is_halting_on s &
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) + 4 holds
CurInstr (
(ProgramPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))))),
(Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))))
= goto ((card I) + 4)
theorem Th21:
theorem Th22:
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_on s &
I is_halting_on s &
s . a = 0 holds
(
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) = 0 & ( for
k being
Element of
NAT st
k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 holds
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) ) )
set sl0 = Start-At (0,SCM+FSA);
definition
let s be
State of
SCM+FSA;
let I be
Program of
SCM+FSA;
let a be
read-write Int-Location ;
deffunc H1(
Nat,
State of
SCM+FSA)
-> set =
Comput (
(ProgramPart ($2 +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),
($2 +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),
((LifeSpan ((ProgramPart ($2 +* (I +* (Start-At (0,SCM+FSA))))),($2 +* (I +* (Start-At (0,SCM+FSA)))))) + 3));
deffunc H2(
Nat,
State of
SCM+FSA)
-> Element of
product the
Object-Kind of
SCM+FSA =
down (Comput ((ProgramPart ($2 +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),($2 +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ($2 +* (I +* (Start-At (0,SCM+FSA))))),($2 +* (I +* (Start-At (0,SCM+FSA)))))) + 3)));
func StepWhile=0 (
a,
I,
s)
-> Function of
NAT,
(product the Object-Kind of SCM+FSA) means :
Def4:
(
it . 0 = s & ( for
i being
Nat holds
it . (i + 1) = Comput (
(ProgramPart ((it . i) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),
((it . i) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),
((LifeSpan ((ProgramPart ((it . i) +* (I +* (Start-At (0,SCM+FSA))))),((it . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 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 ((ProgramPart ((b1 . i) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),((b1 . i) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ((b1 . i) +* (I +* (Start-At (0,SCM+FSA))))),((b1 . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 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 ((ProgramPart ((b1 . i) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),((b1 . i) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ((b1 . i) +* (I +* (Start-At (0,SCM+FSA))))),((b1 . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 3)) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Comput ((ProgramPart ((b2 . i) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),((b2 . i) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ((b2 . i) +* (I +* (Start-At (0,SCM+FSA))))),((b2 . i) +* (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 SCM+FSA
for a being read-write Int-Location
for b4 being Function of NAT,(product the Object-Kind of SCM+FSA) holds
( b4 = StepWhile=0 (a,I,s) iff ( b4 . 0 = s & ( for i being Nat holds b4 . (i + 1) = Comput ((ProgramPart ((b4 . i) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),((b4 . i) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ((b4 . i) +* (I +* (Start-At (0,SCM+FSA))))),((b4 . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 3)) ) ) );
theorem
canceled;
theorem
canceled;
theorem Th25:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th29:
theorem Th30:
for
I being
Program of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA holds
(StepWhile=0 (a,I,s)) . (0 + 1) = Comput (
(ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),
(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),
((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))
theorem Th31:
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,I,s)) . k) = 0 &
(StepWhile=0 (a,I,s)) . k = Comput (
(ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),
(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),
n) holds
(
(StepWhile=0 (a,I,s)) . k = ((StepWhile=0 (a,I,s)) . k) +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))) &
(StepWhile=0 (a,I,s)) . (k + 1) = Comput (
(ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),
(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),
(n + ((LifeSpan ((ProgramPart (((StepWhile=0 (a,I,s)) . k) +* (I +* (Start-At (0,SCM+FSA))))),(((StepWhile=0 (a,I,s)) . k) +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) )
theorem Th32:
for
I being
Program of
SCM+FSA 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,s)) . k &
I is_halting_on (StepWhile=0 (a,I,s)) . k ) ) & ex
f being
Function of
(product the Object-Kind of SCM+FSA),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile=0 (a,I,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,s)) . k) or
f . ((StepWhile=0 (a,I,s)) . k) = 0 ) & (
f . ((StepWhile=0 (a,I,s)) . k) = 0 implies
((StepWhile=0 (a,I,s)) . k) . a <> 0 ) & (
((StepWhile=0 (a,I,s)) . k) . a <> 0 implies
f . ((StepWhile=0 (a,I,s)) . k) = 0 ) ) holds
(
while=0 (
a,
I)
is_halting_on s &
while=0 (
a,
I)
is_closed_on s )
theorem Th33:
for
I being
parahalting 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
Nat holds
( (
f . ((StepWhile=0 (a,I,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,s)) . k) or
f . ((StepWhile=0 (a,I,s)) . k) = 0 ) & (
f . ((StepWhile=0 (a,I,s)) . k) = 0 implies
((StepWhile=0 (a,I,s)) . k) . a <> 0 ) & (
((StepWhile=0 (a,I,s)) . k) . a <> 0 implies
f . ((StepWhile=0 (a,I,s)) . k) = 0 ) ) holds
(
while=0 (
a,
I)
is_halting_on s &
while=0 (
a,
I)
is_closed_on s )
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
theorem Th43:
theorem Th44:
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_on s &
I is_halting_on s &
k < LifeSpan (
(ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),
(s +* (I +* (Start-At (0,SCM+FSA))))) &
IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + k))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) + 4 &
DataPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + k))) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) holds
(
IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + k) + 1))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) + 4 &
DataPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + k) + 1))) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) )
theorem Th45:
for
a being
Int-Location for
I being
Program of
SCM+FSA for
s being
State of
SCM+FSA st
I is_closed_on s &
I is_halting_on s &
IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) + 4 holds
CurInstr (
(ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))))),
(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))))
= goto ((card I) + 4)
theorem Th46:
theorem Th47:
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_on s &
I is_halting_on s &
s . a > 0 holds
(
IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) = 0 & ( for
k being
Element of
NAT st
k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 holds
IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while>0 (a,I)) ) )
set sl0 = Start-At (0,SCM+FSA);
definition
let s be
State of
SCM+FSA;
let I be
Program of
SCM+FSA;
let a be
read-write Int-Location ;
deffunc H1(
Nat,
Element of
product the
Object-Kind of
SCM+FSA)
-> set =
Comput (
(ProgramPart ($2 +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),
($2 +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),
((LifeSpan ((ProgramPart ($2 +* (I +* (Start-At (0,SCM+FSA))))),($2 +* (I +* (Start-At (0,SCM+FSA)))))) + 3));
deffunc H2(
Nat,
Element of
product the
Object-Kind of
SCM+FSA)
-> Element of
product the
Object-Kind of
SCM+FSA =
down (Comput ((ProgramPart ($2 +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),($2 +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ($2 +* (I +* (Start-At (0,SCM+FSA))))),($2 +* (I +* (Start-At (0,SCM+FSA)))))) + 3)));
func StepWhile>0 (
a,
I,
s)
-> Function of
NAT,
(product the Object-Kind of SCM+FSA) means :
Def5:
(
it . 0 = s & ( for
i being
Nat holds
it . (i + 1) = Comput (
(ProgramPart ((it . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),
((it . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),
((LifeSpan ((ProgramPart ((it . i) +* (I +* (Start-At (0,SCM+FSA))))),((it . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 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 ((ProgramPart ((b1 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((b1 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ((b1 . i) +* (I +* (Start-At (0,SCM+FSA))))),((b1 . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 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 ((ProgramPart ((b1 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((b1 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ((b1 . i) +* (I +* (Start-At (0,SCM+FSA))))),((b1 . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 3)) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Comput ((ProgramPart ((b2 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((b2 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ((b2 . i) +* (I +* (Start-At (0,SCM+FSA))))),((b2 . i) +* (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 SCM+FSA
for a being read-write Int-Location
for b4 being Function of NAT,(product the Object-Kind of SCM+FSA) holds
( b4 = StepWhile>0 (a,I,s) iff ( b4 . 0 = s & ( for i being Nat holds b4 . (i + 1) = Comput ((ProgramPart ((b4 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((b4 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ((b4 . i) +* (I +* (Start-At (0,SCM+FSA))))),((b4 . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 3)) ) ) );
theorem
canceled;
theorem
canceled;
theorem Th50:
theorem Th51:
for
I being
Program of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA holds
(StepWhile>0 (a,I,s)) . (0 + 1) = Comput (
(ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),
(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),
((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))
theorem Th52:
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,I,s)) . k) = 0 &
(StepWhile>0 (a,I,s)) . k = Comput (
(ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),
(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),
n) holds
(
(StepWhile>0 (a,I,s)) . k = ((StepWhile>0 (a,I,s)) . k) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) &
(StepWhile>0 (a,I,s)) . (k + 1) = Comput (
(ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),
(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),
(n + ((LifeSpan ((ProgramPart (((StepWhile>0 (a,I,s)) . k) +* (I +* (Start-At (0,SCM+FSA))))),(((StepWhile>0 (a,I,s)) . k) +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) )
theorem Th53:
for
I being
Program of
SCM+FSA 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,s)) . k &
I is_halting_on (StepWhile>0 (a,I,s)) . k ) ) & ex
f being
Function of
(product the Object-Kind of SCM+FSA),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile>0 (a,I,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,s)) . k) or
f . ((StepWhile>0 (a,I,s)) . k) = 0 ) & (
f . ((StepWhile>0 (a,I,s)) . k) = 0 implies
((StepWhile>0 (a,I,s)) . k) . a <= 0 ) & (
((StepWhile>0 (a,I,s)) . k) . a <= 0 implies
f . ((StepWhile>0 (a,I,s)) . k) = 0 ) ) holds
(
while>0 (
a,
I)
is_halting_on s &
while>0 (
a,
I)
is_closed_on s )
theorem Th54:
for
I being
parahalting 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
Nat holds
( (
f . ((StepWhile>0 (a,I,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,s)) . k) or
f . ((StepWhile>0 (a,I,s)) . k) = 0 ) & (
f . ((StepWhile>0 (a,I,s)) . k) = 0 implies
((StepWhile>0 (a,I,s)) . k) . a <= 0 ) & (
((StepWhile>0 (a,I,s)) . k) . a <= 0 implies
f . ((StepWhile>0 (a,I,s)) . k) = 0 ) ) holds
(
while>0 (
a,
I)
is_halting_on s &
while>0 (
a,
I)
is_closed_on s )
theorem