:: deftheorem defines is_halting_on SCMPDS_6:def 3 :
for I being Program of
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds
( I is_halting_on s,P iff P +* (stop I) halts_on Initialize s );