theorem Th9: :: AMISTD_5:9

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
for k being Nat
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being b₄ -autonomic FinPartState of S st IC in dom p holds
for s being State of S st IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)