theorem Th2: :: RELOC:2

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