The abstract of the Mizar article:

Definitions of Petri Net. Part III

by

Waldemar Korczynski

Received January 31, 1992

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;
 redefine func e_adjac 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):];