:: deftheorem defines destroys SCMFSA7B:def 4 :
for I being NAT -defined the InstructionsF of SCM+FSA -valued Function
for a being Int-Location holds
( I destroys a iff ex i being Instruction of SCM+FSA st
( i in rng I & i destroys a ) );