let s be State of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being Program of SCMPDS
for i being Element of NAT st stop I c= P & Start-At (0,SCMPDS) c= s & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds
IC (Comput (P,s,i)) in dom I
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I being Program of SCMPDS
for i being Element of NAT st stop I c= P & Start-At (0,SCMPDS) c= s & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds
IC (Comput (P,s,i)) in dom I
let I be Program of SCMPDS; :: thesis: for i being Element of NAT st stop I c= P & Start-At (0,SCMPDS) c= s & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds
IC (Comput (P,s,i)) in dom I
let i be Element of NAT ; :: thesis: ( stop I c= P & Start-At (0,SCMPDS) c= s & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) implies IC (Comput (P,s,i)) in dom I )
set sI = stop I;
set Ci = Comput (P,s,i);
set Lc = IC (Comput (P,s,i));
assume that
A1: stop I c= P and
B1: Start-At (0,SCMPDS) c= s and
A2: I is_closed_on s,P and
A3: I is_halting_on s,P and
A4: i < LifeSpan (P,s) ; :: thesis: IC (Comput (P,s,i)) in dom I
A5: P +* (stop I) = P by A1, FUNCT_4:104;
A6: s = Initialize s by FUNCT_4:104, B1;
then A7: IC (Comput (P,s,i)) in dom (stop I) by A2, SCMPDS_6:def 2, A5;
A8: stop I c= P by A1;
A9: P halts_on s by A3, A6, SCMPDS_6:def 3, A5;

now

assume A10: (stop I) . (IC (Comput (P,s,i))) = halt SCMPDS ; :: thesis: contradiction
A12: P /. (IC (Comput (P,s,i))) = P . (IC (Comput (P,s,i))) by PBOOLE:158;
CurInstr (P,(Comput (P,s,i))) = P . (IC (Comput (P,s,i))) by A12
.= halt SCMPDS by A7, A8, A10, GRFUNC_1:8 ;
hence contradiction by A4, A9, EXTPRO_1:def 14; :: thesis: verum

end;

hence IC (Comput (P,s,i)) in dom I by A7, SCMPDS_5:3; :: thesis: verum