begin
theorem Th1:
theorem Th2:
definition
let a be
Int-Location ;
let I be
Program of ;
func while=0 a,
I -> Program of
equals
(if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )));
correctness
coherence
(if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) is Program of ;
func while>0 a,
I -> Program of
equals
(if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )));
correctness
coherence
(if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) is Program of ;
end;
:: deftheorem defines while=0 SCMFSA_9:def 1 :
:: deftheorem defines while>0 SCMFSA_9:def 2 :
theorem Th3:
:: deftheorem defines while<0 SCMFSA_9:def 3 :
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
for
s being
State of
for
k being
Element of
NAT st
I is_closed_on s &
I is_halting_on s &
k < LifeSpan (s +* (I +* (Start-At (insloc 0 )))) &
IC (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(1 + k)) = (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k)) + 4 &
DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(1 + k)) = DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),k) holds
(
IC (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((1 + k) + 1)) = (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(k + 1))) + 4 &
DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((1 + k) + 1)) = DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(k + 1)) )
theorem Th20:
theorem Th21:
theorem Th22:
set sl0 = Start-At (insloc 0 );
definition
let s be
State of ;
let I be
Program of ;
let a be
read-write Int-Location ;
deffunc H1(
Nat,
Element of
product the
Object-Kind of
SCM+FSA )
-> Element of
product the
Object-Kind of
SCM+FSA =
Computation ($2 +* ((while=0 a,I) +* (Start-At (insloc 0 )))),
((LifeSpan ($2 +* (I +* (Start-At (insloc 0 ))))) + 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) = Computation ((it . i) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),
((LifeSpan ((it . i) +* (I +* (Start-At (insloc 0 ))))) + 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) = Computation ((b1 . i) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan ((b1 . i) +* (I +* (Start-At (insloc 0 ))))) + 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) = Computation ((b1 . i) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan ((b1 . i) +* (I +* (Start-At (insloc 0 ))))) + 3) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Computation ((b2 . i) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan ((b2 . i) +* (I +* (Start-At (insloc 0 ))))) + 3) ) holds
b1 = b2
end;
:: deftheorem Def4 defines StepWhile=0 SCMFSA_9:def 4 :
theorem
canceled;
theorem
canceled;
theorem Th25:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th29:
theorem Th30:
theorem Th31:
for
I being
Program of
for
a being
read-write Int-Location for
s being
State of
for
k,
n being
Element of
NAT st
IC ((StepWhile=0 a,I,s) . k) = insloc 0 &
(StepWhile=0 a,I,s) . k = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),
n holds
(
(StepWhile=0 a,I,s) . k = ((StepWhile=0 a,I,s) . k) +* ((while=0 a,I) +* (Start-At (insloc 0 ))) &
(StepWhile=0 a,I,s) . (k + 1) = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),
(n + ((LifeSpan (((StepWhile=0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3)) )
theorem Th32:
for
I being
Program of
for
a being
read-write Int-Location for
s being
State of 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
for
a being
read-write Int-Location for
s being
State of 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
for
s being
State of
for
k being
Element of
NAT st
I is_closed_on s &
I is_halting_on s &
k < LifeSpan (s +* (I +* (Start-At (insloc 0 )))) &
IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + k)) = (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k)) + 4 &
DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + k)) = DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),k) holds
(
IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + k) + 1)) = (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(k + 1))) + 4 &
DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + k) + 1)) = DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(k + 1)) )
theorem Th45:
theorem Th46:
theorem Th47:
set sl0 = Start-At (insloc 0 );
definition
let s be
State of ;
let I be
Program of ;
let a be
read-write Int-Location ;
deffunc H1(
Nat,
Element of
product the
Object-Kind of
SCM+FSA )
-> Element of
product the
Object-Kind of
SCM+FSA =
Computation ($2 +* ((while>0 a,I) +* (Start-At (insloc 0 )))),
((LifeSpan ($2 +* (I +* (Start-At (insloc 0 ))))) + 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) = Computation ((it . i) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),
((LifeSpan ((it . i) +* (I +* (Start-At (insloc 0 ))))) + 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) = Computation ((b1 . i) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan ((b1 . i) +* (I +* (Start-At (insloc 0 ))))) + 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) = Computation ((b1 . i) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan ((b1 . i) +* (I +* (Start-At (insloc 0 ))))) + 3) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Computation ((b2 . i) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan ((b2 . i) +* (I +* (Start-At (insloc 0 ))))) + 3) ) holds
b1 = b2
end;
:: deftheorem Def5 defines StepWhile>0 SCMFSA_9:def 5 :
theorem
canceled;
theorem
canceled;
theorem Th50:
theorem Th51:
theorem Th52:
for
I being
Program of
for
a being
read-write Int-Location for
s being
State of
for
k,
n being
Element of
NAT st
IC ((StepWhile>0 a,I,s) . k) = insloc 0 &
(StepWhile>0 a,I,s) . k = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),
n holds
(
(StepWhile>0 a,I,s) . k = ((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) &
(StepWhile>0 a,I,s) . (k + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),
(n + ((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3)) )
theorem Th53:
for
I being
Program of
for
a being
read-write Int-Location for
s being
State of 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
for
a being
read-write Int-Location for
s being
State of 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