:: deftheorem defines good SCMFSA7B:def 5 :
for I being NAT -defined the InstructionsF of SCM+FSA -valued Function holds
( I is good iff not I destroys intloc 0 );