begin
Lm1:
card (Stop SCMPDS) = 1
by AFINSQ_1:33;
set SA0 = Start-At (0,SCMPDS);
theorem Th16:
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS for
I being
parahalting Program of
SCMPDS st
stop I c= P1 &
stop I c= P2 holds
for
k being
Element of
NAT holds
(
Comput (
P1,
s,
k)
= Comput (
P2,
s,
k) &
CurInstr (
P1,
(Comput (P1,s,k)))
= CurInstr (
P2,
(Comput (P2,s,k))) )
Lm2:
Load ((DataLoc (0,0)) := 0) is parahalting
begin
registration
let a,
b be
Int_position;
let k1,
k2 be
Integer;
coherence
AddTo (a,k1,b,k2) is No-StopCode
coherence
SubFrom (a,k1,b,k2) is No-StopCode
coherence
MultBy (a,k1,b,k2) is No-StopCode
coherence
Divide (a,k1,b,k2) is No-StopCode
coherence
(a,k1) := (b,k2) is No-StopCode
end;
Lm3:
for i being Instruction of SCMPDS st ( for s being State of SCMPDS holds (Exec (i,s)) . (IC ) = succ (IC s) ) holds
Load i is parahalting
registration
let a,
b be
Int_position;
let k1,
k2 be
Integer;
coherence
AddTo (a,k1,b,k2) is parahalting
coherence
SubFrom (a,k1,b,k2) is parahalting
coherence
MultBy (a,k1,b,k2) is parahalting
coherence
Divide (a,k1,b,k2) is parahalting
coherence
(a,k1) := (b,k2) is parahalting
end;
begin
Lm4:
for P, P1 being Instruction-Sequence of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds
( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )
begin