for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( I is_halting_onInit s,p iff I is_halting_on Initialized s,p ) by MEMSTR_0:44;