let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of SCMPDS st stop I c= s holds
IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)))))) = card I
let I be halt-free parahalting Program of SCMPDS; :: thesis: ( stop I c= s implies IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)))))) = card I )
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: stop I c= s ; :: thesis: IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)))))) = card I
then A3: ProgramPart s halts_on s by SCMPDS_4:def 10;
X: s +* (stop I) = s by A2, FUNCT_4:79;
I c= stop I by AFINSQ_1:78;
then A4: I c= s by A2, XBOOLE_1:1;

now

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 COMPOS_1:38
.= halt SCMPDS by A3, EXTPRO_1:def 14 ;
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, AFINSQ_1:20;
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;
hence IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)))))) = card I by X, A6, XXREAL_0:1; :: thesis: verum