:: deftheorem Def12 defines Autonomy EXTPRO_1:def 12 :
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b₂ -valued non halt-free Function
for b₄ being FinPartState of S holds
( b₄ is Autonomy of P iff ( b₄ is P -autonomic & b₄ is P -halted ) );