begin
begin
begin
begin
Lm1:
Load (halt SCMPDS) is parahalting
begin
Lm2:
Load (halt SCMPDS) is shiftable
registration
let a,
b be
Int_position;
let k1,
k2 be
Integer;
coherence
AddTo (a,k1,b,k2) is shiftable
coherence
SubFrom (a,k1,b,k2) is shiftable
coherence
MultBy (a,k1,b,k2) is shiftable
coherence
Divide (a,k1,b,k2) is shiftable
coherence
(a,k1) := (b,k2) is shiftable
end;
theorem
for
s2 being
State of
SCMPDS for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
s1 being
0 -started State of
SCMPDS for
J being
parahalting shiftable Program of
SCMPDS st
stop J c= P1 holds
for
n being
Element of
NAT st
Shift (
(stop J),
n)
c= P2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
(IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) &
CurInstr (
P1,
(Comput (P1,s1,i)))
= CurInstr (
P2,
(Comput (P2,s2,i))) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )