The Mizar article:

Definitions of Petri Net. Part III

by

Waldemar Korczynski

Received January 31, 1992

Copyright (c) 1992 Association of Mizar Users

MML identifier: S_SIEC

[ 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;
 theorems SYSREL, E_SIEC;

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
Th41:((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):]
proof
   (the entrance of N) \ diagonal(the carrier of N) c=
                    [:e_Transitions(N),e_Places(N):] &
        (the escape of N) \ diagonal(the carrier of N) c=
                             [:e_Transitions(N),e_Places(N):] by E_SIEC:24;
 hence thesis by SYSREL:16;
end;

 definition let N be G_Net;
 canceled 27;

  func s_pre(N) -> Relation equals
  :Def28: ((the escape of N) \ diagonal(the carrier of N))~;
  coherence;
  func s_post(N) -> Relation equals
  :Def29: ((the entrance of N) \ diagonal(the carrier of N))~;
  coherence;
 end;

canceled;

theorem
   s_post(N) c= [:s_transitions(N),s_places(N):] &
         s_pre(N) c= [:s_transitions(N),s_places(N):]
proof
   ((the entrance of N) \ diagonal(the carrier of N))~ c=
      [:s_transitions(N),s_places(N):] &
 ((the escape of N) \ diagonal(the carrier of N))~ c=
        [:s_transitions(N),s_places(N):] by Th41;
 hence thesis by Def28,Def29;
end;