let P be Instruction-Sequence of SCMPDS; :: thesis:
let I be halt-free Program of ; :: thesis:
let J be Program of ; :: thesis:
let s be 0 -started State of SCMPDS; :: thesis:
assume A1: I is_closed_on s,P ; :: 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 s1 = s;
set P1 = P +* (stop I);
set s2 = s;
reconsider P2 = P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) as Instruction-Sequence of SCMPDS ;
assume A2: I is_halting_on s,P ; :: thesis:
A3: Initialize s = s by MEMSTR_0:44;
set sm = Comput (P2,s,(LifeSpan ((P +* (stop I)),s)));
A4: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by AFINSQ_1:27;
then A5: IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = IC (Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))) by A1, A2, Th16;
then A6: IC (Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))) = card I by A1, A2, Th20, A3;
A7: 0 in dom (Goto ((card J) + 1)) by Th10;
A8: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . 0 = ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS))) . 0 by AFINSQ_1:27
.= (Goto ((card J) + 1)) . 0 by A7, AFINSQ_1:def 3
.= goto ((card J) + 1) ;
card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by AFINSQ_1:17
.= 1 + (card J) by COMPOS_1:54 ;
then A9: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . ((card J) + 1) = (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . (0 + (card ((Goto ((card J) + 1)) ';' J)))
.= halt SCMPDS by Lm1, Lm2, AFINSQ_1:def 3 ;
A10: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) = card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS))) by AFINSQ_1:27
.= (card (Goto ((card J) + 1))) + (card (J ';' (Stop SCMPDS))) by AFINSQ_1:17
.= 1 + (card (J ';' (Stop SCMPDS))) by COMPOS_1:54 ;
then A11: 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:66;
A12: stop ((I ';' (Goto ((card J) + 1))) ';' J) = ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCMPDS)
.= (I ';' ((Goto ((card J) + 1)) ';' J)) ';' (Stop SCMPDS) by AFINSQ_1:27
.= I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:27 ;
then A13: card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) by AFINSQ_1:17;
0 < card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) ;
then (card I) + 0 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by A13, XREAL_1:6;
then A14: card I in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by AFINSQ_1:66;
A15: card (Stop SCMPDS) = 1 by AFINSQ_1:34;
A16: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) = 1 + ((card J) + (card (Stop SCMPDS))) by A10, AFINSQ_1:17
.= (card J) + (1 + (card (Stop SCMPDS))) ;
then (card J) + 1 < card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by A15, XREAL_1:6;
then A17: (card J) + 1 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:66;
card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (((card I) + (card J)) + 1) + 1 by A13, A16, A15;
then ((card I) + (card J)) + 1 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by NAT_1:13;
then A18: ((card I) + (card J)) + 1 in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by AFINSQ_1:66;
A19: P2 /. (IC (Comput (P2,s,(LifeSpan ((P +* (stop I)),s))))) = P2 . (IC (Comput (P2,s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:143;
A20: CurInstr (P2,(Comput (P2,s,(LifeSpan ((P +* (stop I)),s))))) = P2 . (card I) by A1, A2, A5, Th20, A19, A3
.= P2 . (card I)
.= (stop ((I ';' (Goto ((card J) + 1))) ';' J)) . (card I) by A14, FUNCT_4:13
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . (0 + (card I)) by A12
.= goto ((card J) + 1) by A11, A8, AFINSQ_1:def 3 ;

A21: now :: thesis:

let a be Int_position; :: thesis:
thus (Comput (P2,s,((LifeSpan ((P +* (stop I)),s)) + 1))) . a = (Following (P2,(Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))))) . a by EXTPRO_1:3
.= (Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))) . a by A20, SCMPDS_2:54 ; :: thesis:

end;

A22: P2 /. (IC (Comput (P2,s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = P2 . (IC (Comput (P2,s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by PBOOLE:143;
thus IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 1))) = IC (Following (P2,(Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))))) by EXTPRO_1:3
.= ICplusConst ((Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))),((card J) + 1)) by A20, SCMPDS_2:54
.= (card I) + ((card J) + 1) by A6, Th4
.= ((card I) + (card J)) + 1 ; :: thesis:
then A23: CurInstr (P2,(Comput (P2,s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = P2 . (((card I) + (card J)) + 1) by A22
.= (stop ((I ';' (Goto ((card J) + 1))) ';' J)) . (((card I) + (card J)) + 1) by A18, FUNCT_4:13
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . ((card I) + ((card J) + 1)) by A12
.= halt SCMPDS by A17, A9, AFINSQ_1:def 3 ;
DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))) by A1, A2, A4, Th16;
hence DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 1))) by A21, SCMPDS_4:8; :: thesis:

hereby :: thesis:

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

per cases ;

suppose A26: k < LifeSpan ((P +* (stop I)),s) ; :: thesis:

then CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) <> halt SCMPDS by A1, A2, Th19, A3;
hence CurInstr ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,k))) <> halt SCMPDS by A1, A2, A4, A26, Th18; :: thesis:

end;

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

then k = LifeSpan ((P +* (stop I)),s) by A25, XXREAL_0:1;
hence CurInstr ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,k))) <> halt SCMPDS by A20; :: thesis:

end;

thus IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = card I by A1, A2, A5, Th20, A3; :: thesis:
thus A27: P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) halts_on s by A23, EXTPRO_1:29; :: thesis:

now :: thesis:

let k be Nat; :: thesis:
A28: k in NAT by ORDINAL1:def 12;
assume CurInstr (P2,(Comput (P2,s,k))) = halt SCMPDS ; :: thesis:
then LifeSpan ((P +* (stop I)),s) < k by A24, A28;
hence (LifeSpan ((P +* (stop I)),s)) + 1 <= k by INT_1:7; :: thesis:

end;

hence LifeSpan ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + 1 by A23, A27, EXTPRO_1:def 15; :: thesis: