for i being Instruction of SCM+FSA
for a being Int-Location
for n being Element of NAT st not i destroys a holds
not IncAddr (i,n) destroys a