for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function
for p being b₁ -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 Nat; :: according to AMISTD_5:def 1 :: thesis: for s being State of (STC N) holds Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (I,j)),s)),k)
let s be State of (STC N); :: thesis: Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (I,j)),s)),k)
thus Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = Exec (I,(IncIC (s,k))) by COMPOS_0:4
.= IncIC ((Exec (I,s)),k) by Th2
.= IncIC ((Exec ((IncAddr (I,j)),s)),k) by COMPOS_0:4 ; :: thesis: verum