begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem
canceled;
theorem Th13:
theorem Th14:
theorem Th15:
theorem
canceled;
theorem Th17:
theorem Th18:
theorem
theorem
theorem
canceled;
theorem
theorem Th23:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
begin
:: deftheorem SCMPDS_4:def 1 :
canceled;
:: 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)));
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th59:
theorem
canceled;
theorem
begin
:: deftheorem SCMPDS_4:def 7 :
canceled;
:: 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 0 -started State of SCMPDS
for n being Element of NAT st 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 for s being 0 -started State of SCMPDS st stop I c= s holds
ProgramPart s halts_on s );
Lm1:
Load (halt SCMPDS) is parahalting
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th66:
theorem Th67:
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 ) ) ) );
:: 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
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th77:
:: 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
s2 being
State of
SCMPDS for
s1 being
0 -started State of
SCMPDS for
J being
parahalting shiftable Program of
SCMPDS st
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 s1),
(Comput ((ProgramPart s1),s1,i)))
= CurInstr (
(ProgramPart s2),
(Comput ((ProgramPart s2),s2,i))) &
DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )