theorem Th16: :: SF_MASTR:16

for a being Int-Location
for l being Nat
for i being Instruction of SCM+FSA st ( i = a =0_goto l or i = a >0_goto l ) holds
UsedIntLoc i = {a}