theorem :: SCMFSA8C:98

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 by Lm3;