let I be Instruction of S; :: thesis: ( I is relocable implies I is IC-relocable )
assume A1: I is relocable ; :: thesis: I is IC-relocable
let j, k be Nat; :: according to AMISTD_2:def 3 :: thesis: for b₁ being set holds (IC (Exec ((IncAddr (I,j)),b₁))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b₁,k))))
let s be State of S; :: thesis: (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 ; :: thesis: verum