theorem Th11: :: SCMFSA_9:31

for i being Instruction of SCM+FSA st not i destroys intloc 0 holds
Macro i is good