:: deftheorem Def5 defines relocable1 AMISTD_5:def 5 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N holds
( S is relocable1 iff for k being Nat
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty b₄ -autonomic FinPartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & Reloc (q,k) c= P2 holds
for i being Nat holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) );