theorem :: SCMFSA7B:13

for a, b being Int-Location
for l being Nat holds not b >0_goto l destroys a ;