theorem Th6: :: AMISTD_5:6

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized 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 holds IC in dom p