let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of st stop I c= P holds
IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I
let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of st stop I c= P holds
IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I
let I be halt-free parahalting Program of ; :: thesis: ( stop I c= P implies IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I )
set Css = Comput (P,s,(LifeSpan (P,s)));
reconsider n = IC (Comput (P,s,(LifeSpan (P,s)))) as Nat ;
assume A1: stop I c= P ; :: thesis: IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I
then A2: P halts_on s by SCMPDS_4:def 7;
A3: P +* (stop I) = P by A1, FUNCT_4:98;
I c= stop I by AFINSQ_1:74;
then A4: I c= P by A1;

now :: thesis: not IC (Comput (P,s,(LifeSpan (P,s)))) in dom I

assume A5: IC (Comput (P,s,(LifeSpan (P,s)))) in dom I ; :: thesis: contradiction
then I . (IC (Comput (P,s,(LifeSpan (P,s))))) = P . (IC (Comput (P,s,(LifeSpan (P,s))))) by A4, GRFUNC_1:2
.= CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) by PBOOLE:143
.= halt SCMPDS by A2, EXTPRO_1:def 15 ;
hence contradiction by A5, COMPOS_1:def 27; :: thesis: verum

end;

then A6: n >= card I by AFINSQ_1:66;
A7: card (stop I) = (card I) + 1 by Lm1, AFINSQ_1:17;
IC (Comput (P,s,(LifeSpan (P,s)))) in dom (stop I) by A1, SCMPDS_4:def 6;
then n < (card I) + 1 by A7, AFINSQ_1:66;
then n <= card I by NAT_1:13;
hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I by A3, A6, XXREAL_0:1; :: thesis: verum