:: deftheorem Defcntfir defines connecting-firing-rule PETRI_3:def 5 :
for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for O being connecting-mapping of CPNT
for b₄ being ManySortedSet of XorDelta I holds
( b₄ is connecting-firing-rule of O iff for i, j being Element of I st i <> j holds
ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = b₄ . [i,j] & Oij = O . [i,j] & dom qij = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) ) );