let P be Instruction-Sequence of SCMPDS; for s being State of SCMPDS
for I being Program of
for J being shiftable Program of
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & J is_closed_on s,P & J is_halting_on s,P holds
( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P )
let s be State of SCMPDS; for I being Program of
for J being shiftable Program of
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & J is_closed_on s,P & J is_halting_on s,P holds
( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P )
let I be Program of ; for J being shiftable Program of
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & J is_closed_on s,P & J is_halting_on s,P holds
( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P )
let J be shiftable Program of ; for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & J is_closed_on s,P & J is_halting_on s,P holds
( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P )
let a be Int_position; for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & J is_closed_on s,P & J is_halting_on s,P holds
( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P )
let k1 be Integer; ( s . (DataLoc ((s . a),k1)) >= 0 & J is_closed_on s,P & J is_halting_on s,P implies ( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P ) )
set b = DataLoc ((s . a),k1);
set pJ = stop J;
set s1 = Initialize s;
set P1 = P +* (stop J);
set IF = if<0 (a,k1,I,J);
set pIF = stop (if<0 (a,k1,I,J));
set s3 = Initialize s;
set P3 = P +* (stop (if<0 (a,k1,I,J)));
set s4 = Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),1);
set P4 = P +* (stop (if<0 (a,k1,I,J)));
set i = (a,k1) >=0_goto ((card I) + 2);
set G = Goto ((card J) + 1);
set iG = (((a,k1) >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1));
A1: if<0 (a,k1,I,J) =
(((a,k1) >=0_goto ((card I) + 2)) ';' (I ';' (Goto ((card J) + 1)))) ';' J
by SCMPDS_4:14
.=
((a,k1) >=0_goto ((card I) + 2)) ';' ((I ';' (Goto ((card J) + 1))) ';' J)
by SCMPDS_4:14
;
A2: Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),(0 + 1)) =
Following ((P +* (stop (if<0 (a,k1,I,J)))),(Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),0)))
by EXTPRO_1:3
.=
Following ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s))
by EXTPRO_1:2
.=
Exec (((a,k1) >=0_goto ((card I) + 2)),(Initialize s))
by A1, Th3
;
A3:
not DataLoc ((s . a),k1) in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
not a in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
then A4: (Initialize s) . (DataLoc (((Initialize s) . a),k1)) =
(Initialize s) . (DataLoc ((s . a),k1))
by FUNCT_4:11
.=
s . (DataLoc ((s . a),k1))
by A3, FUNCT_4:11
;
A5:
IC (Initialize s) = 0
by MEMSTR_0:47;
assume
s . (DataLoc ((s . a),k1)) >= 0
; ( not J is_closed_on s,P or not J is_halting_on s,P or ( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P ) )
then A6: IC (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),1)) =
ICplusConst ((Initialize s),((card I) + 2))
by A2, A4, SCMPDS_2:57
.=
0 + ((card I) + 2)
by A5, Th4
;
assume A7:
J is_closed_on s,P
; ( not J is_halting_on s,P or ( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P ) )
then A8:
( Start-At (0,SCMPDS) c= Initialize s & J is_closed_on Initialize s,P +* (stop J) )
by FUNCT_4:25;
A9:
stop J c= P +* (stop J)
by FUNCT_4:25;
A10:
stop (if<0 (a,k1,I,J)) c= P +* (stop (if<0 (a,k1,I,J)))
by FUNCT_4:25;
A11: card ((((a,k1) >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) =
(card (((a,k1) >=0_goto ((card I) + 2)) ';' I)) + (card (Goto ((card J) + 1)))
by AFINSQ_1:17
.=
(card (((a,k1) >=0_goto ((card I) + 2)) ';' I)) + 1
by COMPOS_1:54
.=
((card I) + 1) + 1
by Th1
.=
(card I) + (1 + 1)
;
then
Shift ((stop J),((card I) + 2)) c= stop (if<0 (a,k1,I,J))
by Th5;
then
Shift ((stop J),((card I) + 2)) c= P +* (stop (if<0 (a,k1,I,J)))
by A10, XBOOLE_1:1;
then A12:
Shift ((stop J),((card I) + 2)) c= P +* (stop (if<0 (a,k1,I,J)))
;
assume
J is_halting_on s,P
; ( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P )
then A13:
P +* (stop J) halts_on Initialize s
;
for a being Int_position holds (Initialize s) . a = (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),1)) . a
by A2, SCMPDS_2:57;
then A14:
DataPart (Initialize s) = DataPart (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),1))
by SCMPDS_4:8;
now for k being Nat holds IC (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),k)) in dom (stop (if<0 (a,k1,I,J)))let k be
Nat;
IC (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),b1)) in dom (stop (if<0 (a,k1,I,J)))per cases
( 0 < k or k = 0 )
;
suppose
0 < k
;
IC (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),b1)) in dom (stop (if<0 (a,k1,I,J)))then consider k1 being
Nat such that A15:
k1 + 1
= k
by NAT_1:6;
reconsider k1 =
k1 as
Nat ;
reconsider m =
IC (Comput ((P +* (stop J)),(Initialize s),k1)) as
Nat ;
m in dom (stop J)
by A7;
then
m < card (stop J)
by AFINSQ_1:66;
then A16:
m + ((card I) + 2) < (card (stop J)) + ((card I) + 2)
by XREAL_1:6;
A17:
card (stop J) = (card J) + 1
by COMPOS_1:55;
A18:
card (stop (if<0 (a,k1,I,J))) =
(card (if<0 (a,k1,I,J))) + 1
by COMPOS_1:55
.=
(((card I) + 2) + (card J)) + 1
by A11, AFINSQ_1:17
.=
((card I) + 2) + (card (stop J))
by A17
;
IC (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),k)) =
IC (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),1)),k1))
by A15, EXTPRO_1:4
.=
m + ((card I) + 2)
by A8, A14, A12, A6, Th22, A9
;
hence
IC (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),k)) in dom (stop (if<0 (a,k1,I,J)))
by A18, A16, AFINSQ_1:66;
verum end; suppose
k = 0
;
IC (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),b1)) in dom (stop (if<0 (a,k1,I,J)))then
Comput (
(P +* (stop (if<0 (a,k1,I,J)))),
(Initialize s),
k)
= Initialize s
by EXTPRO_1:2;
hence
IC (Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),k)) in dom (stop (if<0 (a,k1,I,J)))
by A5, COMPOS_1:36;
verum end; end; end;
hence
if<0 (a,k1,I,J) is_closed_on s,P
; if<0 (a,k1,I,J) is_halting_on s,P
A19:
Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),((LifeSpan ((P +* (stop J)),(Initialize s))) + 1)) = Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),1)),(LifeSpan ((P +* (stop J)),(Initialize s))))
by EXTPRO_1:4;
CurInstr ((P +* (stop (if<0 (a,k1,I,J)))),(Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),((LifeSpan ((P +* (stop J)),(Initialize s))) + 1)))) =
CurInstr ((P +* (stop (if<0 (a,k1,I,J)))),(Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Comput ((P +* (stop (if<0 (a,k1,I,J)))),(Initialize s),1)),(LifeSpan ((P +* (stop J)),(Initialize s))))))
by A19
.=
CurInstr ((P +* (stop J)),(Comput ((P +* (stop J)),(Initialize s),(LifeSpan ((P +* (stop J)),(Initialize s))))))
by A8, A14, A12, A6, Th22, A9
.=
halt SCMPDS
by A13, EXTPRO_1:def 15
;
then
P +* (stop (if<0 (a,k1,I,J))) halts_on Initialize s
by EXTPRO_1:29;
hence
if<0 (a,k1,I,J) is_halting_on s,P
; verum