Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### Definitions of Petri Net. Part II

**by****Waldemar Korczynski**- Received January 31, 1992
- MML identifier: E_SIEC

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, BOOLE, SYSREL, E_SIEC, FUNCT_1, S_SIEC; notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, SYSREL, STRUCT_0; constructors SYSREL, STRUCT_0, XBOOLE_0; clusters RELAT_1, SYSREL, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin reserve x,y,z,X,Y for set; :: D E F I N I T I O N S definition struct (1-sorted) G_Net (# carrier -> set, entrance, escape -> Relation #); end; definition let N be 1-sorted; func echaos N -> set equals :: E_SIEC:def 1 (the carrier of N) \/ {the carrier of N}; end; definition let IT be G_Net; attr IT is GG means :: E_SIEC:def 2 the entrance of IT c= [:the carrier of IT,the carrier of IT:] & the escape of IT c= [:the carrier of IT,the carrier of IT:] & (the entrance of IT) * (the entrance of IT) = the entrance of IT & (the entrance of IT) * (the escape of IT) = the entrance of IT & (the escape of IT) * (the escape of IT) = the escape of IT & (the escape of IT) * (the entrance of IT) = the escape of IT; end; definition cluster GG G_Net; end; definition mode gg_net is GG G_Net; end; definition let IT be G_Net; attr IT is EE means :: E_SIEC:def 3 (the entrance of IT) * ((the entrance of IT) \ id(the carrier of IT)) = {} & (the escape of IT) * ((the escape of IT) \ id(the carrier of IT)) = {}; end; definition cluster EE G_Net; end; definition cluster strict GG EE G_Net; end; definition mode e_net is EE GG G_Net; end; reserve N for e_net; theorem :: E_SIEC:1 for R, S being Relation holds G_Net (# X, R, S #) is e_net iff R c= [:X,X:] & S c= [:X,X:] & R * R = R & R * S = R & S * S = S & S * R = S & R * (R \ id(X)) = {} & S * (S \ id(X)) = {}; theorem :: E_SIEC:2 G_Net (# X, {}, {} #) is e_net; theorem :: E_SIEC:3 G_Net (# X, id X, id X #) is e_net; theorem :: E_SIEC:4 G_Net (# {}, {}, {} #) is e_net; canceled 3; theorem :: E_SIEC:8 G_Net (# X, id(X \ Y), id(X \ Y) #) is e_net; theorem :: E_SIEC:9 echaos N <> {}; definition func empty_e_net -> strict e_net equals :: E_SIEC:def 4 G_Net (# {}, {}, {} #); end; definition let X; func Tempty_e_net X -> strict e_net equals :: E_SIEC:def 5 G_Net (# X, id X, id X #); func Pempty_e_net(X) -> strict e_net equals :: E_SIEC:def 6 G_Net (# X, {}, {} #); end; canceled; theorem :: E_SIEC:11 the carrier of Tempty_e_net(X) = X & the entrance of Tempty_e_net(X) = id X & the escape of Tempty_e_net(X) = id X; theorem :: E_SIEC:12 the carrier of Pempty_e_net(X) = X & the entrance of Pempty_e_net(X) = {} & the escape of Pempty_e_net(X) = {}; definition let x; func Psingle_e_net(x) -> strict e_net equals :: E_SIEC:def 7 G_Net (#{x}, id{x}, id{x}#); func Tsingle_e_net(x) -> strict e_net equals :: E_SIEC:def 8 G_Net (# {x}, {}, {} #); end; theorem :: E_SIEC:13 the carrier of Psingle_e_net(x) = {x} & the entrance of Psingle_e_net(x) = id{x} & the escape of Psingle_e_net(x) = id{x}; theorem :: E_SIEC:14 the carrier of Tsingle_e_net(x) = {x} & the entrance of Tsingle_e_net(x) = {} & the escape of Tsingle_e_net(x) = {}; theorem :: E_SIEC:15 G_Net (# X \/ Y, id X, id X #) is e_net; definition let X,Y; func PTempty_e_net(X,Y) -> strict e_net equals :: E_SIEC:def 9 G_Net (#X \/ Y, id(X), id(X)#); end; theorem :: E_SIEC:16 (the entrance of N) \ id(dom(the entrance of N)) = (the entrance of N) \ id(the carrier of N) & (the escape of N) \ id(dom(the escape of N)) = (the escape of N) \ id(the carrier of N) & (the entrance of N) \ id(rng(the entrance of N)) = (the entrance of N) \ id(the carrier of N) & (the escape of N) \ id(rng(the escape of N)) = (the escape of N) \ id(the carrier of N); theorem :: E_SIEC:17 CL(the entrance of N) = CL(the escape of N); theorem :: E_SIEC:18 rng (the entrance of N) = rng (CL(the entrance of N)) & rng (the entrance of N) = dom (CL(the entrance of N)) & rng (the escape of N) = rng (CL(the escape of N)) & rng (the escape of N) = dom (CL(the escape of N)) & rng (the entrance of N) = rng (the escape of N); theorem :: E_SIEC:19 dom (the entrance of N) c= the carrier of N & rng (the entrance of N) c= the carrier of N & dom (the escape of N) c= the carrier of N & rng (the escape of N) c= the carrier of N; theorem :: E_SIEC:20 (the entrance of N) * ((the escape of N) \ id(the carrier of N)) = {} & (the escape of N) * ((the entrance of N) \ id(the carrier of N)) = {}; theorem :: E_SIEC:21 ((the entrance of N) \ id(the carrier of N)) * ((the entrance of N) \ id(the carrier of N)) = {} & ((the escape of N) \ id(the carrier of N)) * ((the escape of N) \ id(the carrier of N)) = {} & ((the entrance of N) \ id(the carrier of N)) * ((the escape of N) \ id(the carrier of N)) = {} & ((the escape of N) \ id(the carrier of N)) * ((the entrance of N) \ id(the carrier of N)) = {}; definition let N; func e_Places(N) -> set equals :: E_SIEC:def 10 rng (the entrance of N); end; definition let N; func e_Transitions(N) -> set equals :: E_SIEC:def 11 (the carrier of N) \ e_Places(N); end; theorem :: E_SIEC:22 e_Places(N) misses e_Transitions(N); theorem :: E_SIEC:23 ([x,y] in the entrance of N or [x,y] in the escape of N) & x <> y implies x in e_Transitions(N) & y in e_Places(N); theorem :: E_SIEC:24 (the entrance of N) \ id(the carrier of N) c= [:e_Transitions(N),e_Places(N):] & (the escape of N) \ id(the carrier of N) c= [:e_Transitions(N),e_Places(N):]; definition let N; func e_Flow N -> Relation equals :: E_SIEC:def 12 ((the entrance of N)~ \/ (the escape of N)) \ id(the carrier of N); end; theorem :: E_SIEC:25 e_Flow N c= [:e_Places(N) , e_Transitions(N):] \/ [:e_Transitions(N) , e_Places(N):]; definition let N; redefine func e_Places(N); synonym e_places(N); redefine func e_Transitions(N); synonym e_transitions(N); end; definition let N; canceled 2; func e_pre(N) -> Relation equals :: E_SIEC:def 15 (the entrance of N) \ id(the carrier of N); func e_post(N) -> Relation equals :: E_SIEC:def 16 (the escape of N) \ id(the carrier of N); end; canceled 2; theorem :: E_SIEC:28 e_pre(N) c= [:e_transitions(N),e_places(N):] & e_post(N) c= [:e_transitions(N),e_places(N):]; definition let N; func e_shore(N) -> set equals :: E_SIEC:def 17 the carrier of N; func e_prox(N) -> Relation equals :: E_SIEC:def 18 ((the entrance of N) \/ (the escape of N))~; func e_flow(N) -> Relation equals :: E_SIEC:def 19 ((the entrance of N)~ \/ (the escape of N)) \/ id(the carrier of N); end; theorem :: E_SIEC:29 e_prox(N) c= [:e_shore(N),e_shore(N):] & e_flow(N) c= [:e_shore(N),e_shore(N):]; theorem :: E_SIEC:30 (e_prox(N)) * (e_prox(N)) = e_prox(N) & (e_prox(N) \ id(e_shore(N))) * e_prox(N) = {} & (e_prox(N) \/ (e_prox(N))~) \/ id(e_shore(N)) = e_flow(N) \/ (e_flow(N))~; theorem :: E_SIEC:31 id((the carrier of N) \ rng(the escape of N)) * ((the escape of N) \ id(the carrier of N)) = ((the escape of N) \ id(the carrier of N)) & id((the carrier of N) \ rng(the entrance of N)) * ((the entrance of N) \ id(the carrier of N)) = ((the entrance of N) \ id(the carrier of N)); theorem :: E_SIEC:32 ((the escape of N) \ id(the carrier of N)) * ((the escape of N) \ id(the carrier of N)) = {} & ((the entrance of N) \ id(the carrier of N)) * ((the entrance of N) \ id(the carrier of N)) = {} & ((the escape of N) \ id(the carrier of N)) * ((the entrance of N) \ id(the carrier of N)) = {} & ((the entrance of N) \ id(the carrier of N)) * ((the escape of N) \ id(the carrier of N)) = {}; theorem :: E_SIEC:33 ((the escape of N) \ id(the carrier of N))~ * ((the escape of N) \ id(the carrier of N))~ = {} & ((the entrance of N) \ id(the carrier of N))~ * ((the entrance of N) \ id(the carrier of N))~ = {}; theorem :: E_SIEC:34 ((the escape of N) \ id(the carrier of N))~ * id((the carrier of N) \ rng(the escape of N))~ = ((the escape of N) \ id(the carrier of N))~ & ((the entrance of N) \ id(the carrier of N))~ * id((the carrier of N) \ rng(the entrance of N))~ = ((the entrance of N) \ id(the carrier of N))~; theorem :: E_SIEC:35 ((the escape of N) \ id(the carrier of N)) * (id((the carrier of N) \ rng(the escape of N))) = {} & ((the entrance of N) \ id(the carrier of N)) * (id((the carrier of N) \ rng(the entrance of N))) = {}; theorem :: E_SIEC:36 id((the carrier of N) \ rng(the escape of N)) * ((the escape of N) \ id(the carrier of N))~ = {} & id((the carrier of N) \ rng(the entrance of N)) * ((the entrance of N) \ id(the carrier of N))~ = {}; definition let N; redefine func e_shore(N); synonym e_support(N); end; definition let N; canceled; func e_entrance(N) -> Relation equals :: E_SIEC:def 21 (((the escape of N) \ id(the carrier of N))~) \/ id((the carrier of N) \ rng(the escape of N)); func e_escape(N) -> Relation equals :: E_SIEC:def 22 (((the entrance of N) \ id(the carrier of N))~) \/ id((the carrier of N) \ rng(the entrance of N)); end; theorem :: E_SIEC:37 e_entrance(N) * e_entrance(N) = e_entrance(N) & e_entrance(N) * e_escape(N) = e_entrance(N) & e_escape(N) * e_entrance(N) = e_escape(N) & e_escape(N) * e_escape(N) = e_escape(N); theorem :: E_SIEC:38 e_entrance(N) * (e_entrance(N) \ id(e_support(N))) = {} & e_escape(N) * (e_escape(N) \ id(e_support(N))) = {}; definition let N; redefine func e_shore(N); synonym e_stanchion(N); end; definition let N; canceled; func e_adjac(N) -> Relation equals :: E_SIEC:def 24 (((the entrance of N) \/ (the escape of N)) \ id(the carrier of N)) \/ id((the carrier of N) \ rng(the entrance of N)); redefine func e_flow(N); synonym e_circulation(N); end; theorem :: E_SIEC:39 e_adjac(N) c= [:e_stanchion(N),e_stanchion(N):] & e_circulation(N) c= [:e_stanchion(N),e_stanchion(N):]; theorem :: E_SIEC:40 (e_adjac(N)) * (e_adjac(N)) = e_adjac(N) & (e_adjac(N) \ id(e_stanchion(N))) * e_adjac(N) = {} & (e_adjac(N) \/ (e_adjac(N))~) \/ id(e_stanchion(N)) = e_circulation(N) \/ (e_circulation(N))~; definition let N be e_net; redefine func e_Places N; synonym s_transitions N; redefine func e_Transitions N; synonym s_places N; redefine func e_shore N; synonym s_carrier N; redefine func e_entrance N; synonym s_enter N; redefine func e_escape N; synonym s_exit N; redefine func e_adjac N; synonym s_prox N; end; reserve N for e_net; theorem :: E_SIEC:41 ((the entrance of N) \ id(the carrier of N))~ c= [:e_Places(N),e_Transitions(N):] & ((the escape of N) \ id(the carrier of N))~ c= [:e_Places(N),e_Transitions(N):]; definition let N be G_Net; func s_pre(N) -> Relation equals :: E_SIEC:def 25 ((the escape of N) \ id(the carrier of N))~; func s_post(N) -> Relation equals :: E_SIEC:def 26 ((the entrance of N) \ id(the carrier of N))~; end; theorem :: E_SIEC:42 s_post(N) c= [:s_transitions(N),s_places(N):] & s_pre(N) c= [:s_transitions(N),s_places(N):];

Back to top