for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function

for p being b_{1} -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

for p being b

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