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 (Computation (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 (Computation (s +* (Initialized (stop I))),k) in dom I
let k be Element of NAT ; :: thesis: ( k < LifeSpan (s +* (Initialized (stop I))) implies IC (Computation (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)));
assume A1: k < LifeSpan (s +* (Initialized (stop I))) ; :: thesis: IC (Computation (s +* (Initialized (stop I))),k) in dom I
set Sk = Computation (s +* (Initialized (stop I))),k;
set Ik = IC (Computation (s +* (Initialized (stop I))),k);
A2: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
then A3: IC (Computation (s +* (Initialized (stop I))),k) in dom (stop I) by SCMPDS_4:def 9;
A4: s +* (Initialized (stop I)) is halting by FUNCT_4:26, SCMPDS_4:63;
stop I c= Initialized (stop I) by SCMPDS_4:9;
then A5: stop I c= s +* (Initialized (stop I)) by A2, XBOOLE_1:1;
reconsider n = IC (Computation (s +* (Initialized (stop I))),k) as Element of NAT by ORDINAL1:def 13;
card (stop I) = (card I) + 1 by SCMPDS_4:45, SCMPDS_4:74;
then n < (card I) + 1 by A3, SCMPDS_4:1;
then A7: n <= card I by INT_1:20;

now

assume A8: n = card I ; :: thesis: contradiction
CurInstr (Computation (s +* (Initialized (stop I))),k) = (s +* (Initialized (stop I))) . (IC (Computation (s +* (Initialized (stop I))),k)) by AMI_1:54
.= (stop I) . (inspos (0 + n)) by A3, A5, GRFUNC_1:8
.= halt SCMPDS by A8, SCMPDS_4:38, SCMPDS_4:73 ;
hence contradiction by A1, A4, AMI_1:def 46; :: thesis: verum

end;

then n < card I by A7, XXREAL_0:1;
hence IC (Computation (s +* (Initialized (stop I))),k) in dom I by SCMPDS_4:1; :: thesis: verum