:: deftheorem defines IC-recognized AMISTD_5:def 3 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds
( S is IC-recognized iff for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being b₃ -autonomic FinPartState of S st not p is empty holds
IC in dom p );