theorem Th24: :: AMI_6:24

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