begin
:: deftheorem defines Load SCMPDS_4:def 1 :
theorem
canceled;
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
canceled;
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
canceled;
theorem
canceled;
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
for
s1,
s2 being
State of
SCMPDS for
J being
parahalting shiftable Program of
SCMPDS st
Initialized (stop J) c= s1 holds
for
n being
Element of
NAT st
Shift (stop 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) &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) &
DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )