begin
set A = NAT ;
set D = SCM-Data-Loc ;
JJ:
(Stop SCMPDS ) . 0 = halt SCMPDS
by AFINSQ_1:38;
KK:
0 in dom (Stop SCMPDS )
by COMPOS_1:45;
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem
canceled;
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem
canceled;
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem Th29:
theorem Th30:
theorem Th31:
:: deftheorem defines Goto SCMPDS_6:def 1 :
for k1 being Integer holds Goto k1 = Load (goto k1);
theorem
canceled;
theorem Th33:
begin
:: deftheorem Def2 defines is_closed_on SCMPDS_6:def 2 :
for I being Program of SCMPDS
for s being State of SCMPDS holds
( I is_closed_on s iff for k being Element of NAT holds IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) in dom (stop I) );
:: deftheorem Def3 defines is_halting_on SCMPDS_6:def 3 :
for I being Program of SCMPDS
for s being State of SCMPDS holds
( I is_halting_on s iff ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) );
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
for
I,
J being
Program of
SCMPDS for
s being
State of
SCMPDS st
I is_closed_on s &
I is_halting_on s holds
( ( for
k being
Element of
NAT st
k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),
((Initialize s) +* (stop I)) holds
IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k) ) &
DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) )
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
Lm2:
for I being halt-free Program of SCMPDS
for J being Program of SCMPDS
for s being State of SCMPDS st I is_closed_on s & I is_halting_on s holds
( IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) = ((card I) + (card J)) + 1 & DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) & ( for k being Element of NAT st k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
CurInstr (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),k) <> halt SCMPDS ) & IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = card I & ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) halts_on (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) & LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1 )
theorem Th44:
theorem Th45:
for
s1,
s2 being
State of
SCMPDS for
I being
shiftable Program of
SCMPDS st
Initialize (stop I) c= s1 &
I is_closed_on s1 holds
for
n being
Element of
NAT st
Shift (stop I),
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 (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) &
DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
theorem Th46:
theorem Th47:
theorem Th48:
begin
definition
let a be
Int_position ;
let k be
Integer;
let I,
J be
Program of
SCMPDS ;
func if=0 a,
k,
I,
J -> Program of
SCMPDS equals
(((a,k <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;
coherence
(((a,k <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS
;
func if>0 a,
k,
I,
J -> Program of
SCMPDS equals
(((a,k <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;
coherence
(((a,k <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS
;
func if<0 a,
k,
I,
J -> Program of
SCMPDS equals
(((a,k >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;
coherence
(((a,k >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS
;
end;
:: deftheorem defines if=0 SCMPDS_6:def 4 :
for a being Int_position
for k being Integer
for I, J being Program of SCMPDS holds if=0 a,k,I,J = (((a,k <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;
:: deftheorem defines if>0 SCMPDS_6:def 5 :
for a being Int_position
for k being Integer
for I, J being Program of SCMPDS holds if>0 a,k,I,J = (((a,k <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;
:: deftheorem defines if<0 SCMPDS_6:def 6 :
for a being Int_position
for k being Integer
for I, J being Program of SCMPDS holds if<0 a,k,I,J = (((a,k >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;
definition
let a be
Int_position ;
let k be
Integer;
let I be
Program of
SCMPDS ;
func if=0 a,
k,
I -> Program of
SCMPDS equals
(a,k <>0_goto ((card I) + 1)) ';' I;
coherence
(a,k <>0_goto ((card I) + 1)) ';' I is Program of SCMPDS
;
func if<>0 a,
k,
I -> Program of
SCMPDS equals
((a,k <>0_goto 2) ';' (goto ((card I) + 1))) ';' I;
coherence
((a,k <>0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS
;
func if>0 a,
k,
I -> Program of
SCMPDS equals
(a,k <=0_goto ((card I) + 1)) ';' I;
coherence
(a,k <=0_goto ((card I) + 1)) ';' I is Program of SCMPDS
;
func if<=0 a,
k,
I -> Program of
SCMPDS equals
((a,k <=0_goto 2) ';' (goto ((card I) + 1))) ';' I;
coherence
((a,k <=0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS
;
func if<0 a,
k,
I -> Program of
SCMPDS equals
(a,k >=0_goto ((card I) + 1)) ';' I;
coherence
(a,k >=0_goto ((card I) + 1)) ';' I is Program of SCMPDS
;
func if>=0 a,
k,
I -> Program of
SCMPDS equals
((a,k >=0_goto 2) ';' (goto ((card I) + 1))) ';' I;
coherence
((a,k >=0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS
;
end;
:: deftheorem defines if=0 SCMPDS_6:def 7 :
for a being Int_position
for k being Integer
for I being Program of SCMPDS holds if=0 a,k,I = (a,k <>0_goto ((card I) + 1)) ';' I;
:: deftheorem defines if<>0 SCMPDS_6:def 8 :
for a being Int_position
for k being Integer
for I being Program of SCMPDS holds if<>0 a,k,I = ((a,k <>0_goto 2) ';' (goto ((card I) + 1))) ';' I;
:: deftheorem defines if>0 SCMPDS_6:def 9 :
for a being Int_position
for k being Integer
for I being Program of SCMPDS holds if>0 a,k,I = (a,k <=0_goto ((card I) + 1)) ';' I;
:: deftheorem defines if<=0 SCMPDS_6:def 10 :
for a being Int_position
for k being Integer
for I being Program of SCMPDS holds if<=0 a,k,I = ((a,k <=0_goto 2) ';' (goto ((card I) + 1))) ';' I;
:: deftheorem defines if<0 SCMPDS_6:def 11 :
for a being Int_position
for k being Integer
for I being Program of SCMPDS holds if<0 a,k,I = (a,k >=0_goto ((card I) + 1)) ';' I;
:: deftheorem defines if>=0 SCMPDS_6:def 12 :
for a being Int_position
for k being Integer
for I being Program of SCMPDS holds if>=0 a,k,I = ((a,k >=0_goto 2) ';' (goto ((card I) + 1))) ';' I;
Lm3:
for n being Element of NAT
for i being Instruction of SCMPDS
for I, J being Program of SCMPDS holds card (((i ';' I) ';' (Goto n)) ';' J) = ((card I) + (card J)) + 2
begin
theorem
theorem
Lm4:
for i being Instruction of SCMPDS
for I, J, K being Program of SCMPDS holds (((i ';' I) ';' J) ';' K) . 0 = i
theorem
Lm5:
for n being Element of NAT
for i being Instruction of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),1 c= Comput (ProgramPart ((Initialize s) +* (stop (i ';' I)))),((Initialize s) +* (stop (i ';' I))),n
Lm6:
for n being Element of NAT
for i, j being Instruction of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),2 c= Comput (ProgramPart ((Initialize s) +* (stop ((i ';' j) ';' I)))),((Initialize s) +* (stop ((i ';' j) ';' I))),n
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
registration
let I,
J be
parahalting shiftable Program of
SCMPDS ;
let a be
Int_position ;
let k1 be
Integer;
cluster if=0 a,
k1,
I,
J -> parahalting shiftable ;
correctness
coherence
( if=0 a,k1,I,J is shiftable & if=0 a,k1,I,J is parahalting );
end;
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem
theorem
Lm8:
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds card ((i ';' j) ';' I) = (card I) + 2
begin
theorem
Lm9:
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds
( 0 in dom ((i ';' j) ';' I) & 1 in dom ((i ';' j) ';' I) )
theorem
Lm10:
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds
( ((i ';' j) ';' I) . 0 = i & ((i ';' j) ';' I) . 1 = j )
theorem
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
registration
let I,
J be
parahalting shiftable Program of
SCMPDS ;
let a be
Int_position ;
let k1 be
Integer;
cluster if>0 a,
k1,
I,
J -> parahalting shiftable ;
correctness
coherence
( if>0 a,k1,I,J is shiftable & if>0 a,k1,I,J is parahalting );
end;
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem Th92:
theorem Th93:
theorem Th94:
theorem Th95:
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem Th102:
theorem Th103:
theorem Th104:
theorem Th105:
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem Th112:
theorem Th113:
theorem Th114:
theorem Th115:
registration
let I,
J be
parahalting shiftable Program of
SCMPDS ;
let a be
Int_position ;
let k1 be
Integer;
cluster if<0 a,
k1,
I,
J -> parahalting shiftable ;
correctness
coherence
( if<0 a,k1,I,J is shiftable & if<0 a,k1,I,J is parahalting );
end;
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem Th122:
theorem Th123:
theorem Th124:
theorem Th125:
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem Th132:
theorem Th133:
theorem Th134:
theorem Th135:
theorem
theorem
theorem