let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS
for k being Element of NAT st k < LifeSpan ((P +* (stop I)),s) holds
IC (Comput ((P +* (stop I)),s,k)) in dom I
let s be 0 -started State of SCMPDS; :: thesis: for I being parahalting Program of SCMPDS
for k being Element of NAT st k < LifeSpan ((P +* (stop I)),s) holds
IC (Comput ((P +* (stop I)),s,k)) in dom I
let I be parahalting Program of SCMPDS; :: thesis: for k being Element of NAT st k < LifeSpan ((P +* (stop I)),s) holds
IC (Comput ((P +* (stop I)),s,k)) in dom I
let k be Element of NAT ; :: thesis: ( k < LifeSpan ((P +* (stop I)),s) implies IC (Comput ((P +* (stop I)),s,k)) in dom I )
set ss = s;
set PP = P +* (stop I);
set m = LifeSpan ((P +* (stop I)),s);
set Sk = Comput ((P +* (stop I)),s,k);
set Ik = IC (Comput ((P +* (stop I)),s,k));
XX: stop I c= P +* (stop I) by FUNCT_4:25;
then A1: P +* (stop I) halts_on s by SCMPDS_4:def 7;
reconsider n = IC (Comput ((P +* (stop I)),s,k)) as Element of NAT ;
A2: IC (Comput ((P +* (stop I)),s,k)) in dom (stop I) by XX, SCMPDS_4:def 6;
A3: stop I c= P +* (stop I) by FUNCT_4:25;
assume A4: k < LifeSpan ((P +* (stop I)),s) ; :: thesis: IC (Comput ((P +* (stop I)),s,k)) in dom I

A5: now

assume A6: n = card I ; :: thesis: contradiction
A7: 0 in dom (Stop SCMPDS) by COMPOS_1:3;
A8: (Stop SCMPDS) . 0 = halt SCMPDS by AFINSQ_1:34;
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,k))) by PBOOLE:143
.= (stop I) . (0 + n) by A2, A3, GRFUNC_1:2
.= halt SCMPDS by A6, A8, A7, AFINSQ_1:def 3 ;
hence contradiction by A4, A1, EXTPRO_1:def 15; :: thesis: verum

end;

card (stop I) = (card I) + 1 by Lm1, AFINSQ_1:17;
then n < (card I) + 1 by A2, AFINSQ_1:66;
then n <= card I by INT_1:7;
then n < card I by A5, XXREAL_0:1;
hence IC (Comput ((P +* (stop I)),s,k)) in dom I by AFINSQ_1:66; :: thesis: verum