for k, loc being Nat
for a being Int-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)