theorem Th2: :: SCMFSA_4:2

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