theorem :: SCMFSA8A:44

for i, j being Nat holds IncAddr ((Goto i),j) = <%(goto (i + j))%>