theorem Th42: :: SCMFSA10:42

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