for s being 0 -started State of SCM+FSA
for I being parahalting Program of
for P being Instruction-Sequence of SCM+FSA st I c= P holds
P halts_on s by AMISTD_1:def 11;