let I be No-StopCode Program of SCMPDS ; :: thesis: for s being State of SCMPDS st I is_closed_on s & I is_halting_on s holds
IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I)
let s be State of SCMPDS ; :: thesis: ( I is_closed_on s & I is_halting_on s implies IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) )
set IsI = Initialized (stop I);
set s1 = s +* (Initialized (stop I));
assume A1: ( I is_closed_on s & I is_halting_on s ) ; :: thesis: IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I)
then A2: s +* (Initialized (stop I)) is halting by Def3;
A3: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
I c= Initialized (stop I) by Th17;
then A4: I c= s +* (Initialized (stop I)) by A3, XBOOLE_1:1;
set Css = Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))));
A5: IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) in dom (stop I) by A1, Def2;
reconsider n = IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) as Element of NAT by ORDINAL1:def 13;

now

assume A7: IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) in dom I ; :: thesis: contradiction
then I . (IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) = (s +* (Initialized (stop I))) . (IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) by A4, GRFUNC_1:8
.= CurInstr (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) by AMI_1:54
.= halt SCMPDS by A2, AMI_1:def 46 ;
hence contradiction by A7, SCMPDS_5:def 3; :: thesis: verum

end;

then A8: n >= card I by SCMPDS_4:1;
card (stop I) = (card I) + 1 by SCMPDS_5:7;
then n < (card I) + 1 by A5, SCMPDS_4:1;
then n <= card I by NAT_1:13;
hence IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) by A8, XXREAL_0:1; :: thesis: verum