:: deftheorem Def2 defines keepInt0_1 SCM_HALT:def 2 :
for I being Program of SCM+FSA holds
( I is keepInt0_1 iff for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
for p being Instruction-Sequence of SCM+FSA st I c= p holds
for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1 );