theorem Th7: :: AMISTD_2:7

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N
for I being IC-relocable Instruction of S
for k being Nat
for s being State of S holds (IC (Exec (I,s))) + k = IC (Exec ((IncAddr (I,k)),(IncIC (s,k))))