let s be State of SCMPDS ; :: thesis: for I being parahalting No-StopCode Program of SCMPDS st Initialized (stop I) c= s holds
IC (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))) = card I
let I be parahalting No-StopCode Program of SCMPDS ; :: thesis: ( Initialized (stop I) c= s implies IC (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))) = card I )
set IsI = Initialized (stop I);
A1: stop I c= Initialized (stop I) by SCMPDS_4:9;
set Css = Comput (ProgramPart s),s,(LifeSpan s);
reconsider n = IC (Comput (ProgramPart s),s,(LifeSpan s)) as Element of NAT ;
assume A2: Initialized (stop I) c= s ; :: thesis: IC (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))) = card I
then A3: ProgramPart s halts_on s by SCMPDS_4:63;
I c= stop I by SCMPDS_4:40;
then I c= Initialized (stop I) by A1, XBOOLE_1:1;
then A4: I c= s by A2, XBOOLE_1:1;

now

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

end;

then A6: n >= card I by SCMPDS_4:1;
A7: card (stop I) = (card I) + 1 by SCMPDS_4:45, LL;
IC (Comput (ProgramPart s),s,(LifeSpan s)) in dom (stop I) by A2, SCMPDS_4:def 9;
then n < (card I) + 1 by A7, SCMPDS_4:1;
then n <= card I by NAT_1:13;
then n = card I by A6, XXREAL_0:1;
hence IC (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))) = card I by A2, FUNCT_4:79; :: thesis: verum