:: deftheorem Def4 defines CurIns-recognized AMISTD_5:def 4 :
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 CurIns-recognized iff 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 s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds IC (Comput (P,s,i)) in dom q );