let I be halt-free Program of SCMPDS; :: thesis: for s being State of SCMPDS st I is_closed_on s & I is_halting_on s holds
IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),(s +* (Initialize (stop I))))))) = card I
let s be State of SCMPDS; :: thesis: ( I is_closed_on s & I is_halting_on s implies IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),(s +* (Initialize (stop I))))))) = card I )
set s1 = (Initialize s) +* (stop I);
A1: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by COMPOS_1:125;
assume that
A2: I is_closed_on s and
A3: I is_halting_on s ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),(s +* (Initialize (stop I))))))) = card I
set Css = Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))));
reconsider n = IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) as Element of NAT ;
( Initialize (stop I) c= (Initialize s) +* (stop I) & I c= Initialize (stop I) ) by Th17, A1, FUNCT_4:26;
then A4: I c= (Initialize s) +* (stop I) by XBOOLE_1:1;
A5: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by A3, Def3;
A6: ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = ProgramPart ((Initialize s) +* (stop I)) by AMI_1:123;

now

A7: (ProgramPart (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))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = (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))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by COMPOS_1:38;
assume A8: IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) in dom I ; :: thesis: contradiction
then I . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = ((Initialize s) +* (stop I)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by A4, GRFUNC_1:8
.= CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by A7, AMI_1:54
.= halt SCMPDS by A5, A6, EXTPRO_1:def 14 ;
hence contradiction by A8, SCMPDS_5:def 3; :: thesis: verum

end;

then A9: n >= card I by AFINSQ_1:70;
A10: card (stop I) = (card I) + 1 by SCMPDS_5:7;
IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) in dom (stop I) by A2, Def2;
then n < (card I) + 1 by A10, AFINSQ_1:70;
then n <= card I by NAT_1:13;
hence IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),(s +* (Initialize (stop I))))))) = card I by A9, A1, XXREAL_0:1; :: thesis: verum