let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
let I be halt-free 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,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 = Initialize s;
set P1 = P +* (stop I);
set s2 = Initialize s;
reconsider P2 = P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) as the Instructions of SCMPDS -valued ManySortedSet of NAT ;
assume A4: I is_halting_on s,P ; :: thesis:
set sm = Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
A5: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by AFINSQ_1:30;
then A6: IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = IC (Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A1, A4, Th39;
then A7: IC (Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I by A1, A4, Th43;
A8: 0 in dom (Goto ((card J) + 1)) by Th33;
A9: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . 0 = ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS))) . 0 by AFINSQ_1:30
.= (Goto ((card J) + 1)) . 0 by A8, AFINSQ_1:def 4
.= goto ((card J) + 1) by Th33 ;
card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by AFINSQ_1:20
.= 1 + (card J) by SCMPDS_5:6 ;
then A11: (((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 4 ;
A12: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) = card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS))) by AFINSQ_1:30
.= (card (Goto ((card J) + 1))) + (card (J ';' (Stop SCMPDS))) by AFINSQ_1:20
.= 1 + (card (J ';' (Stop SCMPDS))) by SCMPDS_5:6 ;
then A13: 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:70;
A14: 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:30
.= I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:30 ;
then A15: card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) by AFINSQ_1:20;
then (card I) + 0 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by XREAL_1:8;
then A16: card I in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by AFINSQ_1:70;
A17: card (Stop SCMPDS) = 1 by COMPOS_1:46;
A18: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) = 1 + ((card J) + (card (Stop SCMPDS))) by A12, AFINSQ_1:20
.= (card J) + (1 + (card (Stop SCMPDS))) ;
then (card J) + 1 < card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by A17, XREAL_1:8;
then A19: (card J) + 1 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:70;
card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (((card I) + (card J)) + 1) + 1 by A15, A18, A17;
then ((card I) + (card J)) + 1 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by NAT_1:13;
then A20: ((card I) + (card J)) + 1 in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by AFINSQ_1:70;
A21: P2 /. (IC (Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = P2 . (IC (Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by PBOOLE:158;
A23: CurInstr (P2,(Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = P2 . (card I) by A1, A4, A6, Th43, A21
.= P2 . (card I)
.= (stop ((I ';' (Goto ((card J) + 1))) ';' J)) . (card I) by A16, FUNCT_4:14
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . (0 + (card I)) by A14
.= goto ((card J) + 1) by A13, A9, AFINSQ_1:def 4 ;

A24: now

let a be Int_position ; :: thesis:
thus (Comput (P2,(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))) . a = (Following (P2,(Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))) . a by EXTPRO_1:4
.= (Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by A23, SCMPDS_2:66 ; :: thesis:

end;

A25: P2 /. (IC (Comput (P2,(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) = P2 . (IC (Comput (P2,(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) by PBOOLE:158;
thus IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))) = IC (Following (P2,(Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))) by EXTPRO_1:4
.= ICplusConst ((Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))),((card J) + 1)) by A23, SCMPDS_2:66
.= (card I) + ((card J) + 1) by A7, Th23
.= ((card I) + (card J)) + 1 ; :: thesis:
then A27: CurInstr (P2,(Comput (P2,(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) = P2 . (((card I) + (card J)) + 1) by A25
.= (stop ((I ';' (Goto ((card J) + 1))) ';' J)) . (((card I) + (card J)) + 1) by A20, FUNCT_4:14
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . ((card I) + ((card J) + 1)) by A14
.= halt SCMPDS by A19, A11, AFINSQ_1:def 4 ;
DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Comput (P2,(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A1, A4, A5, Th39;
hence DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))) by A24, SCMPDS_4:23; :: thesis:

hereby :: thesis:

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

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

then CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS by A1, A4, Th42;
hence CurInstr ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s),k))) <> halt SCMPDS by A1, A4, A5, A31, Th41; :: thesis:

end;

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

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

end;

end;

end;

thus IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I by A1, A4, A6, Th43; :: thesis:
thus A32: P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) halts_on Initialize s by A27, EXTPRO_1:30; :: thesis:

let k be Element of NAT ; :: thesis:
assume CurInstr (P2,(Comput (P2,(Initialize s),k))) = halt SCMPDS ; :: thesis:
then LifeSpan ((P +* (stop I)),(Initialize s)) < k by A28;
hence (LifeSpan ((P +* (stop I)),(Initialize s))) + 1 <= k by INT_1:20; :: thesis:

end;

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