let I be No-StopCode Program of SCMPDS ; :: thesis:
let J be Program of SCMPDS ; :: thesis:
let s be State of SCMPDS ; :: thesis:
assume A1: I is_closed_on s ; :: thesis:
assume A2: I is_halting_on s ; :: thesis:
set G1 = Goto ((card J) + 1);
set SS = Stop SCMPDS ;
set J2 = ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS );
set IJ = (I ';' (Goto ((card J) + 1))) ';' J;
set pJ = stop ((I ';' (Goto ((card J) + 1))) ';' J);
set IsJ = Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J));
set s1 = s +* (Initialized (stop I));
set s2 = s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)));
A3: stop ((I ';' (Goto ((card J) + 1))) ';' J) = ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCMPDS ) by SCMPDS_4:def 7
.= (I ';' ((Goto ((card J) + 1)) ';' J)) ';' (Stop SCMPDS ) by SCMPDS_4:46
.= I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by SCMPDS_4:46 ;
A4: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by SCMPDS_4:46;
A5: card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by SCMPDS_4:45
.= 1 + (card J) by SCMPDS_5:6 ;
stop ((I ';' (Goto ((card J) + 1))) ';' J) c= Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:9;
then A6: dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) c= dom (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) by GRFUNC_1:8;
A7: card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) by A3, SCMPDS_4:45;
A8: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) = card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS ))) by SCMPDS_4:46
.= (card (Goto ((card J) + 1))) + (card (J ';' (Stop SCMPDS ))) by SCMPDS_4:45
.= 1 + (card (J ';' (Stop SCMPDS ))) by SCMPDS_5:6 ;
then (card I) + 0 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by A7, XREAL_1:8;
then A9: inspos (card I) in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:1;
A10: inspos 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by A8, SCMPDS_4:1;
A11: inspos 0 in dom (Goto ((card J) + 1)) by Th33;
A12: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . (inspos 0 ) = ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS ))) . (inspos 0 ) by SCMPDS_4:46
.= (Goto ((card J) + 1)) . (inspos 0 ) by A11, SCMPDS_4:37
.= goto ((card J) + 1) by Th33 ;
set sm = Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))));
A13: ( DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) & IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) ) by A1, A2, A4, Th39;
then A14: IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) by A1, A2, Th43;
A15: CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) . (inspos (card I)) by A1, A2, A13, Th43
.= (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) . (inspos (card I)) by AMI_1:54
.= (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) . (inspos (card I)) by A6, A9, FUNCT_4:14
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) . (inspos (0 + (card I))) by A3, A9, SCMPDS_4:33
.= goto ((card J) + 1) by A10, A12, SCMPDS_4:38 ;
A16: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) = 1 + ((card J) + (card (Stop SCMPDS ))) by A8, SCMPDS_4:45
.= (card J) + (1 + (card (Stop SCMPDS ))) ;
then (card J) + 1 < card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by SCMPDS_4:74, XREAL_1:8;
then A17: inspos ((card J) + 1) in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by SCMPDS_4:1;
card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (((card I) + (card J)) + 1) + 1 by A7, A16, SCMPDS_4:74;
then ((card I) + (card J)) + 1 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by NAT_1:13;
then A18: inspos (((card I) + (card J)) + 1) in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:1;
A19: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . (inspos ((card J) + 1)) = (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . (inspos (0 + (card ((Goto ((card J) + 1)) ';' J)))) by A5
.= halt SCMPDS by SCMPDS_4:38, SCMPDS_4:73 ;
thus IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = IC (Following (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))) by AMI_1:14
.= ICplusConst (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))),((card J) + 1) by A15, SCMPDS_2:66
.= inspos ((card I) + ((card J) + 1)) by A14, Th23
.= inspos (((card I) + (card J)) + 1) ; :: thesis:
then A20: CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) . (inspos (((card I) + (card J)) + 1)) by AMI_1:54
.= (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) . (inspos (((card I) + (card J)) + 1)) by A6, A18, FUNCT_4:14
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) . (inspos ((card I) + ((card J) + 1))) by A3, A18, SCMPDS_4:33
.= halt SCMPDS by A17, A19, SCMPDS_4:38 ;

now

let a be Int_position ; :: thesis:
thus (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) . a = (Following (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))) . a by AMI_1:14
.= (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) . a by A15, SCMPDS_2:66 ; :: thesis:

end;

hence DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by A13, SCMPDS_4:23; :: thesis:

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume A22: k <= LifeSpan (s +* (Initialized (stop I))) ; :: thesis:

per cases ;

suppose A23: k < LifeSpan (s +* (Initialized (stop I))) ; :: thesis:

then CurInstr (Computation (s +* (Initialized (stop I))),k) <> halt SCMPDS by A1, A2, Th42;
hence CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS by A1, A2, A4, A23, Th41; :: thesis:

end;

suppose LifeSpan (s +* (Initialized (stop I))) <= k ; :: thesis:

then k = LifeSpan (s +* (Initialized (stop I))) by A22, XXREAL_0:1;
hence CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS by A15, SCMPDS_2:85; :: thesis:

end;

A24: now

let k be Element of NAT ; :: thesis:
assume CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) = halt SCMPDS ; :: thesis:
then LifeSpan (s +* (Initialized (stop I))) < k by A21;
hence (LifeSpan (s +* (Initialized (stop I)))) + 1 <= k by INT_1:20; :: thesis:

end;

thus IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) by A1, A2, A13, Th43; :: thesis:
thus s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) is halting by A20, AMI_1:def 20; :: thesis:
hence LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 by A20, A24, AMI_1:def 46; :: thesis: