:: deftheorem defines is_halting_onInit SCM_HALT:def 3 :
for I being Program of SCM+FSA
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds
( I is_halting_onInit s,p iff p +* I halts_on Initialized s );