:: deftheorem defines -autonomic EXTPRO_1:def 10 :
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for p being NAT -defined the InstructionsF of b₂ -valued Function
for IT being PartState of S holds
( IT is p -autonomic iff for P, Q being Instruction-Sequence of S st p c= P & p c= Q holds
for s1, s2 being State of S st IT c= s1 & IT c= s2 holds
for i being Nat holds (Comput (P,s1,i)) | (dom IT) = (Comput (Q,s2,i)) | (dom IT) );