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
theorem
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
Lm1:
now
let s be
State of ;
for I being Program of holds
( ( Initialized I is_pseudo-closed_on s implies ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) & ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) )let I be
Program of ;
( ( Initialized I is_pseudo-closed_on s implies ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) & ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) )set k =
pseudo-LifeSpan (Initialize s),
I;
A1:
ProgramPart (Initialized I) = I
by SCMFSA6A:33;
hereby ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) )
set k =
pseudo-LifeSpan s,
(Initialized I);
assume A2:
Initialized I is_pseudo-closed_on s
;
( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I )then
IC (Computation (s +* ((Initialized I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,(Initialized I))) = insloc (card (ProgramPart (Initialized I)))
by SCMFSA8A:def 5;
then
IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,(Initialized I))) = insloc (card (ProgramPart (Initialized I)))
by Th16;
then A3:
IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,(Initialized I))) = insloc (card (ProgramPart I))
by A1, AMI_1:105;
hence A5:
I is_pseudo-closed_on Initialize s
by A3, SCMFSA8A:def 3;
pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I
for
n being
Element of
NAT st not
IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),n) in dom I holds
pseudo-LifeSpan s,
(Initialized I) <= n
by A4;
hence
pseudo-LifeSpan s,
(Initialized I) = pseudo-LifeSpan (Initialize s),
I
by A3, A5, SCMFSA8A:def 5;
verum
end;
assume A6:
I is_pseudo-closed_on Initialize s
;
( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I )then
IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize s),I)) = insloc (card (ProgramPart I))
by SCMFSA8A:def 5;
then
IC (Computation (s +* ((Initialized I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize s),I)) = insloc (card (ProgramPart I))
by Th16;
then A7:
IC (Computation (s +* ((Initialized I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize s),I)) = insloc (card (ProgramPart (Initialized I)))
by A1, AMI_1:105;
hence A9:
Initialized I is_pseudo-closed_on s
by A7, SCMFSA8A:def 3;
pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I
for
n being
Element of
NAT st not
IC (Computation (s +* ((Initialized I) +* (Start-At (insloc 0 )))),n) in dom (Initialized I) holds
pseudo-LifeSpan (Initialize s),
I <= n
by A8;
hence
pseudo-LifeSpan s,
(Initialized I) = pseudo-LifeSpan (Initialize s),
I
by A7, A9, SCMFSA8A:def 5;
verum
end;
theorem
theorem
theorem
theorem Th50:
theorem Th51:
for
s1,
s2 being
State of
for
I being
Program of st
I +* (Start-At (insloc 0 )) c= s1 &
I is_pseudo-closed_on s1 holds
for
n being
Element of
NAT st
ProgramPart (Relocated I,n) c= s2 &
IC s2 = insloc n &
DataPart s1 = DataPart s2 holds
( ( for
i being
Element of
NAT st
i < pseudo-LifeSpan s1,
I holds
IncAddr (CurInstr (Computation s1,i)),
n = CurInstr (Computation s2,i) ) & ( for
i being
Element of
NAT st
i <= pseudo-LifeSpan s1,
I holds
(
(IC (Computation s1,i)) + n = IC (Computation s2,i) &
DataPart (Computation s1,i) = DataPart (Computation s2,i) ) ) )
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem
theorem Th68:
theorem Th69:
theorem Th70:
theorem
theorem Th72:
theorem Th73:
theorem
theorem
theorem
theorem Th77:
theorem Th78:
theorem
theorem
theorem Th81:
theorem Th82:
theorem
theorem
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem Th93:
theorem Th94:
theorem Th95:
theorem Th96:
theorem
theorem Th98:
theorem Th99:
theorem Th100:
theorem Th101:
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 :
theorem
canceled;
theorem
theorem
canceled;
theorem Th107:
theorem
canceled;
theorem Th109:
theorem Th110:
Lm2:
for s being State of
for I being Program of st I is_closed_on s & I is_halting_on s holds
( CurInstr (Computation (s +* ((loop I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = goto (insloc 0 ) & ( for m being Element of NAT st m <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
CurInstr (Computation (s +* ((loop I) +* (Start-At (insloc 0 )))),m) <> halt SCM+FSA ) )
theorem
theorem
theorem Th113:
theorem
begin
definition
let a be
Int-Location ;
let I be
Program of ;
func Times a,
I -> Program of
equals
if>0 a,
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))),
(Stop SCM+FSA );
correctness
coherence
if>0 a,(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))),(Stop SCM+FSA ) is Program of ;
;
end;
:: deftheorem defines Times SCMFSA8C:def 5 :
theorem Th115:
theorem Th116:
theorem Th117:
theorem
theorem
theorem
theorem
theorem Th122:
for
s being
State of
for
I being
parahalting good Program of
for
a being
read-write Int-Location st
I does_not_destroy a &
s . (intloc 0 ) = 1 &
s . a > 0 holds
ex
s2 being
State of ex
k being
Element of
NAT st
(
s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) &
k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 &
(Computation s2,k) . a = (s . a) - 1 &
(Computation s2,k) . (intloc 0 ) = 1 & ( for
b being
read-write Int-Location st
b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for
f being
FinSeq-Location holds
(Computation s2,k) . f = (IExec I,s) . f ) &
IC (Computation s2,k) = insloc 0 & ( for
n being
Element of
NAT st
n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
theorem Th123:
theorem Th124:
begin
theorem