:: deftheorem Def2 defines keeping_0 SCMFSA6B:def 4 :
for I being Program of holds
( I is keeping_0 iff for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P holds
for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) );