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 ;
I1: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by SCMPDS_4:5;
assume that
A1: I is_closed_on s and
A2: I is_halting_on s and
A3: 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);
A4: IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) in dom (stop I) by A1, 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 I1, FUNCT_4:26, SCMPDS_4:9;
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 A2, Def3;

A8: now

Y: (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;
TX: ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) by AMI_1:123;
assume A9: 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 Y, AMI_1:54
.= (stop I) . (0 + n) by A4, A6, GRFUNC_1:8
.= halt SCMPDS by A9, JJ, KK, SCMPDS_4:38 ;
hence contradiction by A3, A7, TX, AMI_1:def 46; :: thesis: verum

end;

card (stop I) = (card I) + 1 by SCMPDS_5:7;
then n < (card I) + 1 by A4, 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