theorem Th23: :: AMI_6:23

for i1, k being Nat holds IncAddr ((SCM-goto i1),k) = SCM-goto (i1 + k)