let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being Program of
for i being Nat st stop I c= P & 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 s be 0 -started State of SCMPDS; :: thesis: for I being Program of
for i being Nat st stop I c= P & 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 ; :: thesis: for i being Nat st stop I c= P & 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 Nat; :: thesis: ( stop I c= P & 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
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: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;
A6: P +* (stop I) = P by A1, FUNCT_4:98;
A7: s = Initialize s by A5, FUNCT_4:98;
then A8: IC (Comput (P,s,i)) in dom (stop I) by A2, A6, SCMPDS_6:def 2;
A9: P halts_on s by A3, A7, A6, SCMPDS_6:def 3;

now :: thesis: not (stop I) . (IC (Comput (P,s,i))) = halt SCMPDS

assume A10: (stop I) . (IC (Comput (P,s,i))) = halt SCMPDS ; :: thesis: contradiction
CurInstr (P,(Comput (P,s,i))) = P . (IC (Comput (P,s,i))) by PBOOLE:143
.= halt SCMPDS by A8, A1, A10, GRFUNC_1:2 ;
hence contradiction by A4, A9, EXTPRO_1:def 15; :: thesis: verum

end;

hence IC (Comput (P,s,i)) in dom I by A8, COMPOS_1:51; :: thesis: verum