for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed Program of SCM+FSA
for l being Nat holds
( I is_halting_on s,P iff I is_halting_on s +* (Start-At (l,SCM+FSA)),P +* I )