begin
theorem
canceled;
Lm1:
card (Stop SCMPDS) = 1
by COMPOS_1:46;
theorem Th2:
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
canceled;
theorem
canceled;
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
for
s1,
s2 being
0 -started State of
SCMPDS for
I being
parahalting Program of
SCMPDS st
stop I c= s1 &
stop I c= s2 &
s1,
s2 equal_outside NAT holds
for
k being
Element of
NAT holds
(
Comput (
(ProgramPart s1),
s1,
k),
Comput (
(ProgramPart s2),
s2,
k)
equal_outside NAT &
CurInstr (
(ProgramPart s1),
(Comput ((ProgramPart s1),s1,k)))
= CurInstr (
(ProgramPart s2),
(Comput ((ProgramPart s2),s2,k))) )
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
set SA0 = Start-At (0,SCMPDS);
Lm2:
Load ((DataLoc (0,0)) := 0) is parahalting
begin
:: deftheorem Def1 defines No-StopCode SCMPDS_5:def 1 :
for i being Instruction of SCMPDS holds
( i is No-StopCode iff i <> halt SCMPDS );
:: 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:
:: deftheorem Def3 defines halt-free SCMPDS_5:def 3 :
for N being with_non-empty_elements set
for S being non empty stored-program definite AMI-Struct of N
for IT being NAT -defined the Instructions of b2 -valued Function holds
( IT is halt-free iff for x being Element of NAT st x in dom IT holds
IT . x <> halt S );
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
begin
theorem
for
s being
0 -started State of
SCMPDS for
I being
halt-free parahalting Program of
SCMPDS for
J being
parahalting shiftable Program of
SCMPDS for
k being
Element of
NAT st
stop (I ';' J) c= s holds
(Comput ((ProgramPart ((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J)),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J)),k))) + (card I)),SCMPDS)),
Comput (
(ProgramPart (s +* (stop (I ';' J)))),
(s +* (stop (I ';' J))),
((LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)))) + k))
equal_outside NAT
Lm4:
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
for s1 being State of SCMPDS st stop (I ';' J) c= s & s1 = s +* (stop I) holds
( IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = card I & DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) & Shift ((stop J),(card I)) c= Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1))) & LifeSpan ((ProgramPart s),s) = (LifeSpan ((ProgramPart s1),s1)) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))),((Initialize (Result ((ProgramPart s1),s1))) +* (stop J)))) )
theorem Th37:
theorem Th38:
theorem
begin
theorem Th40:
theorem Th41:
theorem
canceled;
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem