for s being State of SCM+FSA
for I being parahalting Program of 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