theorem :: SCMFSA8C:99

for aa, bb being Int-Location
for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not if=0 (bb,(I ';' (goto 0))) destroys aa