theorem :: SCMFSA8C:97

for aa being Int-Location
for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not I ';' (goto 0) destroys aa by Lm2;