for I being Program of SCM+FSA holds
( I is InitHalting iff for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,p )