let I be Instruction of S; ( I is relocable implies I is IC-relocable )
assume A1:
I is relocable
; I is IC-relocable
let j, k be Nat; AMISTD_2:def 3 for b1 being set holds (IC (Exec ((IncAddr (I,j)),b1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k))))
let s be State of S; (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))))
reconsider kk = k as Nat ;
thus (IC (Exec ((IncAddr (I,j)),s))) + k =
IC (IncIC ((Exec ((IncAddr (I,j)),s)),kk))
by MEMSTR_0:53
.=
IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))))
by A1
; verum