let I be Instruction of S; :: thesis: ( I is sequential implies I is IC-relocable )
assume A1: I is sequential ; :: thesis: I is IC-relocable
let j, k be natural number ; :: 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);
dom ((IC ) .--> ((IC s1) + k)) = {(IC )} by FUNCOP_1:13;
then IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A2: IC (IncIC (s1,k)) = ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCT_4:13
.= (IC s1) + k by FUNCOP_1:72 ;
A3: IC (Exec (I,(IncIC (s1,k)))) = succ (IC (IncIC (s1,k))) by A1, AMISTD_1:def 8
.= ((IC s1) + 1) + k by A2 ;
A4: IncAddr (I,j) = I by A1, COMPOS_1:11;
IC (Exec (I,s1)) = succ (IC s1) by A1, AMISTD_1:def 8
.= (IC s1) + 1 ;
hence (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr ((IncAddr (I,j)),k)),(IncIC (s1,k)))) by A1, A3, A4, COMPOS_1:11
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by COMPOS_1:15 ;
:: thesis: verum