for aa, bb being Int-Location
for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not while>0 (bb,I) destroys aa