begin
theorem
canceled;
theorem Th2:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem
canceled;
theorem
canceled;
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
canceled;
theorem
canceled;
theorem Th42:
for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1 &
I +* (Start-At 0 ,SCM+FSA ) c= s1 holds
for
n being
Element of
NAT st
ProgramPart (Relocated I,n) c= s2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
(IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) &
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) &
DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
theorem Th43:
for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1 &
I +* (Start-At 0 ,SCM+FSA ) c= s1 &
I +* (Start-At 0 ,SCM+FSA ) c= s2 &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
IC (Comput (ProgramPart s1),s1,i) = IC (Comput (ProgramPart s2),s2,i) &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) &
DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
theorem Th44:
theorem Th45:
theorem Th46:
Lm1:
now
let s be
State of
SCM+FSA ;
for I being Program of SCM+FSA holds
( ( Initialized I is_pseudo-closed_on s implies ( I is_pseudo-closed_on Initialized s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialized s),I ) ) & ( I is_pseudo-closed_on Initialized s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialized s),I ) ) )let I be
Program of
SCM+FSA ;
( ( Initialized I is_pseudo-closed_on s implies ( I is_pseudo-closed_on Initialized s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialized s),I ) ) & ( I is_pseudo-closed_on Initialized s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialized s),I ) ) )set k =
pseudo-LifeSpan (Initialized s),
I;
A1:
ProgramPart (Initialized I) = I
by SCMFSA6A:33;
hereby ( I is_pseudo-closed_on Initialized s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialized s),I ) )
set k =
pseudo-LifeSpan s,
(Initialized I);
X:
s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))
by Th16;
assume A2:
Initialized I is_pseudo-closed_on s
;
( I is_pseudo-closed_on Initialized s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialized s),I )then
IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Initialized I))) = card (ProgramPart (Initialized I))
by SCMFSA8A:def 5;
then
IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Initialized I))) = card (ProgramPart (Initialized I))
by X;
then A3:
IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Initialized I))) = card (ProgramPart I)
by A1, RELAT_1:209;
A4:
now
let n be
Element of
NAT ;
( n < pseudo-LifeSpan s,(Initialized I) implies IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I )X:
s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))
by Th16;
assume
n < pseudo-LifeSpan s,
(Initialized I)
;
IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom Ithen
IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I)
by A2, SCMFSA8A:def 5;
then
IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I)
by X;
hence
IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I
by Th20;
verum
end;
hence A5:
I is_pseudo-closed_on Initialized s
by A3, SCMFSA8A:def 3;
pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialized s),I
for
n being
Element of
NAT st not
IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I holds
pseudo-LifeSpan s,
(Initialized I) <= n
by A4;
hence
pseudo-LifeSpan s,
(Initialized I) = pseudo-LifeSpan (Initialized s),
I
by A3, A5, SCMFSA8A:def 5;
verum
end;
X:
s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))
by Th16;
assume A6:
I is_pseudo-closed_on Initialized s
;
( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialized s),I )then
IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialized s),I)) = card (ProgramPart I)
by SCMFSA8A:def 5;
then
IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialized s),I)) = card (ProgramPart I)
by X;
then A7:
IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialized s),I)) = card (ProgramPart (Initialized I))
by A1, RELAT_1:209;
A8:
now
let n be
Element of
NAT ;
( n < pseudo-LifeSpan (Initialized s),I implies IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I) )X:
s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))
by Th16;
assume
n < pseudo-LifeSpan (Initialized s),
I
;
IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I)then
IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I
by A6, SCMFSA8A:def 5;
then
IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom I
by X;
hence
IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I)
by Th20;
verum
end;
hence A9:
Initialized I is_pseudo-closed_on s
by A7, SCMFSA8A:def 3;
pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialized s),I
for
n being
Element of
NAT st not
IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I) holds
pseudo-LifeSpan (Initialized s),
I <= n
by A8;
hence
pseudo-LifeSpan s,
(Initialized I) = pseudo-LifeSpan (Initialized s),
I
by A7, A9, SCMFSA8A:def 5;
verum
end;
theorem
theorem
theorem
theorem Th50:
theorem Th51:
for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I +* (Start-At 0 ,SCM+FSA ) c= s1 &
I is_pseudo-closed_on s1 holds
for
n being
Element of
NAT st
ProgramPart (Relocated I,n) c= s2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
( ( for
i being
Element of
NAT st
i < pseudo-LifeSpan s1,
I holds
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) ) & ( for
i being
Element of
NAT st
i <= pseudo-LifeSpan s1,
I holds
(
(IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) &
DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) ) ) )
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
Directed I is_pseudo-closed_on s holds
(
I ';' (Stop SCM+FSA ) is_closed_on s &
I ';' (Stop SCM+FSA ) is_halting_on s &
LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),
(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = pseudo-LifeSpan s,
(Directed I) & ( for
n being
Element of
NAT st
n < pseudo-LifeSpan s,
(Directed I) holds
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) = IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),n) ) & ( for
n being
Element of
NAT st
n <= pseudo-LifeSpan s,
(Directed I) holds
DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) = DataPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),n) ) )
theorem Th59:
theorem
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a = 0 &
Directed I is_pseudo-closed_on s holds
(
if=0 a,
I,
J is_halting_on s &
if=0 a,
I,
J is_closed_on s &
LifeSpan (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),
(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 1 )
theorem
theorem Th68:
for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a > 0 &
Directed I is_pseudo-closed_on s holds
(
if>0 a,
I,
J is_halting_on s &
if>0 a,
I,
J is_closed_on s &
LifeSpan (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),
(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 1 )
theorem Th69:
theorem Th70:
for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a <> 0 &
Directed J is_pseudo-closed_on s holds
(
if=0 a,
I,
J is_halting_on s &
if=0 a,
I,
J is_closed_on s &
LifeSpan (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),
(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 3 )
theorem
theorem Th72:
for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a <= 0 &
Directed J is_pseudo-closed_on s holds
(
if>0 a,
I,
J is_halting_on s &
if>0 a,
I,
J is_closed_on s &
LifeSpan (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),
(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 3 )
theorem Th73:
theorem
theorem
theorem
theorem Th77:
theorem Th78:
theorem
theorem
theorem Th81:
theorem Th82:
theorem
theorem
theorem Th85:
theorem Th86:
theorem Th87:
for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_halting_on Initialized s holds
( ( for
a being
read-write Int-Location holds
(IExec I,s) . a = (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . a ) & ( for
f being
FinSeq-Location holds
(IExec I,s) . f = (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . f ) )
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem Th93:
for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA for
a being
Int-Location st not
I destroysdestroy a holds
for
k being
Element of
NAT st
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I holds
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) . a = (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) . a
theorem Th94:
theorem Th95:
theorem Th96:
theorem
theorem Th98:
for
s being
State of
SCM+FSA for
I being
parahalting keeping_0 Program of
SCM+FSA for
a being
read-write Int-Location st not
I destroysdestroy a holds
(Comput (ProgramPart ((Initialized s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA ))))) . a = (s . a) - 1
theorem Th99:
theorem Th100:
for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1 &
I is_halting_on s1 &
DataPart s1 = DataPart s2 holds
for
k being
Element of
NAT holds
(
Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),
(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),
k,
Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),
(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),
k equal_outside NAT &
CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k)),
(Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k) = CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k)),
(Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k) )
theorem Th101:
for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1 &
I is_halting_on s1 &
DataPart s1 = DataPart s2 holds
(
LifeSpan (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),
(s1 +* (I +* (Start-At 0 ,SCM+FSA ))) = LifeSpan (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),
(s2 +* (I +* (Start-At 0 ,SCM+FSA ))) &
Result (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),
(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),
Result (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),
(s2 +* (I +* (Start-At 0 ,SCM+FSA ))) equal_outside NAT )
theorem
canceled;
theorem Th103:
begin
:: deftheorem SCMFSA8C:def 1 :
canceled;
:: deftheorem SCMFSA8C:def 2 :
canceled;
:: deftheorem SCMFSA8C:def 3 :
canceled;
:: deftheorem defines loop SCMFSA8C:def 4 :
for I being Program of SCM+FSA holds loop I = Directed I,0 ;
theorem
canceled;
theorem
theorem
canceled;
theorem Th107:
theorem
canceled;
theorem Th109:
for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s &
I is_halting_on s holds
for
m being
Element of
NAT st
m <= LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),
(s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),
(s +* (I +* (Start-At 0 ,SCM+FSA ))),
m,
Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),
(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),
m equal_outside NAT
theorem Th110:
for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s &
I is_halting_on s holds
for
m being
Element of
NAT st
m < LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),
(s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),m)),
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),m) = CurInstr (ProgramPart (Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m)),
(Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m)
Lm2:
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( CurInstr (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m)),(Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m) <> halt SCM+FSA ) )
theorem
for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s &
I is_halting_on s holds
for
m being
Element of
NAT st
m <= LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),
(s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m)),
(Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m) <> halt SCM+FSA by Lm2;
theorem
theorem Th113:
theorem
begin
definition
let a be
Int-Location ;
let I be
Program of
SCM+FSA ;
func Times a,
I -> Program of
SCM+FSA equals
if>0 a,
(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))),
(Stop SCM+FSA );
correctness
coherence
if>0 a,(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))),(Stop SCM+FSA ) is Program of SCM+FSA ;
;
end;
:: deftheorem defines Times SCMFSA8C:def 5 :
for a being Int-Location
for I being Program of SCM+FSA holds Times a,I = if>0 a,(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))),(Stop SCM+FSA );
theorem Th115:
theorem Th116:
theorem Th117:
theorem
theorem
theorem
theorem
theorem Th122:
for
s being
State of
SCM+FSA for
I being
parahalting good Program of
SCM+FSA for
a being
read-write Int-Location st not
I destroysdestroy a &
s . (intloc 0 ) = 1 &
s . a > 0 holds
ex
s2 being
State of
SCM+FSA ex
k being
Element of
NAT st
(
s2 = s +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) &
k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 &
(Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 &
(Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for
b being
read-write Int-Location st
b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for
f being
FinSeq-Location holds
(Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) &
IC (Comput (ProgramPart s2),s2,k) = 0 & ( for
n being
Element of
NAT st
n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
theorem Th123:
theorem Th124:
begin
theorem