theorem Th39: :: SCMFSA8C:48

for i being Instruction of SCM+FSA
for a being Int-Location st not i destroys a holds
not Macro i destroys a