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 ; :: 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) +* (stop I);
set s2 = (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J));
I1: (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = s +* (Initialize (stop ((I ';' (Goto ((card J) + 1))) ';' J))) by SCMPDS_4:5;
I2: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by SCMPDS_4:5;
assume A2: I is_halting_on s ; :: thesis:
set sm = Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
A3: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by SCMPDS_4:46;
then A4: IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by A1, A2, Th39;
then A5: IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = card I by A1, A2, Th43, I2;
A6: 0 in dom (Goto ((card J) + 1)) by Th33;
A7: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . 0 = ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS ))) . 0 by SCMPDS_4:46
.= (Goto ((card J) + 1)) . 0 by A6, SCMPDS_4:37
.= goto ((card J) + 1) by Th33 ;
stop ((I ';' (Goto ((card J) + 1))) ';' J) c= Initialize (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:9;
then A8: dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) c= dom (Initialize (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 )) . ((card J) + 1) = (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . (0 + (card ((Goto ((card J) + 1)) ';' J)))
.= halt SCMPDS by JJ, KK, SCMPDS_4:38 ;
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: 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by AFINSQ_1:70;
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 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: card I in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by AFINSQ_1:70;
X: card (Stop SCMPDS ) = 1 by COMPOS_1:46;
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 X, XREAL_1:8;
then A16: (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 A13, A15, X;
then ((card I) + (card J)) + 1 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by NAT_1:13;
then A17: ((card I) + (card J)) + 1 in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by AFINSQ_1:70;
Y: (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) = (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . (IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) by COMPOS_1:38;
TX: ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by AMI_1:123;
A18: CurInstr (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . (card I) by A1, A2, A4, Th43, Y, TX, I2
.= ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) . (card I) by AMI_1:54
.= (Initialize (stop ((I ';' (Goto ((card J) + 1))) ';' J))) . (card I) by A8, A14, I1, FUNCT_4:14
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) . (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 (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) . a = (Following (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) . a by AMI_1:14
.= (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . a by A18, SCMPDS_2:66 ; :: thesis:

end;

Y: (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))) = (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) . (IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))) by COMPOS_1:38;
TX2: ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) by AMI_1:123;
thus IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) = IC (Following (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) by AMI_1:14
.= ICplusConst (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))),((card J) + 1) by A18, SCMPDS_2:66
.= (card I) + ((card J) + 1) by A5, Th23
.= ((card I) + (card J)) + 1 ; :: thesis:
then A20: CurInstr (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) = ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) . (((card I) + (card J)) + 1) by Y, TX2, AMI_1:54
.= (Initialize (stop ((I ';' (Goto ((card J) + 1))) ';' J))) . (((card I) + (card J)) + 1) by A8, A17, I1, FUNCT_4:14
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) . ((card I) + ((card J) + 1)) by A12, A17, SCMPDS_4:33
.= halt SCMPDS by A16, A9, SCMPDS_4:38 ;
DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by A1, A2, A3, Th39;
hence DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) by A19, SCMPDS_4:23; :: thesis:

hereby :: thesis:

let k be Element of NAT ; :: thesis:
TX1: ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) by AMI_1:123;
assume A22: k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) ; :: thesis:

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

then CurInstr (ProgramPart ((Initialize s) +* (stop I))),(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) <> halt SCMPDS by A1, A2, Th42, TX1;
hence CurInstr (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),k) <> halt SCMPDS by A1, A2, A3, A23, Th41; :: thesis:

end;

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

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

end;

end;

end;

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

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

end;

hence LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1 by A20, A24, AMI_1:def 46; :: thesis: