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

### Definitions of Petri Net. Part II

by
Waldemar Korczynski

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;

:: 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_circulation(N) c= [:e_stanchion(N),e_stanchion(N):];

theorem :: E_SIEC:40
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;
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):];
```