theorem :: SCMFSA8C:51

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