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

A8: now

A9: (ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) by COMPOS_1:38;
A10: ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) by AMI_1:123;
assume A11: n = card I ; :: thesis: contradiction
CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) = ((Initialize s) +* (stop I)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) by A9, AMI_1:54
.= (stop I) . (0 + n) by A5, A6, GRFUNC_1:8
.= halt SCMPDS by A11, Lm1, Lm2, AFINSQ_1:def 4 ;
hence contradiction by A4, A7, A10, EXTPRO_1:def 14; :: thesis: verum

end;

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