theorem Th13: :: AMISTD_5:13

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 b₃ -halted FinPartState of S st IC in dom p holds
for k being Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))