let I be No-StopCode Program of ; :: thesis:
let J be Program of ; :: thesis:
let s be State of ; :: thesis:
assume A1: I is_closed_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)));
assume A2: I is_halting_on s ; :: thesis:
set sm = Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))));
A3: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by SCMPDS_4:46;
then A4: 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, Th39;
then A5: IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) by A1, A2, Th43;
A6: inspos 0 in dom (Goto ((card J) + 1)) by Th33;
A7: (((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 A6, SCMPDS_4:37
.= goto ((card J) + 1) by Th33 ;
stop ((I ';' (Goto ((card J) + 1))) ';' J) c= Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:9;
then A8: dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) c= dom (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) by GRFUNC_1:8;
card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by SCMPDS_4:45
.= 1 + (card J) by SCMPDS_5:6 ;
then A9: (((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))))
.= halt SCMPDS by SCMPDS_4:38, SCMPDS_4:73 ;
A10: 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 A11: inspos 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by SCMPDS_4:1;
A12: 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 ;
then A13: card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) by SCMPDS_4:45;
then (card I) + 0 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by A10, XREAL_1:8;
then A14: inspos (card I) in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:1;
A15: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) = 1 + ((card J) + (card (Stop SCMPDS ))) by A10, 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 A16: 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 A13, A15, SCMPDS_4:74;
then ((card I) + (card J)) + 1 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by NAT_1:13;
then A17: inspos (((card I) + (card J)) + 1) in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:1;
A18: 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, A4, 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 A8, A14, FUNCT_4:14
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) . (inspos (0 + (card I))) by A12, A14, SCMPDS_4:33
.= goto ((card J) + 1) by A11, A7, SCMPDS_4:38 ;

A19: 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 A18, SCMPDS_2:66 ; :: thesis:

end;

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 A18, SCMPDS_2:66
.= inspos ((card I) + ((card J) + 1)) by A5, 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 A8, A17, FUNCT_4:14
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) . (inspos ((card I) + ((card J) + 1))) by A12, A17, SCMPDS_4:33
.= halt SCMPDS by A16, A9, SCMPDS_4:38 ;
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))))) by A1, A2, A3, Th39;
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 A19, SCMPDS_4:23; :: thesis:

hereby :: thesis:

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

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, A3, 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 A18, SCMPDS_2:85; :: thesis:

end;

end;

end;

thus IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) by A1, A2, A4, Th43; :: thesis:
thus A24: ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) by A20, AMI_1:146; :: thesis:

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;

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: