theorem Th1: :: SCMFSA_4:1

for k, loc being Nat holds IncAddr ((goto loc),k) = goto (loc + k) by SCMFSA10:41;