:: deftheorem defines misses PETRI_2:def 12 :
for CPNT1, CPNT2 being Colored_Petri_net holds
( CPNT1 misses CPNT2 iff ( the carrier of CPNT1 /\ the carrier of CPNT2 = {} & the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} ) );