for i1 being Nat
for a being Int-Location holds JumpPart (a =0_goto i1) = <*i1*>