for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of st ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st DataPart t = DataPart s holds
I is_halting_on t,Q ) holds
I is_closed_on s,P