thus
STC N is IC-relocable
:: thesis: verum

proof

let I be Instruction of (STC N); :: according to AMISTD_2:def 4 :: thesis: I is IC-relocable

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

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

set s2 = IncIC (s1,k);

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

then A1: IC (IncIC (s1,k)) = ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCT_4:13

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

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

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

set s2 = IncIC (s1,k);

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

then A1: IC (IncIC (s1,k)) = ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCT_4:13

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

per cases
( InsCode I = 1 or InsCode I = 0 )
by AMISTD_1:6;

end;

suppose A2:
InsCode I = 1
; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))

then A3:
InsCode (IncAddr (I,k)) = 1
by COMPOS_0:def 9;

A4: IncAddr (I,j) = I by COMPOS_0:4;

IC (Exec (I,s1)) = (IC s1) + 1 by A2, AMISTD_1:9;

hence (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (IncIC (s1,k))) + 1 by A1, A4

.= IC (Exec ((IncAddr ((IncAddr (I,j)),k)),(IncIC (s1,k)))) by A4, A3, AMISTD_1:9

.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by COMPOS_0:7 ;

:: thesis: verum

end;A4: IncAddr (I,j) = I by COMPOS_0:4;

IC (Exec (I,s1)) = (IC s1) + 1 by A2, AMISTD_1:9;

hence (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (IncIC (s1,k))) + 1 by A1, A4

.= IC (Exec ((IncAddr ((IncAddr (I,j)),k)),(IncIC (s1,k)))) by A4, A3, AMISTD_1:9

.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by COMPOS_0:7 ;

:: thesis: verum

suppose
InsCode I = 0
; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))

then A5:
I is halting
by AMISTD_1:4;

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

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

:: thesis: verum

end;hence (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC s1) + k by EXTPRO_1:def 3

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

:: thesis: verum