begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th5:
Lm1:
not IC SCM+FSA in NAT
by AMI_1:48;
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
canceled;
theorem Th12:
theorem Th13:
theorem Th14:
begin
begin
:: deftheorem defines IExec SCMFSA6B:def 1 :
:: deftheorem Def2 defines paraclosed SCMFSA6B:def 2 :
:: deftheorem Def3 defines parahalting SCMFSA6B:def 3 :
:: deftheorem Def4 defines keeping_0 SCMFSA6B:def 4 :
Lm2:
Macro (halt SCM+FSA ) is parahalting
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem
theorem Th24:
theorem
canceled;
theorem
canceled;
theorem Th27:
for
s1,
s2 being
State of
SCM+FSA for
J being
parahalting Program of
SCM+FSA st
J +* (Start-At 0 ,SCM+FSA ) c= s1 holds
for
n being
Element of
NAT st
ProgramPart (Relocated J,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 Th28:
for
s1,
s2 being
State of
SCM+FSA for
I being
parahalting Program of
SCM+FSA st
I +* (Start-At 0 ,SCM+FSA ) c= s1 &
I +* (Start-At 0 ,SCM+FSA ) c= s2 &
s1,
s2 equal_outside NAT holds
for
k being
Element of
NAT holds
(
Comput (ProgramPart s1),
s1,
k,
Comput (ProgramPart s2),
s2,
k equal_outside NAT &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),
(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),
(Comput (ProgramPart s2),s2,k) )
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem
Lm3:
( Macro (halt SCM+FSA ) is keeping_0 & Macro (halt SCM+FSA ) is parahalting )
theorem
begin
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
for
s being
State of
SCM+FSA for
I being
paraclosed Program of
SCM+FSA st
ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on s +* (I +* (Start-At 0 ,SCM+FSA )) holds
for
J being
Program of
SCM+FSA for
k being
Element of
NAT st
k <= 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 ))),
k,
Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),
(s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),
k equal_outside NAT
Lm4:
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA
for s being State of SCM+FSA st Initialized (I ';' J) c= s holds
( IC (Comput (ProgramPart s),s,((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1)) = card I & DataPart (Comput (ProgramPart s),s,((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1)) = DataPart ((Comput (ProgramPart (s +* I)),(s +* I),(LifeSpan (ProgramPart (s +* I)),(s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Comput (ProgramPart s),s,((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1) & (Comput (ProgramPart s),s,((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1)) . (intloc 0 ) = 1 & ProgramPart s halts_on s & LifeSpan (ProgramPart s),s = ((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1) + (LifeSpan (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result (ProgramPart s),s) . (intloc 0 ) = 1 ) )
theorem Th41:
for
s being
State of
SCM+FSA for
I being
keeping_0 Program of
SCM+FSA st not
ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on s +* (I +* (Start-At 0 ,SCM+FSA )) holds
for
J being
Program of
SCM+FSA for
k being
Element of
NAT holds
Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),
(s +* (I +* (Start-At 0 ,SCM+FSA ))),
k,
Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),
(s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),
k equal_outside NAT
theorem Th42:
for
s being
State of
SCM+FSA for
I being
keeping_0 Program of
SCM+FSA st
ProgramPart (s +* I) halts_on s +* I holds
for
J being
paraclosed Program of
SCM+FSA st
(I ';' J) +* (Start-At 0 ,SCM+FSA ) c= s holds
for
k being
Element of
NAT holds
(Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (J +* (Start-At 0 ,SCM+FSA )))),((Result (ProgramPart (s +* I)),(s +* I)) +* (J +* (Start-At 0 ,SCM+FSA ))),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (J +* (Start-At 0 ,SCM+FSA )))),((Result (ProgramPart (s +* I)),(s +* I)) +* (J +* (Start-At 0 ,SCM+FSA ))),k)) + (card I)),SCM+FSA ),
Comput (ProgramPart (s +* (I ';' J))),
(s +* (I ';' J)),
(((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1) + k) equal_outside NAT
theorem Th43:
theorem