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 (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (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 (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = card I )
set IsI = Initialized (stop I);
set s1 = s +* (Initialized (stop I));
assume that
A1: I is_closed_on s and
A2: I is_halting_on s ; :: thesis: IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = card I
set Css = Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))));
reconsider n = IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) as Element of NAT ;
( Initialized (stop I) c= s +* (Initialized (stop I)) & I c= Initialized (stop I) ) by Th17, FUNCT_4:26;
then A3: I c= s +* (Initialized (stop I)) by XBOOLE_1:1;
A4: ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by A2, Def3;

now

Y: (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) /. (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) by AMI_1:150;
assume A5: IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) in dom I ; :: thesis: contradiction
then I . (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) = (s +* (Initialized (stop I))) . (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) by A3, GRFUNC_1:8
.= CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) by AMI_1:54, Y
.= halt SCMPDS by A4, AMI_1:def 46 ;
hence contradiction by A5, SCMPDS_5:def 3; :: thesis: verum

end;

then A6: n >= card I by SCMPDS_4:1;
A7: card (stop I) = (card I) + 1 by SCMPDS_5:7;
IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) in dom (stop I) by A1, Def2;
then n < (card I) + 1 by A7, SCMPDS_4:1;
then n <= card I by NAT_1:13;
hence IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = card I by A6, XXREAL_0:1; :: thesis: verum