:: deftheorem defines PetriNet PETRI_DF:def 2 :
PetriNet = PT_net_Str(# {0},{1},([#] ({0},{1})),([#] ({1},{0})) #);