let I be Instruction of S; :: thesis: ( I is halting implies I is IC-relocable )

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

let j, k be Nat; :: according to AMISTD_2:def 3 :: thesis: for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))))

let s1 be State of S; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))

set s2 = IncIC (s1,k);

A2: IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def 1;

thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC s1) + k by A1, EXTPRO_1:def 3

.= ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCOP_1:72

.= IC (IncIC (s1,k)) by A2, FUNCT_4:13

.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A1, EXTPRO_1:def 3 ; :: thesis: verum

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

let j, k be Nat; :: according to AMISTD_2:def 3 :: thesis: for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))))

let s1 be State of S; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))

set s2 = IncIC (s1,k);

A2: IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def 1;

thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC s1) + k by A1, EXTPRO_1:def 3

.= ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCOP_1:72

.= IC (IncIC (s1,k)) by A2, FUNCT_4:13

.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A1, EXTPRO_1:def 3 ; :: thesis: verum