:: deftheorem defines TrivialPetriNet PETRI:def 3 :
TrivialPetriNet = PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #);