for I being MacroInstruction of SCM+FSA
for a, b being Int-Location st not I destroys b & a <> b holds
not Times (a,I) destroys b