:: deftheorem Def1 defines decision_free_like PETRI_DF:def 7 :
for IT being Petri_net holds
( IT is decision_free_like iff for s being place of IT holds
( ex t being transition of IT st [t,s] in the T-S_Arcs of IT & ( for t1, t2 being transition of IT st [t1,s] in the T-S_Arcs of IT & [t2,s] in the T-S_Arcs of IT holds
t1 = t2 ) & ex t being transition of IT st [s,t] in the S-T_Arcs of IT & ( for t1, t2 being transition of IT st [s,t1] in the S-T_Arcs of IT & [s,t2] in the S-T_Arcs of IT holds
t1 = t2 ) ) );