for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N
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 k being Nat st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )