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