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