begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem Th13:
theorem
canceled;
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
Lm1:
Load ((DataLoc 0 ,0 ) := 0 ) is parahalting
begin
:: deftheorem Def1 defines No-StopCode SCMPDS_5:def 1 :
:: deftheorem Def2 defines parahalting SCMPDS_5:def 2 :
theorem
registration
let a,
b be
Int_position ;
let k1,
k2 be
Integer;
cluster AddTo a,
k1,
b,
k2 -> No-StopCode ;
coherence
AddTo a,k1,b,k2 is No-StopCode
cluster SubFrom a,
k1,
b,
k2 -> No-StopCode ;
coherence
SubFrom a,k1,b,k2 is No-StopCode
cluster MultBy a,
k1,
b,
k2 -> No-StopCode ;
coherence
MultBy a,k1,b,k2 is No-StopCode
cluster Divide a,
k1,
b,
k2 -> No-StopCode ;
coherence
Divide a,k1,b,k2 is No-StopCode
cluster a,
k1 := b,
k2 -> No-StopCode ;
coherence
a,k1 := b,k2 is No-StopCode
end;
Lm2:
for i being Instruction of st ( for s being State of holds (Exec i,s) . (IC SCMPDS ) = Next (IC s) ) holds
Load i is parahalting
registration
let a,
b be
Int_position ;
let k1,
k2 be
Integer;
cluster AddTo a,
k1,
b,
k2 -> parahalting ;
coherence
AddTo a,k1,b,k2 is parahalting
cluster SubFrom a,
k1,
b,
k2 -> parahalting ;
coherence
SubFrom a,k1,b,k2 is parahalting
cluster MultBy a,
k1,
b,
k2 -> parahalting ;
coherence
MultBy a,k1,b,k2 is parahalting
cluster Divide a,
k1,
b,
k2 -> parahalting ;
coherence
Divide a,k1,b,k2 is parahalting
cluster a,
k1 := b,
k2 -> parahalting ;
coherence
a,k1 := b,k2 is parahalting
end;
theorem Th26:
:: deftheorem Def3 defines No-StopCode SCMPDS_5:def 3 :
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
begin
theorem
Lm3:
for I being parahalting No-StopCode Program of
for J being parahalting shiftable Program of
for s, s1 being State of st Initialized (stop (I ';' J)) c= s & s1 = s +* (Initialized (stop I)) holds
( IC (Computation s,(LifeSpan s1)) = inspos (card I) & DataPart (Computation s,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Computation s,(LifeSpan s1) & LifeSpan s = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )
theorem Th37:
theorem Th38:
theorem
begin
:: deftheorem defines Initialized SCMPDS_5:def 4 :
theorem Th40:
theorem Th41:
theorem
canceled;
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem