:: deftheorem Def1 defines InitHalting SCM_HALT:def 1 :
for I being Program of SCM+FSA holds
( I is InitHalting iff for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
for P being Instruction-Sequence of SCM+FSA st I c= P holds
P halts_on s );