let s be State of SCMPDS ; :: thesis: for I being halt-free parahalting Program of SCMPDS st Initialized (stop I) c= s holds
IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))))) = card I
let I be halt-free parahalting Program of SCMPDS ; :: thesis: ( Initialized (stop I) c= s implies IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart (s +* (Initialized (stop I)))),(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 (ProgramPart s),s);
reconsider n = IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s)) as Element of NAT ;
assume A2: Initialized (stop I) c= s ; :: thesis: IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))))) = card I
then A3: ProgramPart s halts_on s by SCMPDS_4:63;
X: ( (Initialized (stop I)) +* s = s & s +* (Initialized (stop I)) = s ) by A2, FUNCT_4:79;
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 (ProgramPart s),s))) /. (IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s))) = (Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s)) . (IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s))) by AMI_1:150;
TX: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s)) by AMI_1:123;
assume A5: IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s)) in dom I ; :: thesis: contradiction
then I . (IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s))) = s . (IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s))) by A4, GRFUNC_1:8
.= CurInstr (ProgramPart s),(Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s)) by Y, TX, AMI_1:54
.= halt SCMPDS by A3, AMI_1:def 46 ;
hence contradiction by A5, Def3; :: thesis: verum

end;

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