let s be State of SCMPDS; for I, J being shiftable Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s & I is_halting_on s holds
( if>0 (a,k1,I,J) is_closed_on s & if>0 (a,k1,I,J) is_halting_on s )
let I, J be shiftable Program of SCMPDS; for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s & I is_halting_on s holds
( if>0 (a,k1,I,J) is_closed_on s & if>0 (a,k1,I,J) is_halting_on s )
let a be Int_position ; for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s & I is_halting_on s holds
( if>0 (a,k1,I,J) is_closed_on s & if>0 (a,k1,I,J) is_halting_on s )
let k1 be Integer; ( s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s & I is_halting_on s implies ( if>0 (a,k1,I,J) is_closed_on s & if>0 (a,k1,I,J) is_halting_on s ) )
set b = DataLoc ((s . a),k1);
set G = Goto ((card J) + 1);
set I2 = (I ';' (Goto ((card J) + 1))) ';' J;
set IF = if>0 (a,k1,I,J);
set pIF = stop (if>0 (a,k1,I,J));
set pI2 = stop ((I ';' (Goto ((card J) + 1))) ';' J);
set s2 = (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J));
set s3 = (Initialize s) +* (stop (if>0 (a,k1,I,J)));
set s4 = Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1);
I1:
s +* (Initialize (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))
by COMPOS_1:125;
I2:
s +* (Initialize (stop (if>0 (a,k1,I,J)))) = (Initialize s) +* (stop (if>0 (a,k1,I,J)))
by COMPOS_1:125;
set i = (a,k1) <=0_goto ((card I) + 2);
A1:
0 in dom (stop (if>0 (a,k1,I,J)))
by COMPOS_1:135;
A2:
IC ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) = 0
by I2, FUNCT_4:26, SCMPDS_5:18;
A3:
not DataLoc ((s . a),k1) in dom (Initialize (stop (if>0 (a,k1,I,J))))
by SCMPDS_4:31;
not a in dom (Initialize (stop (if>0 (a,k1,I,J))))
by SCMPDS_4:31;
then A4: ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) . (DataLoc ((((Initialize s) +* (stop (if>0 (a,k1,I,J)))) . a),k1)) =
((Initialize s) +* (stop (if>0 (a,k1,I,J)))) . (DataLoc ((s . a),k1))
by I2, FUNCT_4:12
.=
s . (DataLoc ((s . a),k1))
by A3, I2, FUNCT_4:12
;
A5: if>0 (a,k1,I,J) =
(((a,k1) <=0_goto ((card I) + 2)) ';' (I ';' (Goto ((card J) + 1)))) ';' J
by SCMPDS_4:50
.=
((a,k1) <=0_goto ((card I) + 2)) ';' ((I ';' (Goto ((card J) + 1))) ';' J)
by SCMPDS_4:50
;
then A6:
Shift ((stop ((I ';' (Goto ((card J) + 1))) ';' J)),1) c= Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)
by Lm5;
A7: Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),(0 + 1)) =
Following ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),0)))
by EXTPRO_1:4
.=
Following ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))))
by EXTPRO_1:3
.=
Exec (((a,k1) <=0_goto ((card I) + 2)),((Initialize s) +* (stop (if>0 (a,k1,I,J)))))
by A5, Th22, I2
;
A8:
DataPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = DataPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))
by COMPOS_1:138, FUNCT_7:134;
now let a be
Int_position ;
((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) . a = (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)) . athus ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) . a =
((Initialize s) +* (stop (if>0 (a,k1,I,J)))) . a
by A8, SCMPDS_4:23
.=
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)) . a
by A7, SCMPDS_2:68
;
verum end;
then A9:
DataPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))
by SCMPDS_4:23;
assume
s . (DataLoc ((s . a),k1)) > 0
; ( not I is_closed_on s or not I is_halting_on s or ( if>0 (a,k1,I,J) is_closed_on s & if>0 (a,k1,I,J) is_halting_on s ) )
then A10: IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)) =
succ (IC ((Initialize s) +* (stop (if>0 (a,k1,I,J)))))
by A7, A4, SCMPDS_2:68
.=
0 + 1
by A2
;
assume A11:
I is_closed_on s
; ( not I is_halting_on s or ( if>0 (a,k1,I,J) is_closed_on s & if>0 (a,k1,I,J) is_halting_on s ) )
assume A12:
I is_halting_on s
; ( if>0 (a,k1,I,J) is_closed_on s & if>0 (a,k1,I,J) is_halting_on s )
then A13:
(I ';' (Goto ((card J) + 1))) ';' J is_closed_on s
by A11, Th44;
then A14:
( Initialize (stop ((I ';' (Goto ((card J) + 1))) ';' J)) c= (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) )
by Th38, I1, FUNCT_4:26;
(I ';' (Goto ((card J) + 1))) ';' J is_halting_on s
by A11, A12, Th44;
then A15:
ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) halts_on (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))
by Def3;
A16: card (stop (if>0 (a,k1,I,J))) =
(card (if>0 (a,k1,I,J))) + 1
by SCMPDS_5:7
.=
((card ((I ';' (Goto ((card J) + 1))) ';' J)) + 1) + 1
by A5, Th15
;
now let k be
Element of
NAT ;
IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),b1)) in dom (stop (if>0 (a,k1,I,J)))per cases
( 0 < k or k = 0 )
;
suppose
0 < k
;
IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),b1)) in dom (stop (if>0 (a,k1,I,J)))then consider k1 being
Nat such that A17:
k1 + 1
= k
by NAT_1:6;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 13;
reconsider m =
IC (Comput ((ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),k1)) as
Element of
NAT ;
A18:
card (stop (if>0 (a,k1,I,J))) = (card (stop ((I ';' (Goto ((card J) + 1))) ';' J))) + 1
by A16, SCMPDS_5:7;
m in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J))
by A13, Def2;
then
m < card (stop ((I ';' (Goto ((card J) + 1))) ';' J))
by AFINSQ_1:70;
then A19:
m + 1
< card (stop (if>0 (a,k1,I,J)))
by A18, XREAL_1:8;
T:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))
by AMI_1:123;
IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),k)) =
IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),k1))
by A17, EXTPRO_1:5
.=
m + 1
by A14, A6, A10, A9, Th45, T
;
hence
IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),k)) in dom (stop (if>0 (a,k1,I,J)))
by A19, AFINSQ_1:70;
verum end; suppose
k = 0
;
IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),b1)) in dom (stop (if>0 (a,k1,I,J)))hence
IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),k)) in dom (stop (if>0 (a,k1,I,J)))
by A1, A2, EXTPRO_1:3;
verum end; end;
hence
if>0 (a,k1,I,J) is_closed_on s
by Def2; if>0 (a,k1,I,J) is_halting_on s
T:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))
by AMI_1:123;
x:
Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1)) = Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))))))
by EXTPRO_1:5;
TX4:
ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))))
by AMI_1:123;
TX2:
ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = ProgramPart (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 ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))))
by AMI_1:123;
CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1)))) =
CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))),(Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))))))))
by x, T
.=
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))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))))))))
by A14, A6, A10, A9, Th45, TX2, TX4
.=
halt SCMPDS
by A15, EXTPRO_1:def 14
;
then
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) halts_on (Initialize s) +* (stop (if>0 (a,k1,I,J)))
by EXTPRO_1:30;
hence
if>0 (a,k1,I,J) is_halting_on s
by Def3; verum