begin
:: deftheorem defines Load SCMPDS_4:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
:: deftheorem defines Initialized SCMPDS_4:def 2 :
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem
canceled;
theorem Th11:
theorem
canceled;
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem
theorem
theorem
theorem
theorem Th23:
theorem
theorem
canceled;
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem
theorem
begin
:: deftheorem defines ';' SCMPDS_4:def 3 :
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem
theorem
begin
:: deftheorem defines ';' SCMPDS_4:def 4 :
:: deftheorem defines ';' SCMPDS_4:def 5 :
:: deftheorem defines ';' SCMPDS_4:def 6 :
theorem
theorem
theorem Th45:
theorem Th46:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th54:
theorem
canceled;
theorem Th56:
theorem
theorem Th58:
theorem Th59:
theorem
canceled;
theorem
theorem
begin
:: deftheorem defines stop SCMPDS_4:def 7 :
:: deftheorem defines IExec SCMPDS_4:def 8 :
:: deftheorem Def9 defines paraclosed SCMPDS_4:def 9 :
:: deftheorem Def10 defines parahalting SCMPDS_4:def 10 :
Lm1:
Load (halt SCMPDS ) is parahalting
theorem Th63:
theorem
canceled;
theorem
canceled;
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem
canceled;
theorem Th71:
theorem
canceled;
theorem
theorem Th74:
theorem Th75:
begin
:: deftheorem Def11 defines valid_at SCMPDS_4:def 11 :
theorem
canceled;
theorem Th77:
:: deftheorem Def12 defines shiftable SCMPDS_4:def 12 :
Lm2:
Load (halt SCMPDS ) is shiftable
:: deftheorem Def13 defines shiftable SCMPDS_4:def 13 :
registration
let a,
b be
Int_position ;
let k1,
k2 be
Integer;
cluster AddTo a,
k1,
b,
k2 -> shiftable ;
coherence
AddTo a,k1,b,k2 is shiftable
cluster SubFrom a,
k1,
b,
k2 -> shiftable ;
coherence
SubFrom a,k1,b,k2 is shiftable
cluster MultBy a,
k1,
b,
k2 -> shiftable ;
coherence
MultBy a,k1,b,k2 is shiftable
cluster Divide a,
k1,
b,
k2 -> shiftable ;
coherence
Divide a,k1,b,k2 is shiftable
cluster a,
k1 := b,
k2 -> shiftable ;
coherence
a,k1 := b,k2 is shiftable
end;
theorem
theorem
theorem
theorem
theorem Th82:
theorem Th83:
theorem