Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Definitions of Petri Net. Part III

by
Waldemar Korczynski

MML identifier: S_SIEC
[ Mizar article, MML identifier index ]

```environ

vocabulary E_SIEC, BOOLE, RELAT_1, S_SIEC;
notation TARSKI, XBOOLE_0, ZFMISC_1, STRUCT_0, RELAT_1, E_SIEC;
constructors E_SIEC;
clusters RELAT_1, ZFMISC_1;

begin

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;
synonym s_prox N;
end;

reserve N for e_net;

canceled 40;

theorem :: S_SIEC:41
((the entrance of N) \ diagonal(the carrier of N))~ c=
[:e_Places(N),e_Transitions(N):] &
((the escape of N) \ diagonal(the carrier of N))~ c=
[:e_Places(N),e_Transitions(N):];

definition let N be G_Net;
canceled 27;

func s_pre(N) -> Relation equals
:: S_SIEC:def 28
((the escape of N) \ diagonal(the carrier of N))~;
func s_post(N) -> Relation equals
:: S_SIEC:def 29
((the entrance of N) \ diagonal(the carrier of N))~;
end;

canceled;

theorem :: S_SIEC:43
s_post(N) c= [:s_transitions(N),s_places(N):] &
s_pre(N) c= [:s_transitions(N),s_places(N):];
```