theorem Th3: :: RELOC:3

for k, loc being Nat
for a being Data-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)