begin
set A = NAT ;
set D = SCM-Data-Loc ;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
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 :
Lm1:
for k1 being Integer holds
( inspos 0 in dom ((inspos 0 ) .--> (goto k1)) & ((inspos 0 ) .--> (goto k1)) . (inspos 0 ) = goto k1 )
theorem
canceled;
theorem Th33:
begin
:: deftheorem Def2 defines is_closed_on SCMPDS_6:def 2 :
:: deftheorem Def3 defines is_halting_on SCMPDS_6:def 3 :
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
Lm2:
for I being No-StopCode Program of
for J being Program of
for s being State of st I is_closed_on s & I is_halting_on s holds
( IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = inspos (((card I) + (card J)) + 1) & DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) & ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS ) & IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) & ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 )
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
begin
definition
let a be
Int_position ;
let k be
Integer;
let I,
J be
Program of ;
func if=0 a,
k,
I,
J -> Program of
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
;
func if>0 a,
k,
I,
J -> Program of
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
;
func if<0 a,
k,
I,
J -> Program of
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
;
end;
:: deftheorem defines if=0 SCMPDS_6:def 4 :
:: deftheorem defines if>0 SCMPDS_6:def 5 :
:: deftheorem defines if<0 SCMPDS_6:def 6 :
definition
let a be
Int_position ;
let k be
Integer;
let I be
Program of ;
func if=0 a,
k,
I -> Program of
equals
(a,k <>0_goto ((card I) + 1)) ';' I;
coherence
(a,k <>0_goto ((card I) + 1)) ';' I is Program of
;
func if<>0 a,
k,
I -> Program of
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
;
func if>0 a,
k,
I -> Program of
equals
(a,k <=0_goto ((card I) + 1)) ';' I;
coherence
(a,k <=0_goto ((card I) + 1)) ';' I is Program of
;
func if<=0 a,
k,
I -> Program of
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
;
func if<0 a,
k,
I -> Program of
equals
(a,k >=0_goto ((card I) + 1)) ';' I;
coherence
(a,k >=0_goto ((card I) + 1)) ';' I is Program of
;
func if>=0 a,
k,
I -> Program of
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
;
end;
:: deftheorem defines if=0 SCMPDS_6:def 7 :
:: deftheorem defines if<>0 SCMPDS_6:def 8 :
:: deftheorem defines if>0 SCMPDS_6:def 9 :
:: deftheorem defines if<=0 SCMPDS_6:def 10 :
:: deftheorem defines if<0 SCMPDS_6:def 11 :
:: deftheorem defines if>=0 SCMPDS_6:def 12 :
Lm3:
for n being Element of NAT
for i being Instruction of
for I, J being Program of holds card (((i ';' I) ';' (Goto n)) ';' J) = ((card I) + (card J)) + 2
begin
theorem
theorem
Lm4:
for i being Instruction of
for I, J, K being Program of holds (((i ';' I) ';' J) ';' K) . (inspos 0 ) = i
theorem
Lm5:
for n being Element of NAT
for i being Instruction of
for s being State of
for I being Program of holds Shift (stop I),1 c= Computation (s +* (Initialized (stop (i ';' I)))),n
Lm6:
for n being Element of NAT
for i, j being Instruction of
for s being State of
for I being Program of holds Shift (stop I),2 c= Computation (s +* (Initialized (stop ((i ';' j) ';' I)))),n
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
registration
let I,
J be
parahalting shiftable Program of ;
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:
Lm7:
for s being State of
for loc being Instruction-Location of SCMPDS holds (s +* (Start-At loc)) . (IC SCMPDS ) = loc
theorem Th65:
theorem
theorem
theorem
Lm8:
for i, j being Instruction of
for I being Program of holds card ((i ';' j) ';' I) = (card I) + 2
begin
theorem
Lm9:
for i, j being Instruction of
for I being Program of holds
( inspos 0 in dom ((i ';' j) ';' I) & inspos 1 in dom ((i ';' j) ';' I) )
theorem
Lm10:
for i, j being Instruction of
for I being Program of holds
( ((i ';' j) ';' I) . (inspos 0 ) = i & ((i ';' j) ';' I) . (inspos 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 ;
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 ;
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