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

now

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

end;

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