let s be State of SCMPDS ; :: thesis:
let I be Program of SCMPDS ; :: thesis:
let J be shiftable Program of SCMPDS ; :: thesis:
let a be Int_position ; :: thesis:
let k1 be Integer; :: thesis:
set b = DataLoc (s . a),k1;
set pJ = stop J;
set IsJ = Initialized (stop J);
set s1 = s +* (Initialized (stop J));
set IF = if>0 a,k1,I,J;
set pIF = stop (if>0 a,k1,I,J);
set IsIF = Initialized (stop (if>0 a,k1,I,J));
set s3 = s +* (Initialized (stop (if>0 a,k1,I,J)));
set s4 = Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),1;
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:50
.= (a,k1 <=0_goto ((card I) + 2)) ';' ((I ';' (Goto ((card J) + 1))) ';' J) by SCMPDS_4:50 ;
A2: Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),(0 + 1) = Following (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),0 ) by AMI_1:14
.= Following (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))) by AMI_1:13
.= Exec (a,k1 <=0_goto ((card I) + 2)),(s +* (Initialized (stop (if>0 a,k1,I,J)))) by A1, Th22 ;
A3: not DataLoc (s . a),k1 in dom (Initialized (stop (if>0 a,k1,I,J))) by SCMPDS_4:31;
not a in dom (Initialized (stop (if>0 a,k1,I,J))) by SCMPDS_4:31;
then A4: (s +* (Initialized (stop (if>0 a,k1,I,J)))) . (DataLoc ((s +* (Initialized (stop (if>0 a,k1,I,J)))) . a),k1) = (s +* (Initialized (stop (if>0 a,k1,I,J)))) . (DataLoc (s . a),k1) by FUNCT_4:12
.= s . (DataLoc (s . a),k1) by A3, FUNCT_4:12 ;
A5: IC (s +* (Initialized (stop (if>0 a,k1,I,J)))) = 0 by FUNCT_4:26, SCMPDS_5:18;
assume s . (DataLoc (s . a),k1) <= 0 ; :: thesis:
then A6: IC (Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),1) = ICplusConst (s +* (Initialized (stop (if>0 a,k1,I,J)))),((card I) + 2) by A2, A4, SCMPDS_2:68
.= 0 + ((card I) + 2) by A5, Th23 ;
assume A7: J is_closed_on s ; :: thesis:
then A8: ( Initialized (stop J) c= s +* (Initialized (stop J)) & J is_closed_on s +* (Initialized (stop J)) ) by Th38, FUNCT_4:26;
A9: stop (if>0 a,k1,I,J) c= s +* (Initialized (stop (if>0 a,k1,I,J))) by FUNCT_4:26, SCMPDS_4:57;
A10: 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 SCMPDS_4:45
.= (card ((a,k1 <=0_goto ((card I) + 2)) ';' I)) + 1 by SCMPDS_5:6
.= ((card I) + 1) + 1 by Th15
.= (card I) + (1 + 1) ;
then Shift (stop J),((card I) + 2) c= stop (if>0 a,k1,I,J) by Th24;
then Shift (stop J),((card I) + 2) c= s +* (Initialized (stop (if>0 a,k1,I,J))) by A9, XBOOLE_1:1;
then A11: Shift (stop J),((card I) + 2) c= Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),1 by AMI_1:81;
assume J is_halting_on s ; :: thesis:
then A12: ProgramPart (s +* (Initialized (stop J))) halts_on s +* (Initialized (stop J)) by Def3;
A13: DataPart (s +* (Initialized (stop J))) = DataPart (s +* (Initialized (stop (if>0 a,k1,I,J)))) by SCMPDS_4:24, SCMPDS_4:36;

now

let a be Int_position ; :: thesis:
thus (s +* (Initialized (stop J))) . a = (s +* (Initialized (stop (if>0 a,k1,I,J)))) . a by A13, SCMPDS_4:23
.= (Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),1) . a by A2, SCMPDS_2:68 ; :: thesis:

end;

then A14: DataPart (s +* (Initialized (stop J))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),1) by SCMPDS_4:23;

now

let k be Element of NAT ; :: thesis:

per cases ;

suppose 0 < k ; :: thesis:

end;

suppose k = 0 ; :: thesis:

then Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),k = s +* (Initialized (stop (if>0 a,k1,I,J))) by AMI_1:13;
hence IC (Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),k) in dom (stop (if>0 a,k1,I,J)) by A5, SCMPDS_4:75; :: thesis:

end;