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 ;
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
.= CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) by PBOOLE:143
.= halt SCMPDS by ;
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 ;
IC (Comput (P,s,(LifeSpan (P,s)))) in dom (stop I) by ;
then n < (card I) + 1 by ;
then n <= card I by NAT_1:13;
hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I by ; :: thesis: verum