for I being Program of SCM+FSA st ( for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,P ) holds
Initialize ((intloc 0) .--> 1) is I -halted