let s be State of SCMPDS ; :: thesis: for I being parahalting Program of SCMPDS
for k being Element of NAT st k < LifeSpan (s +* (Initialized (stop I))) holds
IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) in dom I
let I be parahalting Program of SCMPDS ; :: thesis: for k being Element of NAT st k < LifeSpan (s +* (Initialized (stop I))) holds
IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) in dom I
let k be Element of NAT ; :: thesis: ( k < LifeSpan (s +* (Initialized (stop I))) implies IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) in dom I )
set IsI = Initialized (stop I);
set ss = s +* (Initialized (stop I));
set m = LifeSpan (s +* (Initialized (stop I)));
set Sk = Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k;
set Ik = IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k);
A1: ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by FUNCT_4:26, SCMPDS_4:63;
reconsider n = IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) as Element of NAT ;
A2: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
then A3: IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) in dom (stop I) by SCMPDS_4:def 9;
stop I c= Initialized (stop I) by SCMPDS_4:9;
then A4: stop I c= s +* (Initialized (stop I)) by A2, XBOOLE_1:1;
assume A5: k < LifeSpan (s +* (Initialized (stop I))) ; :: thesis: IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) in dom I

A6: now

Y: (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)) /. (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)) = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) . (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)) by AMI_1:150;
assume A7: n = card I ; :: thesis: contradiction
y: 0 in dom (Stop SCMPDS ) by SCMNORM:2;
x: (Stop SCMPDS ) . 0 = halt SCMPDS by AFINSQ_1:38;
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) = (s +* (Initialized (stop I))) . (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)) by AMI_1:54, Y
.= (stop I) . (0 + n) by A3, A4, GRFUNC_1:8
.= halt SCMPDS by A7, SCMPDS_4:38, x, y ;
hence contradiction by A5, A1, AMI_1:def 46; :: thesis: verum

end;

card (stop I) = (card I) + 1 by SCMPDS_4:45, LL;
then n < (card I) + 1 by A3, SCMPDS_4:1;
then n <= card I by INT_1:20;
then n < card I by A6, XXREAL_0:1;
hence IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) in dom I by SCMPDS_4:1; :: thesis: verum