let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I being Program of SCMPDS
for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I
let P be Instruction-Sequence of SCMPDS; :: thesis: for I being Program of SCMPDS
for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I
let I be Program of SCMPDS; :: thesis: for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I
let k be Element of NAT ; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) implies IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I )
set ss = Initialize s;
set PP = P +* (stop I);
set m = LifeSpan ((P +* (stop I)),(Initialize s));
set Sp = Stop SCMPDS;
assume that
A2: I is_closed_on s,P and
A3: I is_halting_on s,P and
A4: k < LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I
set Sk = Comput ((P +* (stop I)),(Initialize s),k);
set Ik = IC (Comput ((P +* (stop I)),(Initialize s),k));
A5: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) by A2, Def2;
reconsider n = IC (Comput ((P +* (stop I)),(Initialize s),k)) as Element of NAT ;
A6: stop I c= P +* (stop I) by FUNCT_4:25;
A7: P +* (stop I) halts_on Initialize s by A3, Def3;

A8: now

A9: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),(Initialize s),k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by PBOOLE:143;
assume A11: n = card I ; :: thesis: contradiction
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A9
.= (stop I) . (0 + n) by A5, A6, GRFUNC_1:2
.= halt SCMPDS by A11, Lm1, Lm2, AFINSQ_1:def 3 ;
hence contradiction by A4, A7, EXTPRO_1:def 15; :: thesis: verum

end;

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