for p being autonomic FinPartState of (STC N) st DataPart p <> {} holds
IC in dom p ;
hence STC N is IC-recognized by Th3; :: thesis: STC N is relocable
let I be Instruction of (STC N); :: according to AMISTD_5:def 2 :: thesis: I is relocable
let j, k be natural number ; :: according to AMISTD_5:def 1 :: thesis: for s being State of (STC N) holds NPP (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (I,j)),s)),k))
let s be State of (STC N); :: thesis: NPP (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (I,j)),s)),k))
thus NPP (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) = NPP (Exec (I,(IncIC (s,k)))) by COMPOS_1:92
.= NPP (IncIC ((Exec (I,s)),k)) by Th2
.= NPP (IncIC ((Exec ((IncAddr (I,j)),s)),k)) by COMPOS_1:92 ; :: thesis: verum