for I being Program of holds
( I is paraclosed iff for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds I is_closed_on s,P )