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_{1} being set holds (IC (Exec ((IncAddr (I,j)),b_{1}))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b_{1},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

assume A1: I is relocable ; :: thesis: I is IC-relocable

let j, k be Nat; :: according to AMISTD_2:def 3 :: thesis: for b

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