for P being Instruction-Sequence of SCMPDS
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