for i1 being Nat
for a being Int-Location holds JUMP (a >0_goto i1) = {i1}