environ
vocabularies HIDDEN, RELAT_1, XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, NET_1, STRUCT_0, PETRI;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, PARTIT_2, STRUCT_0, PETRI;
definitions XBOOLE_0;
theorems TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1;
schemes XBOOLE_0, SUBSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1;
constructors HIDDEN, TARSKI, SUBSET_1, RELAT_1, STRUCT_0, PETRI, PARTIT_2;
requirements HIDDEN, SUBSET, BOOLE;
equalities ;
expansions ;
Lm1:
PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) is Petri
:: N = (carrier, carrier', Flow)
:: with carrier and carrier' being disjoint sets and
:: Flow c= (carrier' x carrier) U (carrier x carrier')
:: It is allowed that both sets carrier and carrier' are empty.
:: A Petri net is here described as a predicate defined in the set
:: (on the mode) PT_net_Str.