:: deftheorem defines is_halting_on SCMFSA7B:def 6 :
for I being Program of
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( I is_halting_on s,P iff P +* I halts_on Initialize s );