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);
set i = (a,k1) >=0_goto ((card I) + 2);
A1:
s +* (Initialize (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))
by COMPOS_1:125;
A2:
s +* (Initialize (stop (if<0 (a,k1,I,J)))) = (Initialize s) +* (stop (if<0 (a,k1,I,J)))
by COMPOS_1:125;
A3:
0 in dom (stop (if<0 (a,k1,I,J)))
by COMPOS_1:135;
A4:
IC ((Initialize s) +* (stop (if<0 (a,k1,I,J)))) = 0
by A2, FUNCT_4:26, SCMPDS_5:18;
A5:
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 A6: ((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 A2, FUNCT_4:12
.=
s . (DataLoc ((s . a),k1))
by A5, A2, FUNCT_4:12
;
A7: 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 A8:
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 Lm6;
A9: 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 A7, Th22, A2
;
A10:
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 A10, 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 A9, SCMPDS_2:69
;
verum end;
then A11:
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 A12: 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 A9, A6, SCMPDS_2:69
.=
0 + 1
by A4
;
assume A13:
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 A14:
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 A15:
(I ';' (Goto ((card J) + 1))) ';' J is_closed_on s
by A13, Th44;
then A16:
( 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, A1, FUNCT_4:26;
(I ';' (Goto ((card J) + 1))) ';' J is_halting_on s
by A13, A14, Th44;
then A17:
ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) halts_on (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))
by Def3;
A18: 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 A7, 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 A19:
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 ;
A20:
card (stop (if<0 (a,k1,I,J))) = (card (stop ((I ';' (Goto ((card J) + 1))) ';' J))) + 1
by A18, SCMPDS_5:7;
m in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J))
by A15, Def2;
then
m < card (stop ((I ';' (Goto ((card J) + 1))) ';' J))
by AFINSQ_1:70;
then A21:
m + 1
< card (stop (if<0 (a,k1,I,J)))
by A20, XREAL_1:8;
A22:
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 A19, EXTPRO_1:5
.=
m + 1
by A16, A8, A12, A11, Th45, A22
;
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 A21, 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 A3, A4, 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
A23:
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;
A24:
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;
A25:
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;
A26:
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 A24, A23
.=
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 A16, A8, A12, A11, Th45, A26, A25
.=
halt SCMPDS
by A17, 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