theorem Th43: :: SCMFSA10:43

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