(bi v ... V b;"). If e· = 0, then aCe) is the formula I (b) 1\ ... 1\ bn ). If ·e = 0, then a (e) is the formula bi V ... V b;". (c) Lemma. Let L be a finite C/ E-system and let e aCe) is valid in c iff e is not c-enabled. Proof c(a(e» = 1 ~ ::3b E·e with ::3b E ·e with b ¢ cor ::3b' E e· with b' E EE. Then for each c E CE , c(b) = 0 E or ::3b' E e· with C(b') = 1 ~ c ~ e is not c-enabled.
0 This lemma establishes a unique correspondence between elementary processes and arcs, and we therefore define: 42 Processes of Condition IEvent-Systems {I,'} y~ )"S} p= {o c} U,4} /' \o\. ~< ')'/j\
A) Definition. A net K = (SK, T K; FK) is called an occurrence net if and only if (i) Ya, bE K: a (Ft) b <=> I (b Ft a) (K is cycle-free), (ii) Y sE SK: I·s I:S:. 1/\ I s·1 :S:. 1 (S-elements are unbranched). Figure 34 shows examples of occurrence nets. 36 Processes of Condition IE vent-Systems (b) Proposition. Let K be an occurrence net. < b, for all a, b E K, is a partial order on K. Hence, all notions concerning partially ordered sets, such as lines, cuts, boundedness and K-density are particularly defined for occurrence nets.