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 natural number ; :: according to AMISTD_2:def 18 :: 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))))
X2: IC in dom (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) by COMPOS_1:9;
reconsider kk = k as Element of NAT by ORDINAL1:def 13;
X1: IC in dom (IncIC ((Exec ((IncAddr (I,j)),s)),kk)) by COMPOS_1:9;
thus (IC (Exec ((IncAddr (I,j)),s))) + k = IC (IncIC ((Exec ((IncAddr (I,j)),s)),kk)) by COMPOS_1:54
.= IC (NPP (IncIC ((Exec ((IncAddr (I,j)),s)),kk))) by X1, COMPOS_1:72
.= IC (NPP (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))))) by A1, Def1
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) by X2, COMPOS_1:72
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) ; :: thesis: verum