theorem Th1: :: RELOC:1
for k, loc being Nat holds IncAddr ((SCM-goto loc),k) = SCM-goto (loc + k)