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;

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

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

then A6:
n >= card I
by AFINSQ_1:66;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 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

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