begin
Lm1:
card (Stop SCMPDS) = 1
by AFINSQ_1:33;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th12:
theorem Th16:
theorem Th17:
set SA0 = Start-At (0,SCMPDS);
theorem Th19:
theorem Th20:
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))) )
theorem Th21:
theorem
canceled;
theorem Th23:
theorem Th24:
Lm2:
Load ((DataLoc (0,0)) := 0) is parahalting
begin
:: deftheorem SCMPDS_5:def 1 :
canceled;
:: deftheorem Def2 defines parahalting SCMPDS_5:def 2 :
for i being Instruction of SCMPDS holds
( i is parahalting iff Load i is parahalting );
theorem
registration
let a,
b be
Int_position ;
let k1,
k2 be
Integer;
cluster AddTo (
a,
k1,
b,
k2)
-> No-StopCode ;
coherence
AddTo (a,k1,b,k2) is No-StopCode
cluster SubFrom (
a,
k1,
b,
k2)
-> No-StopCode ;
coherence
SubFrom (a,k1,b,k2) is No-StopCode
cluster MultBy (
a,
k1,
b,
k2)
-> No-StopCode ;
coherence
MultBy (a,k1,b,k2) is No-StopCode
cluster Divide (
a,
k1,
b,
k2)
-> No-StopCode ;
coherence
Divide (a,k1,b,k2) is No-StopCode
cluster (
a,
k1)
:= (
b,
k2)
-> 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;
cluster AddTo (
a,
k1,
b,
k2)
-> parahalting ;
coherence
AddTo (a,k1,b,k2) is parahalting
cluster SubFrom (
a,
k1,
b,
k2)
-> parahalting ;
coherence
SubFrom (a,k1,b,k2) is parahalting
cluster MultBy (
a,
k1,
b,
k2)
-> parahalting ;
coherence
MultBy (a,k1,b,k2) is parahalting
cluster Divide (
a,
k1,
b,
k2)
-> parahalting ;
coherence
Divide (a,k1,b,k2) is parahalting
cluster (
a,
k1)
:= (
b,
k2)
-> parahalting ;
coherence
(a,k1) := (b,k2) is parahalting
end;
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
begin
theorem
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))))) )
theorem Th37:
theorem Th38:
theorem
begin
theorem
canceled;
theorem
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem