for I being Program of holds
( I is parahalting iff for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P )