:: deftheorem defines destroys SCMFSA7B:def 3 :
for i being Instruction of SCM+FSA
for a being Int-Location holds
( i destroys a iff not for b being Int-Location
for f being FinSeq-Location holds
( a := b <> i & AddTo (a,b) <> i & SubFrom (a,b) <> i & MultBy (a,b) <> i & Divide (a,b) <> i & Divide (b,a) <> i & a := (f,b) <> i & a :=len f <> i ) );