begin
:: deftheorem SCMPDS_4:def 1 :
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem Th6:
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem
canceled;
theorem Th11:
theorem
canceled;
theorem Th13:
theorem Th14:
theorem Th15:
theorem
canceled;
theorem Th17:
theorem Th18:
theorem
theorem
theorem
theorem
theorem Th23:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th31:
theorem Th32:
theorem
theorem
begin
:: deftheorem SCMPDS_4:def 2 :
canceled;
:: deftheorem defines ';' SCMPDS_4:def 3 :
for I, J being Program of SCMPDS holds I ';' J = I +* (Shift J,(card I));
theorem
canceled;
theorem
canceled;
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem
theorem
begin
:: deftheorem defines ';' SCMPDS_4:def 4 :
for i being Instruction of SCMPDS
for J being Program of SCMPDS holds i ';' J = (Load i) ';' J;
:: deftheorem defines ';' SCMPDS_4:def 5 :
for I being Program of SCMPDS
for j being Instruction of SCMPDS holds I ';' j = I ';' (Load j);
:: deftheorem defines ';' SCMPDS_4:def 6 :
for i, j being Instruction of SCMPDS holds i ';' j = (Load i) ';' (Load j);
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 :
for I being Program of SCMPDS holds stop I = I ';' (Stop SCMPDS );
:: deftheorem defines IExec SCMPDS_4:def 8 :
for I being Program of SCMPDS
for s being State of SCMPDS holds IExec I,s = (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (s | NAT );
:: deftheorem Def9 defines paraclosed SCMPDS_4:def 9 :
for I being Program of SCMPDS holds
( I is paraclosed iff for s being State of SCMPDS
for n being Element of NAT st Initialize (stop I) c= s holds
IC (Comput (ProgramPart s),s,n) in dom (stop I) );
:: deftheorem Def10 defines parahalting SCMPDS_4:def 10 :
for I being Program of SCMPDS holds
( I is parahalting iff Initialize (stop I) is halting );
Lm1:
Load (halt SCMPDS ) is parahalting
theorem Th63:
theorem
canceled;
theorem
canceled;
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th75:
begin
:: deftheorem Def11 defines valid_at SCMPDS_4:def 11 :
for i being Instruction of SCMPDS
for n being Element of NAT holds
( i valid_at n iff ( ( InsCode i = 0 implies ex k1 being Integer st
( i = goto k1 & n + k1 >= 0 ) ) & ( InsCode i = 4 implies ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 <>0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 5 implies ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 <=0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 6 implies ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 >=0_goto k2 & n + k2 >= 0 ) ) ) );
theorem
canceled;
theorem Th77:
:: deftheorem Def12 defines shiftable SCMPDS_4:def 12 :
for IT being FinPartState of SCMPDS holds
( IT is shiftable iff for n being Element of NAT
for i being Instruction of SCMPDS st n in dom IT & i = IT . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) );
Lm2:
Load (halt SCMPDS ) is shiftable
:: deftheorem Def13 defines shiftable SCMPDS_4:def 13 :
for i being Instruction of SCMPDS holds
( i is shiftable iff ( InsCode i = 2 or InsCode i > 6 ) );
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
Initialize (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) )