:: deftheorem defines is_closed_on SCMPDS_6:def 2 :
for I being Program of
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds
( I is_closed_on s,P iff for k being Nat holds IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) );