:: deftheorem Def6 defines paraclosed SCMPDS_4:def 6 :
for I being Program of holds
( I is paraclosed iff for s being 0 -started State of SCMPDS
for n being Nat
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
IC (Comput (P,s,n)) in dom (stop I) );