for R being Ring
for a being Data-Location of R
for i1, k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)