begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th5:
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
theorem Th26:
theorem Th27:
theorem Th28:
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:
Lm4:
for I being parahalting keeping_0 Program of
for J being parahalting Program of
for s being State of st Initialized (I ';' J) c= s holds
( IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) & DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) & (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & ProgramPart s halts_on s & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )
theorem Th41:
theorem Th42:
theorem Th43:
theorem