let s be State of SCMPDS ; :: thesis:
let I, J be shiftable Program of SCMPDS ; :: thesis:
let a be Int_position ; :: thesis:
let k1 be Integer; :: thesis:
set b = DataLoc (s . a),k1;
assume A1: s . (DataLoc (s . a),k1) = 0 ; :: thesis:
assume A2: I is_closed_on s ; :: thesis:
assume A3: I is_halting_on s ; :: thesis:
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 IsIF = Initialized (stop (if=0 a,k1,I,J));
set pI2 = stop ((I ';' (Goto ((card J) + 1))) ';' J);
set II2 = Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J));
set s2 = s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)));
set s3 = s +* (Initialized (stop (if=0 a,k1,I,J)));
set s4 = Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1;
set i = a,k1 <>0_goto ((card I) + 2);
A4: Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)) c= s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) by FUNCT_4:26;
(I ';' (Goto ((card J) + 1))) ';' J is_halting_on s by A2, A3, Th44;
then A5: s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) is halting by Def3;
A6: (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s by A2, A3, Th44;
then A7: (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) by Th38;
A8: inspos 0 in dom (stop (if=0 a,k1,I,J)) by SCMPDS_4:75;
A9: 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 ;
A10: IC (s +* (Initialized (stop (if=0 a,k1,I,J)))) = inspos 0 by FUNCT_4:26, SCMPDS_5:18;
A11: Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),(0 + 1) = Following (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),0 ) by AMI_1:14
.= Following (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 A9, Th22 ;
A12: ( not a in dom (Initialized (stop (if=0 a,k1,I,J))) & a in dom s ) by SCMPDS_2:49, SCMPDS_4:31;
A13: ( not DataLoc (s . a),k1 in dom (Initialized (stop (if=0 a,k1,I,J))) & DataLoc (s . a),k1 in dom s ) by SCMPDS_2:49, SCMPDS_4:31;
A14: (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 A12, FUNCT_4:12
.= 0 by A1, A13, FUNCT_4:12 ;
A15: 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 A9, Th15 ;
A16: Shift (stop ((I ';' (Goto ((card J) + 1))) ';' J)),1 c= Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1 by A9, Lm6;
A18: IC (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1) = Next (IC (s +* (Initialized (stop (if=0 a,k1,I,J))))) by A11, A14, SCMPDS_2:67
.= inspos (0 + 1) by A10 ;
A19: DataPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' 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 ((I ';' (Goto ((card J) + 1))) ';' J)))) . a = (s +* (Initialized (stop (if=0 a,k1,I,J)))) . a by A19, SCMPDS_4:23
.= (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1) . a by A11, SCMPDS_2:67 ; :: thesis:

end;

then A20: DataPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = DataPart (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1) by SCMPDS_4:23;
CurInstr (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),((LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1)) = CurInstr (Computation (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1),(LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))) by AMI_1:51
.= CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))) by A4, A7, A16, A18, A20, Th45
.= halt SCMPDS by A5, AMI_1:def 46 ;
then A21: s +* (Initialized (stop (if=0 a,k1,I,J))) is halting by AMI_1:def 20;

now

let k be Element of NAT ; :: thesis:

per cases ;

suppose 0 < k ; :: thesis:

then consider k1 being Nat such that
A22: k1 + 1 = k by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
reconsider m = IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k1) as Element of NAT by ORDINAL1:def 13;
A24: card (stop (if=0 a,k1,I,J)) = (card (stop ((I ';' (Goto ((card J) + 1))) ';' J))) + 1 by A15, SCMPDS_5:7;
inspos m in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by A6, Def2;
then m < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:1;
then A25: m + 1 < card (stop (if=0 a,k1,I,J)) by A24, XREAL_1:8;
IC (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),k) = IC (Computation (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1),k1) by A22, AMI_1:51
.= inspos (m + 1) by A4, A7, A16, A18, A20, Th45 ;
hence IC (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),k) in dom (stop (if=0 a,k1,I,J)) by A25, SCMPDS_4:1; :: thesis:

end;

suppose k = 0 ; :: thesis:

hence IC (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),k) in dom (stop (if=0 a,k1,I,J)) by A8, A10, AMI_1:13; :: thesis:

end;

hence if=0 a,k1,I,J is_closed_on s by Def2; :: thesis:
thus if=0 a,k1,I,J is_halting_on s by A21, Def3; :: thesis: