The Mizar article:

Definitions of Petri Net. Part I

by
Waldemar Korczynski

Received January 31, 1992

Copyright (c) 1992 Association of Mizar Users

MML identifier: FF_SIEC
[ MML identifier index ]


environ

 vocabulary NET_1, BOOLE, RELAT_1, FF_SIEC, FUNCT_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, NET_1;
 constructors TARSKI, NET_1, XBOOLE_0;
 clusters RELAT_1, NET_1, SYSREL, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 theorems ZFMISC_1, RELAT_1, SYSREL, TARSKI, RELSET_1, NET_1, XBOOLE_0,
      XBOOLE_1;

begin :: F - Nets

 reserve x,y,X,Y for set;

definition
 let N be Net;
 canceled;

 func chaos(N) -> set equals
:Def2: Elements(N) \/ {Elements(N)};
 correctness;
end;

reserve M for Pnet;

definition let X,Y;
 assume A1: X misses Y;
 canceled;

 func PTempty_f_net(X,Y) -> strict Pnet equals
 :Def4: Net (# X, Y, {} #);
 correctness
 proof
  set M = Net (# X, Y, {} #);
    (the Places of M) misses (the Transitions of M) &
   (the Flow of M) c= [:the Places of M, the Transitions of M:] \/
            [:the Transitions of M, the Places of M:] by A1,XBOOLE_1:2;
  hence thesis by NET_1:def 1;
 end;
end;

definition let X;
 func Tempty_f_net(X) -> strict Pnet equals
 :Def5: PTempty_f_net(X,{});
 correctness;

 func Pempty_f_net(X) -> strict Pnet equals
 :Def6: PTempty_f_net({},X);
 correctness;
end;

definition let x;
 func Tsingle_f_net(x) -> strict Pnet equals
 :Def7: PTempty_f_net({},{x});
 correctness;

 func Psingle_f_net(x) -> strict Pnet equals
 :Def8: PTempty_f_net({x},{});
 correctness;
end;

definition
 func empty_f_net -> strict Pnet equals
 :Def9: PTempty_f_net({},{});
 correctness;
end;

canceled;

theorem
   X misses Y implies the Places of PTempty_f_net(X,Y) = X &
      the Transitions of PTempty_f_net(X,Y) = Y &
       the Flow of PTempty_f_net(X,Y) = {}
proof
 assume X misses Y;
 then PTempty_f_net(X,Y) = Net (# X, Y, {} #) by Def4;
 hence thesis;
end;

theorem
   the Places of Tempty_f_net(X) = X &
      the Transitions of Tempty_f_net(X) = {} &
       the Flow of Tempty_f_net(X) = {}
proof
 A1:X misses {} by XBOOLE_1:65;
   Tempty_f_net(X) = PTempty_f_net(X,{}) by Def5
                .= Net (# X, {}, {} #) by A1,Def4;
 hence thesis;
end;

theorem
   for X holds the Places of Pempty_f_net(X) = {} &
      the Transitions of Pempty_f_net(X) = X &
       the Flow of Pempty_f_net(X) = {}
proof
 let X;
 A1: {} misses X by XBOOLE_1:65;
   Pempty_f_net(X) = PTempty_f_net({},X) by Def6
                .= Net (# {}, X, {} #) by A1,Def4;
 hence thesis;
end;

theorem
   for x holds the Places of (Tsingle_f_net(x)) = {} &
      the Transitions of (Tsingle_f_net(x)) = {x} &
       the Flow of (Tsingle_f_net(x)) = {}
proof
 let x;
 A1: {} misses {x} by XBOOLE_1:65;
   Tsingle_f_net(x) = PTempty_f_net({},{x}) by Def7
                 .= Net (# {}, {x}, {} #) by A1,Def4;
 hence thesis;
end;

theorem
   for x holds the Places of (Psingle_f_net(x)) = {x} &
      the Transitions of (Psingle_f_net(x)) = {} &
       the Flow of (Psingle_f_net(x)) = {}
proof
 let x;
 A1:{x} misses {} by XBOOLE_1:65;
   Psingle_f_net(x) = PTempty_f_net({x},{}) by Def8
                 .= Net (# {x}, {}, {} #) by A1,Def4;
 hence thesis;
end;

theorem
   the Places of empty_f_net = {} &
  the Transitions of empty_f_net = {} &
    the Flow of empty_f_net = {}
proof
  {} misses {} by XBOOLE_1:65;
 then empty_f_net = Net (# {}, {}, {} #) by Def4,Def9;
 hence thesis;
end;

theorem
  the Places of M c= Elements M & the Transitions of M c= Elements M
   by NET_1:4,5;

canceled 2;

theorem Th11:
 (([x,y] in the Flow of M & x in the Transitions of M) implies
   not x in the Places of M & not y in the Transitions of M &
                                           y in the Places of M) &
 (([x,y] in the Flow of M & y in the Transitions of M) implies
   not y in the Places of M & not x in the Transitions of M &
                                           x in the Places of M) &
 (([x,y] in the Flow of M & x in the Places of M) implies
   not y in the Places of M & not x in the Transitions of M &
                                      y in the Transitions of M) &
 (([x,y] in the Flow of M & y in the Places of M) implies
   not x in the Places of M & not y in the Transitions of M &
                                      x in the Transitions of M)
proof
   (the Places of M) misses (the Transitions of M) &
  ((the Flow of M) c= [:the Places of M, the Transitions of M:] \/
               [:the Transitions of M, the Places of M:]) by NET_1:def 1;
 hence thesis by SYSREL:22;
end;

theorem
   chaos(M) <> {}
proof
 A1:chaos(M) = Elements(M) \/ {Elements(M)} by Def2;
   Elements(M) in {Elements(M)} by TARSKI:def 1;
 hence thesis by A1,XBOOLE_0:def 2;
end;

theorem Th13:
 (the Flow of M) c= [:Elements(M), Elements(M):] &
                      (the Flow of M)~ c= [:Elements(M), Elements(M):]
proof
    (the Flow of M) c= [:Elements(M), Elements(M):]
 proof
  A1: the Places of M c= Elements(M) by NET_1:4;
  A2:the Transitions of M c= Elements(M) by NET_1:5;
  then A3:[:the Places of M, the Transitions of M:] c=
                        [:Elements(M), Elements(M):] by A1,ZFMISC_1:119;
    [:the Transitions of M, the Places of M:] c=
                       [:Elements(M), Elements(M):] by A1,A2,ZFMISC_1:119;
  then A4:[:the Places of M, the Transitions of M:] \/
         [:the Transitions of M, the Places of M:] c=
                              [:Elements(M), Elements(M):] by A3,XBOOLE_1:8;
    the Flow of M c= [:the Places of M, the Transitions of M:] \/
                    [:the Transitions of M, the Places of M:] by NET_1:def 1;
  hence thesis by A4,XBOOLE_1:1;
 end;
 hence thesis by SYSREL:16;
end;

theorem Th14:
 rng ((the Flow of M)|(the Transitions of M)) c= (the Places of M) &
       rng ((the Flow of M)~|(the Transitions of M)) c= (the Places of M) &
         dom ((the Flow of M)|(the Transitions of M)) c=
                            (the Transitions of M) &
         dom ((the Flow of M)~|(the Transitions of M)) c=
                            (the Transitions of M) &
         rng ((the Flow of M)|(the Places of M)) c= (the Transitions of M) &
        rng ((the Flow of M)~|(the Places of M)) c= (the Transitions of M) &
         dom ((the Flow of M)|(the Places of M)) c= (the Places of M) &
         dom ((the Flow of M)~|(the Places of M)) c= (the Places of M) &
         rng id(the Transitions of M) c= (the Transitions of M) &
         dom id(the Transitions of M) c= (the Transitions of M) &
         rng id(the Places of M) c= (the Places of M) &
         dom id(the Places of M) c= (the Places of M)
proof
 A1:rng ((the Flow of M)|(the Transitions of M)) c= (the Places of M)
 proof
    for x holds x in rng ((the Flow of M)|(the Transitions of M)) implies
                                              x in (the Places of M)
  proof
   let x;
   assume x in rng ((the Flow of M)|(the Transitions of M));
   then consider y such that A2:[y,x] in
                (the Flow of M)|(the Transitions of M) by RELAT_1:def 5;
     y in (the Transitions of M) & [y,x] in (the Flow of M) by A2,RELAT_1:def
11
;
   hence thesis by Th11;
  end;
  hence thesis by TARSKI:def 3;
 end;
 A3: rng ((the Flow of M)~|(the Transitions of M)) c= (the Places of M)
 proof
    for x holds x in rng ((the Flow of M)~|(the Transitions of M)) implies
                                              x in (the Places of M)
  proof
   let x;
   assume x in rng ((the Flow of M)~|(the Transitions of M));
   then consider y such that
A4: [y,x] in (the Flow of M)~|(the Transitions of M) by RELAT_1:def 5;
     y in (the Transitions of M) & [y,x] in (the Flow of M)~ by A4,RELAT_1:def
11
;
   then y in (the Transitions of M) & [x,y] in (the Flow of M) by RELAT_1:def 7
;
   hence thesis by Th11;
  end;
  hence thesis by TARSKI:def 3;
 end;
 A5:rng ((the Flow of M)|(the Places of M)) c= (the Transitions of M)
 proof
    for x holds x in rng ((the Flow of M)|(the Places of M)) implies
                                              x in (the Transitions of M)
  proof
   let x;
   assume x in rng ((the Flow of M)|(the Places of M));
   then consider y such that A6:[y,x] in (the Flow of M)|(the Places of M) by
RELAT_1:def 5;
     y in (the Places of M) & [y,x] in (the Flow of M) by A6,RELAT_1:def 11;
   hence thesis by Th11;
  end;
  hence thesis by TARSKI:def 3;
 end;
   rng ((the Flow of M)~|(the Places of M)) c= (the Transitions of M)
 proof
    for x holds x in rng ((the Flow of M)~|(the Places of M)) implies
                                              x in (the Transitions of M)
  proof
   let x;
   assume x in rng ((the Flow of M)~|(the Places of M));
   then consider y such that A7:
        [y,x] in (the Flow of M)~|(the Places of M) by RELAT_1:def 5;
     y in (the Places of M) & [y,x] in (the Flow of M)~ by A7,RELAT_1:def 11;
   then y in (the Places of M) & [x,y] in (the Flow of M) by RELAT_1:def 7;
   hence thesis by Th11;
  end;
  hence thesis by TARSKI:def 3;
 end;
 hence thesis by A1,A3,A5,RELAT_1:71,87;
end;

Lm1:
  for A,B,C,D being set st B misses D & A c= B & C c= D holds
    A misses C
proof
  let A,B,C,D be set; assume A1: B misses D & A c= B & C c= D;
  assume A meets C;
  then consider x be set such that
A2:  x in A /\ C by XBOOLE_0:4;
    A /\ C c= B /\ D by A1,XBOOLE_1:27;
  hence thesis by A1,A2,XBOOLE_0:4;
end;

theorem Th15:
        rng ((the Flow of M)|(the Transitions of M)) misses
             dom((the Flow of M)|(the Transitions of M)) &
        rng ((the Flow of M)|(the Transitions of M)) misses
             dom((the Flow of M)~|(the Transitions of M)) &
        rng ((the Flow of M)|(the Transitions of M)) misses
             dom(id(the Transitions of M)) &

        rng ((the Flow of M)~|(the Transitions of M)) misses
             dom((the Flow of M)|(the Transitions of M)) &
        rng ((the Flow of M)~|(the Transitions of M)) misses
             dom((the Flow of M)~|(the Transitions of M)) &
        rng ((the Flow of M)~|(the Transitions of M)) misses
             dom(id(the Transitions of M)) &

        dom ((the Flow of M)|(the Transitions of M)) misses
             rng((the Flow of M)|(the Transitions of M)) &
        dom ((the Flow of M)|(the Transitions of M)) misses
             rng((the Flow of M)~|(the Transitions of M)) &
        dom ((the Flow of M)|(the Transitions of M)) misses
             rng(id(the Places of M)) &

        dom ((the Flow of M)~|(the Transitions of M)) misses
             rng((the Flow of M)|(the Transitions of M)) &
        dom ((the Flow of M)~|(the Transitions of M)) misses
             rng((the Flow of M)~|(the Transitions of M)) &
        dom ((the Flow of M)~|(the Transitions of M)) misses
             rng(id(the Places of M)) &

        rng ((the Flow of M)|(the Places of M)) misses
             dom((the Flow of M)|(the Places of M)) &
        rng ((the Flow of M)|(the Places of M)) misses
             dom((the Flow of M)~|(the Places of M)) &
        rng ((the Flow of M)|(the Places of M)) misses
             dom(id(the Places of M)) &

        rng ((the Flow of M)~|(the Places of M)) misses
             dom((the Flow of M)|(the Places of M)) &
        rng ((the Flow of M)~|(the Places of M)) misses
             dom((the Flow of M)~|(the Places of M)) &
        rng ((the Flow of M)~|(the Places of M)) misses
             dom(id(the Places of M)) &

        dom ((the Flow of M)|(the Places of M)) misses
             rng((the Flow of M)|(the Places of M)) &
        dom ((the Flow of M)|(the Places of M)) misses
             rng((the Flow of M)~|(the Places of M)) &
        dom ((the Flow of M)|(the Places of M)) misses
             rng(id(the Transitions of M)) &

        dom ((the Flow of M)~|(the Places of M)) misses
             rng((the Flow of M)|(the Places of M)) &
        dom ((the Flow of M)~|(the Places of M)) misses
             rng((the Flow of M)~|(the Places of M)) &
        dom ((the Flow of M)~|(the Places of M)) misses
             rng(id(the Transitions of M))
proof
 set R = (the Flow of M)|(the Transitions of M);
 set S = (the Flow of M)~|(the Transitions of M);
 set T = id(the Transitions of M);
 set R1 = (the Flow of M)|(the Places of M);
 set S1 = (the Flow of M)~|(the Places of M);
 set T1 = id(the Places of M);
 A1:dom R c= the Transitions of M & rng R c= the Places of M by Th14;
 A2:dom S c= the Transitions of M & rng S c= the Places of M by Th14;
 A3:dom T c= the Transitions of M & rng T c= the Transitions of M by Th14;
 A4:dom R1 c= the Places of M & rng R1 c= the Transitions of M by Th14;
 A5:dom S1 c= the Places of M & rng S1 c= the Transitions of M by Th14;
 A6:dom T1 c= the Places of M & rng T1 c= the Places of M by Th14;
   (the Places of M) misses (the Transitions of M) by NET_1:def 1;
 hence thesis by A1,A2,A3,A4,A5,A6,Lm1;
end;

theorem Th16:
        (((the Flow of M)|(the Transitions of M)) *
           ((the Flow of M)|(the Transitions of M)) = {}) &
        (((the Flow of M)~|(the Transitions of M)) *
           ((the Flow of M)~|(the Transitions of M)) = {}) &
        (((the Flow of M)|(the Transitions of M)) *
           ((the Flow of M)~|(the Transitions of M)) = {}) &
        (((the Flow of M)~|(the Transitions of M)) *
           ((the Flow of M)|(the Transitions of M)) = {}) &

       (((the Flow of M)|(the Places of M)) *
           ((the Flow of M)|(the Places of M)) = {}) &
        (((the Flow of M)~|(the Places of M)) *
           ((the Flow of M)~|(the Places of M)) = {}) &
        (((the Flow of M)|(the Places of M)) *
           ((the Flow of M)~|(the Places of M)) = {}) &
        (((the Flow of M)~|(the Places of M)) *
           ((the Flow of M)|(the Places of M)) = {})
proof
 A1:(((the Flow of M)|(the Transitions of M)) *
           ((the Flow of M)|(the Transitions of M)) = {})
 proof
    rng ((the Flow of M)|(the Transitions of M)) misses
    dom ((the Flow of M)|(the Transitions of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A2:((the Flow of M)~|(the Transitions of M)) *
           ((the Flow of M)~|(the Transitions of M)) = {}
 proof
    rng ((the Flow of M)~|(the Transitions of M)) misses
    dom ((the Flow of M)~|(the Transitions of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A3:((the Flow of M)|(the Transitions of M)) *
           ((the Flow of M)~|(the Transitions of M)) = {}
 proof
    rng ((the Flow of M)|(the Transitions of M)) misses
    dom ((the Flow of M)~|(the Transitions of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A4:((the Flow of M)~|(the Transitions of M)) *
           ((the Flow of M)|(the Transitions of M)) = {}
 proof
    rng ((the Flow of M)~|(the Transitions of M)) misses
    dom ((the Flow of M)|(the Transitions of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;

 A5:(((the Flow of M)|(the Places of M)) *
           ((the Flow of M)|(the Places of M)) = {})
 proof
    rng ((the Flow of M)|(the Places of M)) misses
    dom ((the Flow of M)|(the Places of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A6:((the Flow of M)~|(the Places of M)) *
           ((the Flow of M)~|(the Places of M)) = {}
 proof
    rng ((the Flow of M)~|(the Places of M)) misses
    dom ((the Flow of M)~|(the Places of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A7:((the Flow of M)|(the Places of M)) *
           ((the Flow of M)~|(the Places of M)) = {}
 proof
    rng ((the Flow of M)|(the Places of M)) misses
    dom ((the Flow of M)~|(the Places of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
   ((the Flow of M)~|(the Places of M)) *
           ((the Flow of M)|(the Places of M)) = {}
 proof
    rng ((the Flow of M)~|(the Places of M)) misses
    dom ((the Flow of M)|(the Places of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 hence thesis by A1,A2,A3,A4,A5,A6,A7;
end;

theorem Th17:
  (((the Flow of M)|(the Transitions of M)) *
   id(the Places of M) = (the Flow of M)|(the Transitions of M)) &
        (((the Flow of M)~|(the Transitions of M)) *
  id(the Places of M) = (the Flow of M)~|(the Transitions of M)) &
        ((id(the Transitions of M) *
        ((the Flow of M)|(the Transitions of M))) =
                    (the Flow of M)|(the Transitions of M)) &
        ((id(the Transitions of M) *
        ((the Flow of M)~|(the Transitions of M))) =
                    (the Flow of M)~|(the Transitions of M)) &

   (((the Flow of M)|(the Places of M)) *
     id(the Transitions of M) = (the Flow of M)|(the Places of M)) &
        (((the Flow of M)~|(the Places of M)) *
   id(the Transitions of M) = (the Flow of M)~|(the Places of M)) &
        (id(the Places of M)) *
        ((the Flow of M)|(the Places of M)) =
                    (the Flow of M)|(the Places of M) &
   (id(the Places of M)) * ((the Flow of M)~|(the Places of M)) =
                    (the Flow of M)~|(the Places of M) &
   ((the Flow of M)|(the Places of M)) * id(the Transitions of M) =
                (the Flow of M)|(the Places of M) &
   ((the Flow of M)~|(the Places of M)) * id(the Transitions of M) =
                (the Flow of M)~|(the Places of M) &
 (id(the Transitions of M) * ((the Flow of M)|(the Places of M))) = {} &
   (id(the Transitions of M) *
          ((the Flow of M)~|(the Places of M))) = {} &
   ((the Flow of M)|(the Places of M)) * id(the Places of M) = {} &
   ((the Flow of M)~|(the Places of M)) * id(the Places of M) = {} &
   (id(the Places of M)) *
     ((the Flow of M)|(the Transitions of M)) = {} &
        (id(the Places of M)) *
        ((the Flow of M)~|(the Transitions of M)) = {} &
   ((the Flow of M)|(the Transitions of M)) *
                 (id(the Transitions of M)) = {} &
   ((the Flow of M)~|(the Transitions of M)) *
                (id(the Transitions of M)) = {}
proof
 A1: ((the Flow of M)|(the Transitions of M)) *
     id(the Places of M) = (the Flow of M)|(the Transitions of M)
 proof
    rng ((the Flow of M)|(the Transitions of M)) c= the Places of M by Th14;
  hence thesis by RELAT_1:79;
 end;
 A2:((the Flow of M)~|(the Transitions of M)) *
     id(the Places of M) = (the Flow of M)~|(the Transitions of M)
 proof
    rng ((the Flow of M)~|(the Transitions of M)) c= the Places of M by Th14;
  hence thesis by RELAT_1:79;
 end;
 A3:(id(the Transitions of M) *
        ((the Flow of M)|(the Transitions of M))) =
                    (the Flow of M)|(the Transitions of M)
 proof
    dom ((the Flow of M)|(the Transitions of M)) c= the Transitions of M
    by Th14;
  hence thesis by RELAT_1:77;
 end;
 A4:(id(the Transitions of M) *
        ((the Flow of M)~|(the Transitions of M))) =
                    (the Flow of M)~|(the Transitions of M)
 proof
    dom ((the Flow of M)~|(the Transitions of M)) c= (the Transitions of M)
                                                    by Th14;
  hence thesis by RELAT_1:77;
 end;

 A5: ((the Flow of M)|(the Places of M)) *
     id(the Transitions of M) = (the Flow of M)|(the Places of M)
 proof
    rng ((the Flow of M)|(the Places of M)) c= the Transitions of M by Th14;
  hence thesis by RELAT_1:79;
 end;
 A6:((the Flow of M)~|(the Places of M)) *
     id(the Transitions of M) = (the Flow of M)~|(the Places of M)
 proof
    rng ((the Flow of M)~|(the Places of M)) c= the Transitions of M by Th14;
  hence thesis by RELAT_1:79;
 end;
 A7:(id(the Places of M) *
        ((the Flow of M)|(the Places of M))) =
                    (the Flow of M)|(the Places of M)
 proof
    dom ((the Flow of M)|(the Places of M)) c= the Places of M by Th14;
  hence thesis by RELAT_1:77;
 end;
 A8:(id(the Places of M) *
        ((the Flow of M)~|(the Places of M))) =
                    (the Flow of M)~|(the Places of M)
 proof
    dom ((the Flow of M)~|(the Places of M)) c= the Places of M by Th14;
  hence thesis by RELAT_1:77;
 end;
 A9:(id(the Transitions of M) *
        ((the Flow of M)|(the Places of M))) = {}
 proof
    dom ((the Flow of M)|(the Places of M)) misses
   rng (id(the Transitions of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A10:(id(the Transitions of M) *
        ((the Flow of M)~|(the Places of M))) = {}
 proof
    dom ((the Flow of M)~|(the Places of M)) misses
   rng (id(the Transitions of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A11: ((the Flow of M)|(the Places of M)) *
            id(the Places of M) = {}
 proof
    rng ((the Flow of M)|(the Places of M)) misses
   dom (id(the Places of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A12:((the Flow of M)~|(the Places of M)) *
     id(the Places of M) = {}
 proof
    rng ((the Flow of M)~|(the Places of M)) misses
   dom (id(the Places of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A13:(id(the Places of M) *
        ((the Flow of M)|(the Transitions of M))) = {}
 proof
    rng id(the Places of M) misses
    dom ((the Flow of M)|(the Transitions of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A14:(id(the Places of M) *
        ((the Flow of M)~|(the Transitions of M))) = {}
 proof
    rng id(the Places of M) misses
    dom ((the Flow of M)~|(the Transitions of M)) by Th15;
  hence thesis by RELAT_1:67;
 end;
 A15:((the Flow of M)|(the Transitions of M)) *
                     id(the Transitions of M) = {}
 proof
    rng ((the Flow of M)|(the Transitions of M)) misses
   dom id(the Transitions of M) by Th15;
  hence thesis by RELAT_1:67;
 end;
   ((the Flow of M)~|(the Transitions of M)) *
                     id(the Transitions of M) = {}
 proof
    rng ((the Flow of M)~|(the Transitions of M)) misses
   dom id(the Transitions of M) by Th15;
  hence thesis by RELAT_1:67;
 end;
 hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15;
end;

theorem Th18:
  (((the Flow of M)~|(the Transitions of M)) misses (id(Elements(M)))) &
  (((the Flow of M)|(the Transitions of M)) misses (id(Elements(M)))) &
  (((the Flow of M)~|(the Places of M)) misses (id(Elements(M)))) &
  (((the Flow of M)|(the Places of M)) misses (id(Elements(M))))
proof
 set T = id(Elements(M));
 thus ((the Flow of M)~|(the Transitions of M)) misses (id(Elements(M)))
 proof
  set R = (the Flow of M)~|(the Transitions of M);
    for x,y holds not [x,y] in R /\ T
  proof
   let x,y;
   assume [x,y] in R /\ T;
   then A1:[x,y] in R & [x,y] in T by XBOOLE_0:def 3;
   then x in (the Transitions of M) & [x,y] in (the Flow of M)~ by RELAT_1:def
11;
   then x in (the Transitions of M) & [y,x] in (the Flow of M) by RELAT_1:def 7
;
   then x <> y by Th11;
   hence thesis by A1,RELAT_1:def 10;
  end;
  then R /\ T = {} by RELAT_1:56;
  hence thesis by XBOOLE_0:def 7;
 end;
 thus ((the Flow of M)|(the Transitions of M)) misses (id(Elements(M)))
 proof
  set R = (the Flow of M)|(the Transitions of M);
    for x,y holds not [x,y] in R /\ T
  proof
   let x,y;
   assume [x,y] in R /\ T;
   then A2:[x,y] in R & [x,y] in T by XBOOLE_0:def 3;
   then x in (the Transitions of M) & [x,y] in (the Flow of M) by RELAT_1:def
11;
   then x <> y by Th11;
   hence thesis by A2,RELAT_1:def 10;
  end; then R /\ T = {} by RELAT_1:56;
  hence thesis by XBOOLE_0:def 7;
 end;
 thus ((the Flow of M)~|(the Places of M)) misses (id(Elements(M)))
 proof
  set R = (the Flow of M)~|(the Places of M);
    for x,y holds not [x,y] in R /\ T
  proof
   let x,y;
   assume [x,y] in R /\ T;
   then A3:[x,y] in R & [x,y] in T by XBOOLE_0:def 3;
   then x in the Places of M & [x,y] in (the Flow of M)~ by RELAT_1:def 11;
   then x in the Places of M & [y,x] in the Flow of M by RELAT_1:def 7;
   then x <> y by Th11;
   hence thesis by A3,RELAT_1:def 10;
  end;
  then R /\ T = {} by RELAT_1:56;
  hence thesis by XBOOLE_0:def 7;
 end;
  set R = (the Flow of M)|(the Places of M);
    for x,y holds not [x,y] in R /\ T
  proof
   let x,y;
   assume [x,y] in R /\ T;
   then A4:[x,y] in R & [x,y] in T by XBOOLE_0:def 3;
   then x in the Places of M & [x,y] in the Flow of M by RELAT_1:def 11;
   then x <> y by Th11;
   hence thesis by A4,RELAT_1:def 10;
  end;
  then R /\ T = {} by RELAT_1:56;
  hence thesis by XBOOLE_0:def 7;
end;

theorem Th19:
         ((the Flow of M)~|(the Transitions of M)) \/
                (id(the Places of M)) \ id(Elements(M)) =
                           (the Flow of M)~|(the Transitions of M) &
         ((the Flow of M)|(the Transitions of M)) \/
                (id(the Places of M)) \ id(Elements(M)) =
                             (the Flow of M)|(the Transitions of M) &

         (((the Flow of M)~|(the Places of M)) \/
                (id(the Places of M))) \ id(Elements(M)) =
                           (the Flow of M)~|(the Places of M) &
         (((the Flow of M)|(the Places of M)) \/
                (id(the Places of M))) \ id(Elements(M)) =
                             (the Flow of M)|(the Places of M) &

         ((the Flow of M)~|(the Places of M)) \/
                (id(the Transitions of M)) \ id(Elements(M)) =
                           (the Flow of M)~|(the Places of M) &
         ((the Flow of M)|(the Places of M)) \/
                (id(the Transitions of M)) \ id(Elements(M)) =
                             (the Flow of M)|(the Places of M) &

         (((the Flow of M)~|(the Transitions of M)) \/
                (id(the Transitions of M))) \ id(Elements(M)) =
                           (the Flow of M)~|(the Transitions of M) &
         (((the Flow of M)|(the Transitions of M)) \/
                (id(the Transitions of M))) \ id(Elements(M)) =
                             (the Flow of M)|(the Transitions of M)
proof
 A1:((the Flow of M)~|(the Transitions of M)) \/
                (id(the Places of M)) \ id(Elements(M)) =
                           (the Flow of M)~|(the Transitions of M)
 proof
  set R = (the Flow of M)~|(the Transitions of M);
  set S = id(the Places of M);
  set T = id(Elements(M));
    the Places of M c= Elements(M) by NET_1:4;
  then A2: S c= T by SYSREL:33;
A3:  R misses T by Th18;
    (R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
                  .= (R \ T) \/ {} by A2,XBOOLE_1:37
                  .= R by A3,XBOOLE_1:83;
  hence thesis;
 end;
 A4:((the Flow of M)|(the Transitions of M)) \/
                (id(the Places of M)) \ id(Elements(M)) =
                           (the Flow of M)|(the Transitions of M)
 proof
  set R = (the Flow of M)|(the Transitions of M);
  set S = id(the Places of M);
  set T = id(Elements(M));
    the Places of M c= Elements(M) by NET_1:4;
  then A5: S c= T by SYSREL:33;
A6:  R misses T by Th18;
    (R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
                  .= (R \ T) \/ {} by A5,XBOOLE_1:37
                  .= R by A6,XBOOLE_1:83;
  hence thesis;
 end;
 A7:((the Flow of M)~|(the Places of M)) \/
                (id(the Places of M)) \ id(Elements(M)) =
                           (the Flow of M)~|(the Places of M)
 proof
  set R = (the Flow of M)~|(the Places of M);
  set S = id(the Places of M);
  set T = id(Elements(M));
    the Places of M c= Elements(M) by NET_1:4;
  then A8: S c= T by SYSREL:33;
A9:  R misses T by Th18;
    (R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
                  .= (R \ T) \/ {} by A8,XBOOLE_1:37
                  .= R by A9,XBOOLE_1:83;
  hence thesis;
 end;
 A10:((the Flow of M)|(the Places of M)) \/
                (id(the Places of M)) \ id(Elements(M)) =
                           (the Flow of M)|(the Places of M)
 proof
  set R = (the Flow of M)|(the Places of M);
  set S = id(the Places of M);
  set T = id(Elements(M));
    the Places of M c= Elements(M) by NET_1:4;
  then A11: S c= T by SYSREL:33;
A12:  R misses T by Th18;
    (R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
                  .= (R \ T) \/ {} by A11,XBOOLE_1:37
                  .= R by A12,XBOOLE_1:83;
  hence thesis;
 end;
 A13:((the Flow of M)~|(the Places of M)) \/
                (id(the Transitions of M)) \ id(Elements(M)) =
                           (the Flow of M)~|(the Places of M)
 proof
  set R = (the Flow of M)~|(the Places of M);
  set S = id(the Transitions of M);
  set T = id(Elements(M));
    the Transitions of M c= Elements(M) by NET_1:5;
  then A14: S c= T by SYSREL:33;
A15:  R misses T by Th18;
    (R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
                  .= (R \ T) \/ {} by A14,XBOOLE_1:37
                  .= R by A15,XBOOLE_1:83;
  hence thesis;
 end;
 A16:((the Flow of M)|(the Places of M)) \/
                (id(the Transitions of M)) \ id(Elements(M)) =
                           (the Flow of M)|(the Places of M)
 proof
  set R = (the Flow of M)|(the Places of M);
  set S = id(the Transitions of M);
  set T = id(Elements(M));
    the Transitions of M c= Elements(M) by NET_1:5;
  then A17: S c= T by SYSREL:33;
A18:  R misses T by Th18;
    (R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
                  .= (R \ T) \/ {} by A17,XBOOLE_1:37
                  .= R by A18,XBOOLE_1:83;
  hence thesis;
 end;
 A19:((the Flow of M)~|(the Transitions of M)) \/
                (id(the Transitions of M)) \ id(Elements(M)) =
                           (the Flow of M)~|(the Transitions of M)
 proof
  set R = (the Flow of M)~|(the Transitions of M);
  set S = id(the Transitions of M);
  set T = id(Elements(M));
    the Transitions of M c= Elements(M) by NET_1:5;
  then A20: S c= T by SYSREL:33;
A21:  R misses T by Th18;
    (R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
                  .= (R \ T) \/ {} by A20,XBOOLE_1:37
                  .= R by A21,XBOOLE_1:83;
  hence thesis;
 end;
   ((the Flow of M)|(the Transitions of M)) \/
                (id(the Transitions of M)) \ id(Elements(M)) =
                           (the Flow of M)|(the Transitions of M)
 proof
  set R = (the Flow of M)|(the Transitions of M);
  set S = id(the Transitions of M);
  set T = id(Elements(M));
    the Transitions of M c= Elements(M) by NET_1:5;
  then A22: S c= T by SYSREL:33;
A23:  R misses T by Th18;
    (R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
                  .= (R \ T) \/ {} by A22,XBOOLE_1:37
                  .= R by A23,XBOOLE_1:83;
  hence thesis;
 end;
 hence thesis by A1,A4,A7,A10,A13,A16,A19;
end;

theorem Th20:
          ((the Flow of M)|(the Places of M))~ =
             ((the Flow of M)~)|(the Transitions of M) &
          ((the Flow of M)|(the Transitions of M))~ =
             ((the Flow of M)~)|(the Places of M)
proof
 set R = the Flow of M;
 set X = the Places of M;
 set Y = the Transitions of M;
 A1:((R|X)~) c= ((R~)|Y)
 proof
    for x,y holds [x,y] in (R|X)~ implies [x,y] in (R~)|Y
  proof
   let x,y;
   assume [x,y] in (R|X)~;
   then [y,x] in R|X by RELAT_1:def 7;
   then [y,x] in R & y in X by RELAT_1:def 11;
   then [x,y] in R~ & x in Y by Th11,RELAT_1:def 7;
   hence thesis by RELAT_1:def 11;
  end;
  hence thesis by RELAT_1:def 3;
 end;
A2: ((R~)|Y) c= ((R|X)~)
 proof
    for x,y holds [x,y] in (R~)|Y implies [x,y] in (R|X)~
  proof
   let x,y;
   assume [x,y] in (R~)|Y;
   then [x,y] in R~ & x in Y by RELAT_1:def 11;
   then [y,x] in R & x in Y by RELAT_1:def 7;
   then [y,x] in R & y in X by Th11;
   then [y,x] in R|X by RELAT_1:def 11;
   hence thesis by RELAT_1:def 7;
  end;
  hence thesis by RELAT_1:def 3;
 end;

 A3:((R|Y)~) c= ((R~)|X)
 proof
    for x,y holds [x,y] in (R|Y)~ implies [x,y] in (R~)|X
  proof
   let x,y;
   assume [x,y] in (R|Y)~;
   then [y,x] in R|Y by RELAT_1:def 7;
   then [y,x] in R & y in Y by RELAT_1:def 11;
   then [x,y] in R~ & x in X by Th11,RELAT_1:def 7;
   hence thesis by RELAT_1:def 11;
  end;
  hence thesis by RELAT_1:def 3;
 end;
   ((R~)|X) c= ((R|Y)~)
 proof
    for x,y holds [x,y] in (R~)|X implies [x,y] in (R|Y)~
  proof
   let x,y;
   assume [x,y] in (R~)|X;
   then [x,y] in R~ & x in X by RELAT_1:def 11;
   then [y,x] in R & x in X by RELAT_1:def 7;
   then [y,x] in R & y in Y by Th11;
   then [y,x] in R|Y by RELAT_1:def 11;
   hence thesis by RELAT_1:def 7;
  end;
  hence thesis by RELAT_1:def 3;
 end;
 hence thesis by A1,A2,A3,XBOOLE_0:def 10;
end;

theorem Th21:
          ((the Flow of M)|(the Places of M)) \/
           ((the Flow of M)|(the Transitions of M)) = (the Flow of M) &
          ((the Flow of M)|(the Transitions of M)) \/
                ((the Flow of M)|(the Places of M)) = (the Flow of M) &
         (((the Flow of M)|(the Places of M))~) \/
           (((the Flow of M)|(the Transitions of M))~) = (the Flow of M)~ &
          (((the Flow of M)|(the Transitions of M))~) \/
                (((the Flow of M)|(the Places of M))~) = (the Flow of M)~
proof
 set R = the Flow of M;
 A1:the Flow of M c= [:Elements(M),Elements(M):] by Th13;
   Elements(M) = (the Places of M) \/ (the Transitions of M) by NET_1:def 2;
 then (R|the Places of M) \/ (R|the Transitions of M) = R by A1,SYSREL:25;
 hence thesis by RELAT_1:40;
end;

:: T R A N S F O R M A T I O N S
:: A [F -> E]

definition
 let M;
 func f_enter(M) -> Relation equals :Def10:
  ((the Flow of M)~|(the Transitions of M)) \/ id(the Places of M);
 correctness;

 func f_exit(M) -> Relation equals :Def11:
  ((the Flow of M)|(the Transitions of M)) \/ id(the Places of M);
 correctness;
end;

theorem
    f_exit(M) c= [:Elements(M),Elements(M):] &
    f_enter(M) c= [:Elements(M),Elements(M):]
proof
 thus f_exit(M) c= [:Elements(M),Elements(M):]
 proof
  A1:id(the Places of M) c= [:Elements(M),Elements(M):]
  proof
     (the Places of M) c= Elements(M) by NET_1:4;
   then A2: id(the Places of M) c= id(Elements(M)) by SYSREL:33;
     id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:28;
   hence thesis by A2,XBOOLE_1:1;
  end;
  A3:(the Flow of M)|(the Transitions of M) c= (the Flow of M) by RELAT_1:88;
    (the Flow of M) c= [:Elements(M),Elements(M):] by Th13;
  then (the Flow of M)|(the Transitions of M) c= [:Elements(M),Elements(M):]
                                                 by A3,XBOOLE_1:1;
  then ((the Flow of M)|(the Transitions of M)) \/
       id(the Places of M) c= [:Elements(M),Elements(M):] by A1,XBOOLE_1:8;
  hence thesis by Def11;
 end;
  A4:id(the Places of M) c= [:Elements(M),Elements(M):]
  proof
     (the Places of M) c= Elements(M) by NET_1:4;
   then A5: id(the Places of M) c= id(Elements(M)) by SYSREL:33;
     id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:28;
   hence thesis by A5,XBOOLE_1:1;
  end;
  A6:(the Flow of M)~|(the Transitions of M) c=
                                         (the Flow of M)~ by RELAT_1:88;
    (the Flow of M)~ c= [:Elements(M),Elements(M):] by Th13;
  then (the Flow of M)~|(the Transitions of M) c= [:Elements(M),Elements(M):]
                                                 by A6,XBOOLE_1:1;
  then ((the Flow of M)~|(the Transitions of M)) \/
       id(the Places of M) c= [:Elements(M),Elements(M):]
                                                 by A4,XBOOLE_1:8;
  hence thesis by Def10;
end;

theorem
    dom(f_exit(M)) c= Elements(M) & rng(f_exit(M)) c= Elements(M) &
     dom(f_enter(M)) c= Elements(M) & rng(f_enter(M)) c= Elements(M)
proof
A1: for x holds x in dom(f_exit(M)) implies x in Elements(M)
 proof
  let x;
  assume x in dom(f_exit(M));
  then x in dom(((the Flow of M)|(the Transitions of M)) \/
                         id(the Places of M)) by Def11;
  then x in dom((the Flow of M)|(the Transitions of M)) \/
                dom(id(the Places of M)) by RELAT_1:13;
  then x in dom((the Flow of M)|(the Transitions of M)) or
            x in dom(id(the Places of M)) by XBOOLE_0:def 2;
  then x in (the Transitions of M) or x in the Places of M by RELAT_1:71,86;
  then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
  hence thesis by NET_1:def 2;
 end;

A2: for x holds x in rng(f_exit(M)) implies x in Elements(M)
 proof
  let x;
  assume x in rng(f_exit(M));
  then x in rng(((the Flow of M)|(the Transitions of M)) \/
                id(the Places of M)) by Def11;
  then A3: x in rng((the Flow of M)|(the Transitions of M)) \/
                rng(id(the Places of M)) by RELAT_1:26;

  A4:x in rng((the Flow of M)|(the Transitions of M)) implies thesis
  proof
   assume x in rng((the Flow of M)|(the Transitions of M));
   then consider y such that A5:
                        [y,x] in (the Flow of M)|(the Transitions of M) by
RELAT_1:def 5;
     y in (the Transitions of M) & [y,x] in (the Flow of M) by A5,RELAT_1:def
11
;
   then x in (the Transitions of M) or x in the Places of M by Th11;
   then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
   hence thesis by NET_1:def 2;
  end;
     x in rng(id(the Places of M)) implies thesis
  proof
   assume x in rng(id(the Places of M));
   then x in (the Transitions of M) or x in the Places of M by RELAT_1:71;
   then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
   hence thesis by NET_1:def 2;
  end;
  hence thesis by A3,A4,XBOOLE_0:def 2;
 end;

A6: for x holds x in dom(f_enter(M)) implies x in Elements(M)
 proof
  let x;
  assume x in dom(f_enter(M));
  then x in dom(((the Flow of M)~|(the Transitions of M)) \/
                id(the Places of M)) by Def10;
  then x in dom((the Flow of M)~|(the Transitions of M)) \/
                dom(id(the Places of M)) by RELAT_1:13;
  then x in dom((the Flow of M)~|(the Transitions of M)) or
           x in dom(id(the Places of M)) by XBOOLE_0:def 2;
  then x in (the Transitions of M) or x in the Places of M by RELAT_1:71,86;
  then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
  hence thesis by NET_1:def 2;
 end;

   for x holds x in rng(f_enter(M)) implies x in Elements(M)
 proof
  let x;
  assume x in rng(f_enter(M));
  then x in rng(((the Flow of M)~|(the Transitions of M)) \/
                id(the Places of M)) by Def10;
  then A7: x in rng((the Flow of M)~|(the Transitions of M)) \/
                rng(id(the Places of M)) by RELAT_1:26;

  A8:x in rng((the Flow of M)~|(the Transitions of M)) implies thesis
  proof
   assume x in rng((the Flow of M)~|(the Transitions of M));
   then consider y such that A9:
                          [y,x] in (the Flow of M)~|(the Transitions of M) by
RELAT_1:def 5;
     y in (the Transitions of M) & [y,x] in (the Flow of M)~ by A9,RELAT_1:def
11
;
   then y in (the Transitions of M) & [x,y] in (the Flow of M) by RELAT_1:def 7
;
   then x in (the Transitions of M) or x in the Places of M by Th11;
   then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
   hence thesis by NET_1:def 2;
  end;
    x in rng(id(the Places of M)) implies thesis
  proof
   assume x in rng(id(the Places of M));
   then x in (the Transitions of M) or x in the Places of M by RELAT_1:71;
   then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
   hence thesis by NET_1:def 2;
  end;
  hence thesis by A7,A8,XBOOLE_0:def 2;
 end;
 hence thesis by A1,A2,A6,TARSKI:def 3;
end;

theorem
         (f_exit(M)) * (f_exit(M)) = f_exit(M) &
         (f_exit(M)) * (f_enter(M)) = f_exit(M) &
           (f_enter(M)) * (f_enter(M)) = f_enter(M) &
             (f_enter(M)) * (f_exit(M)) = f_enter(M)
proof
 A1:(f_exit(M)) * (f_exit(M)) = f_exit(M)
 proof
  set R = ((the Flow of M)|(the Transitions of M));
  set S = id(the Places of M);
  A2: S * R = {} by Th17;
  A3: R * S = R by Th17;
  A4: S * S = S by SYSREL:29;
    (f_exit(M)) * (f_exit(M)) = (R \/ S) * (f_exit(M)) by Def11
          .= (R \/ S) * (R \/ S) by Def11
          .= (R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
          .= ((R * R) \/ (R * S)) \/ (S * (R \/ S)) by RELAT_1:51
          .= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S)) by RELAT_1:51
          .= ({} \/ R) \/ ({} \/ S) by A2,A3,A4,Th16 .= f_exit(M) by Def11;
  hence thesis;
 end;
 A5:(f_exit(M)) * (f_enter(M)) = f_exit(M)
 proof
  set R = ((the Flow of M)|(the Transitions of M));
  set S = id(the Places of M);
  set T = ((the Flow of M)~|(the Transitions of M));
  A6: S * T = {} by Th17;
  A7: R * S = R by Th17;
  A8: S * S = S by SYSREL:29;
    (f_exit(M)) * (f_enter(M)) = (R \/ S) * (f_enter(M)) by Def11
                               .= (R \/ S) * (T \/ S) by Def10
                               .= (R * (T \/ S)) \/ (S * (T \/ S)) by SYSREL:20
                               .= ((R * T) \/ (R * S)) \/ (S * (T \/ S))
                                                                by RELAT_1:51
                               .= ((R * T) \/ (R * S)) \/ ((S * T) \/ (S * S))
                                                                by RELAT_1:51
                               .= ({} \/ R) \/ ({} \/ S) by A6,A7,A8,Th16
                               .=f_exit(M) by Def11;
  hence thesis;
 end;
 A9:(f_enter(M)) * (f_enter(M)) = f_enter(M)
 proof
  set R = ((the Flow of M)~|(the Transitions of M));
  set S = id(the Places of M);
  A10: S * R = {} by Th17;
  A11: R * S = R by Th17;
  A12: S * S = S by SYSREL:29;
    (f_enter(M)) * (f_enter(M)) = (R \/ S) * (f_enter(M)) by Def10
                               .= (R \/ S) * (R \/ S) by Def10
                               .= (R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
                               .= ((R * R) \/ (R * S)) \/ (S * (R \/ S))
                                                                by RELAT_1:51
                               .= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S))
                                                                by RELAT_1:51
                               .= ({} \/ R) \/ ({} \/ S) by A10,A11,A12,Th16
                               .=f_enter(M) by Def10;
  hence thesis;
 end;
   (f_enter(M)) * (f_exit(M)) = f_enter(M)
 proof
  set R = ((the Flow of M)|(the Transitions of M));
  set S = id(the Places of M);
  set T = ((the Flow of M)~|(the Transitions of M));
  A13: T * S = T by Th17;
  A14: S * R = {} by Th17;
  A15: S * S = S by SYSREL:29;
    (f_enter(M)) * (f_exit(M)) = (T \/ S) * (f_exit(M)) by Def10
                               .= (T \/ S) * (R \/ S) by Def11
                               .= (T * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
                               .= ((T * R) \/ (T * S)) \/ (S * (R \/ S))
                                                                by RELAT_1:51
                               .= ((T * R) \/ (T * S)) \/ ((S * R) \/ (S * S))
                                                                by RELAT_1:51
                               .= ({} \/ T) \/ ({} \/ S) by A13,A14,A15,Th16
                               .=f_enter(M) by Def10;
  hence thesis;
 end;
 hence thesis by A1,A5,A9;
end;

theorem
    (f_exit(M)) * (f_exit(M) \ id(Elements(M))) = {} &
    (f_enter(M)) * (f_enter(M) \ id(Elements(M))) = {}
proof
 set S = id(the Places of M);
 thus (f_exit(M)) * (f_exit(M) \ id(Elements(M))) = {}
 proof
  set R = (the Flow of M)|(the Transitions of M);
  A1: S * R = {} by Th17;
    (f_exit(M)) * (f_exit(M) \ id(Elements(M))) =
                       (R \/ S) * (f_exit(M) \ id(Elements(M)))
                                                            by Def11
                    .= (R \/ S) * ((R \/ S) \ (id(Elements(M)))) by Def11
                    .= (R \/ S) * R by Th19
                    .= (R * R) \/ (S * R) by SYSREL:20
                    .= {} by A1,Th16;
  hence thesis;
 end;
  set R = ((the Flow of M)~|(the Transitions of M));
  A2: S * R = {} by Th17;
    (f_enter(M)) * (f_enter(M) \ id(Elements(M))) =
                       (R \/ S) * (f_enter(M) \ id(Elements(M)))
                                               by Def10
                    .= (R \/ S) * ((R \/ S) \ (id(Elements(M)))) by Def10
                    .= (R \/ S) * R by Th19
                    .= (R * R) \/ (S * R) by SYSREL:20
                    .= {} by A2,Th16;
  hence thesis;
end;

::B [F ->R]
definition
 let M;
 func f_prox(M) -> Relation equals
:Def12: ((the Flow of M)|(the Places of M) \/
                        (the Flow of M)~|(the Places of M)) \/
                                              id(the Places of M);
 correctness;

 func f_flow(M) -> Relation equals
:Def13: (the Flow of M) \/ id(Elements(M));
 correctness;
end;

theorem
     f_prox(M) * f_prox(M) = f_prox(M) &
    (f_prox(M) \ id(Elements(M))) * f_prox(M) = {} &
      (f_prox(M) \/ ((f_prox(M))~)) \/ id(Elements(M)) =
                                         f_flow(M) \/ (f_flow(M))~
proof
 set R = (the Flow of M)|(the Places of M);
 set S = (the Flow of M)~|(the Places of M);
 set T = id(the Places of M);
 set Q = id(Elements(M));
 A1:((R \/ S) \/ T) \ Q = R \/ S
 proof
    ((R \/ S) \/ T) \ Q = ((R \/ T) \/ (S \/ T)) \ Q by XBOOLE_1:5
                   .= ((R \/ T) \ (id(Elements(M))) \/
                       ((S \/ T) \ (id(Elements(M))))) by XBOOLE_1:42
                   .= R \/
                       ((S \/ T) \ (id(Elements(M)))) by Th19
                   .= R \/ S by Th19;
  hence thesis;
 end;
 A2:(R \/ S) * (R \/ S) = {}
 proof
    (R \/ S) * (R \/ S) = ((R \/ S) * R) \/ ((R \/ S) *S) by SYSREL:20
                   .= ((R * R) \/ (S * R)) \/ ((R \/ S) *S) by SYSREL:20
                   .= ((R * R) \/ (S * R)) \/ ((R * S) \/ (S *S)) by SYSREL:20
                   .= ({} \/ (S * R)) \/ ((R * S) \/ (S *S)) by Th16
                   .= ({} \/ {}) \/ ((R * S) \/ (S *S)) by Th16
                   .= ({} \/ {}) \/ ({} \/ (S *S)) by Th16
                   .= {} by Th16;
  hence thesis;
 end;
 A3:R \/ S~ = the Flow of M & R~ \/ S = (the Flow of M)~
 proof
  A4:R \/ S~ = R \/ (((the Flow of M)|(the Transitions of M))~)~ by Th20
          .= the Flow of M by Th21;
    R~ \/ S = R~ \/ ((the Flow of M)|(the Transitions of M))~ by Th20
        .= (the Flow of M)~ by Th21;
  hence thesis by A4;
 end;
 A5:(R \/ S)~ \/ (R \/ S) = (the Flow of M) \/ (the Flow of M)~
 proof
    (R \/ S)~ \/ (R \/ S) = (R~ \/ S~) \/ (R \/ S) by RELAT_1:40
                      .= (R~ \/ (S \/ R)) \/ S~ by XBOOLE_1:4
                      .= ((R~ \/ S) \/ R) \/ S~ by XBOOLE_1:4
                 .= (the Flow of M) \/ (the Flow of M)~ by A3,XBOOLE_1:4;
  hence thesis;
 end;
 A6:f_prox(M) \/ (f_prox(M))~ =
      ((the Flow of M) \/ (the Flow of M)~) \/ id(the Places of M)
 proof
    f_prox(M) \/ (f_prox(M))~ = ((R \/ S) \/ T) \/ (f_prox(M))~ by Def12
                     .= ((R \/ S) \/ T) \/ ((R \/ S) \/ T)~ by Def12
                     .= ((R \/ S) \/ T) \/ ((R \/ S)~ \/ T~) by RELAT_1:40
                     .= (((R \/ S) \/ T) \/ (R \/ S)~) \/ T~ by XBOOLE_1:4
                     .= (((R \/ S) \/ (R \/ S)~) \/ T) \/ T~ by XBOOLE_1:4
                     .= ((R \/ S) \/ (R \/ S)~) \/ (T \/ T~) by XBOOLE_1:4
                     .= ((R \/ S) \/ (R \/ S)~) \/ (T \/ T) by RELAT_1:72
                     .= ((the Flow of M) \/ (the Flow of M)~) \/
                         id(the Places of M) by A5;
  hence thesis;
 end;
 A7:id(the Places of M) c= id(Elements(M))
 proof
    the Places of M c= Elements(M) by NET_1:4;
  hence thesis by SYSREL:33;
 end;
 A8:f_prox(M) * f_prox(M) = f_prox(M) * ((R \/ S) \/ T) by Def12

                        .= (((R \/ S) \/ T) * ((R \/ S) \/ T)) by Def12
                        .= (((R \/ S) \/ T) * (R \/ S)) \/
                            (((R \/ S) \/ T) * T) by SYSREL:20
                        .= ((((R \/ S) \/ T) * R ) \/ (((R \/ S) \/ T) * S)) \/
                            (((R \/ S) \/ T) * T) by SYSREL:20
                        .= (((R \/ S) * R ) \/ (T * R )) \/
                            (((R \/ S) \/ T) * S) \/
                              (((R \/ S) \/ T) * T) by SYSREL:20
                        .= (((R * R) \/ (S * R)) \/ (T * R )) \/
                            (((R \/ S) \/ T) * S) \/
                              (((R \/ S) \/ T) * T) by SYSREL:20
                        .= (((R * R) \/ (S * R)) \/ (T * R )) \/
                            (((R \/ S) * S) \/ (T * S)) \/
                              (((R \/ S) \/ T) * T) by SYSREL:20
                        .= (((R * R) \/ (S * R)) \/ (T * R )) \/
                            (((R * S) \/ (S * S)) \/ (T * S)) \/
                              (((R \/ S) \/ T) * T) by SYSREL:20
                        .= (((R * R) \/ (S * R)) \/ (T * R )) \/
                            (((R * S) \/ (S * S)) \/ (T * S)) \/
                              (((R \/ S) * T) \/ (T * T)) by SYSREL:20
                        .= (((R * R) \/ (S * R)) \/ (T * R )) \/
                            (((R * S) \/ (S * S)) \/ (T * S)) \/
                              (((R * T) \/ (S * T)) \/ (T * T)) by SYSREL:20
                        .= (({} \/ (S * R)) \/ (T * R )) \/
                           (((R * S) \/ (S * S)) \/ (T * S)) \/
                              (((R * T) \/ (S * T)) \/ (T * T)) by Th16
                        .= (({} \/ {}) \/ (T * R )) \/
                           (((R * S) \/ (S * S)) \/ (T * S)) \/
                              (((R * T) \/ (S * T)) \/ (T * T)) by Th16
                        .= (({} \/ {}) \/ (T * R )) \/
                           (({} \/ (S * S)) \/ (T * S)) \/
                              (((R * T) \/ (S * T)) \/ (T * T)) by Th16
                        .= (T * R ) \/ ({} \/ (T * S)) \/
                              (((R * T) \/ (S * T)) \/ (T * T)) by Th16
                        .= R \/ (T * S) \/
                              (((R * T) \/ (S * T)) \/ (T * T)) by Th17
                        .= R \/ S \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th17
                        .= R \/ S \/ (((R * T) \/ (S * T)) \/ T) by SYSREL:29
                        .= R \/ S \/ (({} \/ (S * T)) \/ T) by Th17
                        .= R \/ S \/ ({} \/ T) by Th17
                        .= f_prox(M) by Def12;

 A9: (f_prox(M) \ id(Elements(M))) * f_prox(M) =
     (f_prox(M) \ id(Elements(M))) * ((R \/ S) \/ T) by Def12
   .= (R \/ S) * ((R \/ S) \/ T) by A1,Def12
   .= {} \/ ((R \/ S) * T) by A2,SYSREL:20
   .= (R * T) \/ (S * T) by SYSREL:20
   .= {} \/ (S * T) by Th17
   .= {} by Th17;

     (f_prox(M) \/ (f_prox(M))~) \/ id(Elements(M)) =
(((the Flow of M) \/ (the Flow of M)~) \/ (id(the Places of M) \/
                               id(Elements(M)))) by A6,XBOOLE_1:4
    .= (((the Flow of M) \/ (the Flow of M)~) \/ id(Elements(M)))
                                                          by A7,XBOOLE_1:12
    .= ((the Flow of M) \/ id(Elements(M))) \/
                    ((the Flow of M)~ \/ id(Elements(M))) by XBOOLE_1:5
    .= ((the Flow of M) \/ id(Elements(M))) \/
                 ((the Flow of M)~ \/ (id(Elements(M)))~) by RELAT_1:72
    .= ((the Flow of M) \/ id(Elements(M))) \/
                 ((the Flow of M) \/ id(Elements(M)))~ by RELAT_1:40
    .= f_flow(M) \/
                 ((the Flow of M) \/ id(Elements(M)))~ by Def13
    .= f_flow(M) \/ (f_flow(M))~ by Def13;
  hence thesis by A8,A9;
 end;

::C [F ->P]
 definition let M;
  func f_places(M) -> set equals
  :Def14: the Places of M;
  correctness;

  func f_transitions(M) -> set equals
  :Def15: the Transitions of M;
  correctness;

  func f_pre(M) -> Relation equals
  :Def16: (the Flow of M)|(the Transitions of M);
  correctness;

  func f_post(M) -> Relation equals
  :Def17: (the Flow of M)~|(the Transitions of M);
  correctness;
 end;

theorem
          f_pre(M) c= [:f_transitions(M),f_places(M):] &
          f_post(M) c= [:f_transitions(M),f_places(M):]
proof
A1: for x,y holds [x,y] in f_pre(M) implies
                  [x,y] in [:f_transitions(M),f_places(M):]
 proof
  let x,y;
  assume [x,y] in f_pre(M);
  then [x,y] in (the Flow of M)|(the Transitions of M) by Def16;
  then x in (the Transitions of M) & [x,y] in (the Flow of M) by RELAT_1:def 11
;
  then x in f_transitions(M) & y in (the Places of M) by Def15,Th11;
  then x in f_transitions(M) & y in f_places(M) by Def14;
  hence thesis by ZFMISC_1:106;
 end;
   for x,y holds [x,y] in f_post(M) implies
                  [x,y] in [:f_transitions(M),f_places(M):]
 proof
  let x,y;
  assume [x,y] in f_post(M);
  then [x,y] in (the Flow of M)~|(the Transitions of M) by Def17;
  then x in (the Transitions of M) & [x,y] in (the Flow of M)~ by RELAT_1:def
11;
  then x in (the Transitions of M) & [y,x] in (the Flow of M) by RELAT_1:def 7
;
  then x in f_transitions(M) & y in (the Places of M) by Def15,Th11;
  then x in f_transitions(M) & y in f_places(M) by Def14;
  hence thesis by ZFMISC_1:106;
 end;
 hence thesis by A1,RELAT_1:def 3;
end;

theorem
    f_places(M) misses f_transitions(M)
proof
    f_places(M) = the Places of M &
    f_transitions(M) = the Transitions of M by Def14,Def15;
  hence thesis by NET_1:def 1;
end;

theorem
        f_prox(M) c= [:Elements(M), Elements(M):] &
       f_flow(M) c= [:Elements(M), Elements(M):]
proof
 thus f_prox(M) c= [:Elements(M), Elements(M):]
 proof
  A1:(the Flow of M)|(the Places of M) c= the Flow of M by RELAT_1:88;
    the Flow of M c= [:Elements(M), Elements(M):] by Th13;
  then A2:(the Flow of M)|(the Places of M) c= [:Elements(M), Elements(M):]
                                                      by A1,XBOOLE_1:1;
  A3:(the Flow of M)~|(the Places of M) c= (the Flow of M)~ by RELAT_1:88;
    (the Flow of M)~ c= [:Elements(M), Elements(M):] by Th13;
  then A4:(the Flow of M)~|(the Places of M) c= [:Elements(M), Elements(M):]
                                                      by A3,XBOOLE_1:1;
    the Places of M c= Elements(M) by NET_1:4;
  then A5:[:the Places of M, the Places of M:] c=
    [:Elements(M), Elements(M):] by ZFMISC_1:119;
    id(the Places of M) c= [:the Places of M, the Places of M:]
                                                      by RELSET_1:28;
  then A6:id(the Places of M) c= [:Elements(M), Elements(M):]
    by A5,XBOOLE_1:1;
    (the Flow of M)|(the Places of M) \/
    (the Flow of M)~|(the Places of M) c= [:Elements(M), Elements(M):]
                                                      by A2,A4,XBOOLE_1:8;
  then ((the Flow of M)|(the Places of M) \/
    (the Flow of M)~|(the Places of M)) \/
       id(the Places of M) c= [:Elements(M), Elements(M):]
                                                      by A6,XBOOLE_1:8;
  hence thesis by Def12;
 end;
  A7:the Flow of M c= [:Elements(M), Elements(M):] by Th13;
    id(Elements(M)) c= [:Elements(M), Elements(M):] by RELSET_1:28;
  then (the Flow of M) \/ id(Elements(M)) c= [:Elements(M), Elements(M)
:]
                                             by A7,XBOOLE_1:8;
  hence thesis by Def13;
end;

::A [F -> E]
definition let M;
 func f_entrance(M) -> Relation equals :Def18:
   ((the Flow of M)~|(the Places of M)) \/ id(the Transitions of M);
 correctness;

 func f_escape(M) -> Relation equals :Def19:
   ((the Flow of M)|(the Places of M)) \/ id(the Transitions of M);
 correctness;
end;

theorem
         f_escape(M) c= [:Elements(M),Elements(M):] &
         f_entrance(M) c= [:Elements(M),Elements(M):]
proof
 thus f_escape(M) c= [:Elements(M),Elements(M):]
 proof
  A1:id(the Transitions of M) c= [:Elements(M),Elements(M):]
  proof
     (the Transitions of M) c= Elements(M) by NET_1:5;
   then A2: id(the Transitions of M) c= id(Elements(M))
     by SYSREL:33;
     id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:28;
   hence thesis by A2,XBOOLE_1:1;
  end;
  A3:(the Flow of M)|(the Places of M) c= (the Flow of M) by RELAT_1:88;
    (the Flow of M) c= [:Elements(M),Elements(M):] by Th13;
  then (the Flow of M)|(the Places of M) c= [:Elements(M),Elements(M):]
                                                 by A3,XBOOLE_1:1;
  then ((the Flow of M)|(the Places of M)) \/
       id(the Transitions of M) c= [:Elements(M),Elements(M):]
                                                 by A1,XBOOLE_1:8;
  hence thesis by Def19;
 end;
  A4:id(the Transitions of M) c= [:Elements(M),Elements(M):]
  proof
     (the Transitions of M) c= Elements(M) by NET_1:5;
   then A5: id(the Transitions of M) c= id(Elements(M))
     by SYSREL:33;
     id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:28;
   hence thesis by A5,XBOOLE_1:1;
  end;
  A6:(the Flow of M)~|(the Places of M) c= (the Flow of M)~ by RELAT_1:88;
    (the Flow of M)~ c= [:Elements(M),Elements(M):] by Th13;
  then (the Flow of M)~|(the Places of M) c= [:Elements(M),Elements(M):]
                                                 by A6,XBOOLE_1:1;
  then ((the Flow of M)~|(the Places of M)) \/
       id(the Transitions of M) c= [:Elements(M),Elements(M):]
                                                 by A4,XBOOLE_1:8;
  hence thesis by Def18;
end;

theorem
         dom(f_escape(M)) c= Elements(M) & rng(f_escape(M)) c= Elements(M) &
         dom(f_entrance(M)) c= Elements(M) & rng(f_entrance(M)) c= Elements(M)
proof
A1: for x holds x in dom(f_escape(M)) implies x in Elements(M)
 proof
  let x;
  assume x in dom(f_escape(M));
  then x in dom(((the Flow of M)|(the Places of M)) \/
                         id(the Transitions of M)) by Def19;
  then x in dom((the Flow of M)|(the Places of M)) \/
                dom(id(the Transitions of M)) by RELAT_1:13;
  then x in dom((the Flow of M)|(the Places of M)) or
            x in dom(id(the Transitions of M)) by XBOOLE_0:def 2;
  then x in (the Places of M) or x in the Transitions of M by RELAT_1:71,86;
  then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
  hence thesis by NET_1:def 2;
 end;

A2: for x holds x in rng(f_escape(M)) implies x in Elements(M)
 proof
  let x;
  assume x in rng(f_escape(M));
  then x in rng(((the Flow of M)|(the Places of M)) \/
                id(the Transitions of M)) by Def19;
  then A3: x in rng((the Flow of M)|(the Places of M)) \/
                rng(id(the Transitions of M)) by RELAT_1:26;

  A4:x in rng((the Flow of M)|(the Places of M)) implies thesis
  proof
   assume x in rng((the Flow of M)|(the Places of M));
   then consider y such that A5:[y,x] in (the Flow of M)|(the Places of M) by
RELAT_1:def 5;
     y in (the Places of M) & [y,x] in (the Flow of M) by A5,RELAT_1:def 11;
   then x in (the Places of M) or x in the Transitions of M by Th11;
   then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
   hence thesis by NET_1:def 2;
  end;
     x in rng(id(the Transitions of M)) implies thesis
  proof
   assume x in rng(id(the Transitions of M));
   then x in (the Places of M) or x in the Transitions of M by RELAT_1:71;
   then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
   hence thesis by NET_1:def 2;
  end;
  hence thesis by A3,A4,XBOOLE_0:def 2;
 end;

A6: for x holds x in dom(f_entrance(M)) implies x in Elements(M)
 proof
  let x;
  assume x in dom(f_entrance(M));
  then x in dom(((the Flow of M)~|(the Places of M)) \/
                id(the Transitions of M)) by Def18;
  then x in dom((the Flow of M)~|(the Places of M)) \/
                dom(id(the Transitions of M)) by RELAT_1:13;
  then x in dom((the Flow of M)~|(the Places of M)) or
           x in dom(id(the Transitions of M)) by XBOOLE_0:def 2;
  then x in (the Places of M) or x in the Transitions of M by RELAT_1:71,86;
  then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
  hence thesis by NET_1:def 2;
 end;

   for x holds x in rng(f_entrance(M)) implies x in Elements(M)
 proof
  let x;
  assume x in rng(f_entrance(M));
  then x in rng(((the Flow of M)~|(the Places of M)) \/
                id(the Transitions of M)) by Def18;
  then A7: x in rng((the Flow of M)~|(the Places of M)) \/
                rng(id(the Transitions of M)) by RELAT_1:26;

  A8:x in rng((the Flow of M)~|(the Places of M)) implies thesis
  proof
   assume x in rng((the Flow of M)~|(the Places of M));
   then consider y such that A9:
                          [y,x] in (the Flow of M)~|(the Places of M) by
RELAT_1:def 5;
     y in (the Places of M) & [y,x] in (the Flow of M)~ by A9,RELAT_1:def 11;
   then y in (the Places of M) & [x,y] in (the Flow of M) by RELAT_1:def 7;
   then x in (the Places of M) or x in the Transitions of M by Th11;
   then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
   hence thesis by NET_1:def 2;
  end;
     x in rng(id(the Transitions of M)) implies thesis
  proof
   assume x in rng(id(the Transitions of M));
   then x in (the Places of M) or x in the Transitions of M by RELAT_1:71;
   then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
   hence thesis by NET_1:def 2;
  end;
  hence thesis by A7,A8,XBOOLE_0:def 2;
 end;
 hence thesis by A1,A2,A6,TARSKI:def 3;
end;

theorem
         (f_escape(M)) * (f_escape(M)) = f_escape(M) &
         (f_escape(M)) * (f_entrance(M)) = f_escape(M) &
           (f_entrance(M)) * (f_entrance(M)) =f_entrance(M) &
             (f_entrance(M)) * (f_escape(M)) = f_entrance(M)
proof
 set R = ((the Flow of M)|(the Places of M));
 set S = id(the Transitions of M);
 A1:(f_escape(M)) * (f_escape(M)) = f_escape(M)
 proof
  A2: S * R = {} by Th17;
  A3: R * S = R by Th17;
  A4: S * S = S by SYSREL:29;
    (f_escape(M)) * (f_escape(M)) = (R \/ S) * (f_escape(M)) by Def19
                             .= (R \/ S) * (R \/ S) by Def19
                             .= (R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
                             .= ((R * R) \/ (R * S)) \/ (S * (R \/ S))
                                                              by RELAT_1:51
                             .= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S))
                                                              by RELAT_1:51
                             .= ({} \/ R) \/ ({} \/ S) by A2,A3,A4,Th16
                             .=f_escape(M) by Def19;
  hence thesis;
 end;
 A5:(f_escape(M)) * (f_entrance(M)) = f_escape(M)
 proof
  set T = ((the Flow of M)~|(the Places of M));
  A6: S * T = {} by Th17;
  A7: R * S = R by Th17;
  A8: S * S = S by SYSREL:29;
    (f_escape(M)) * (f_entrance(M)) = (R \/ S) * (f_entrance(M)) by Def19
                               .= (R \/ S) * (T \/ S) by Def18
                               .= (R * (T \/ S)) \/ (S * (T \/ S)) by SYSREL:20
                               .= ((R * T) \/ (R * S)) \/ (S * (T \/ S))
                                                                by RELAT_1:51
                               .= ((R * T) \/ (R * S)) \/ ((S * T) \/ (S * S))
                                                                by RELAT_1:51
                               .= ({} \/ R) \/ ({} \/ S) by A6,A7,A8,Th16
                               .=f_escape(M) by Def19;
  hence thesis;
 end;
 A9:(f_entrance(M)) * (f_entrance(M)) = f_entrance(M)
 proof
  set R = ((the Flow of M)~|(the Places of M));
  A10: S * R = {} by Th17;
  A11: R * S = R by Th17;
  A12: S * S = S by SYSREL:29;
    (f_entrance(M)) * (f_entrance(M)) = (R \/ S) * (f_entrance(M)) by Def18
                               .= (R \/ S) * (R \/ S) by Def18
                               .= (R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
                               .= ((R * R) \/ (R * S)) \/ (S * (R \/ S))
                                                                by RELAT_1:51
                               .= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S))
                                                                by RELAT_1:51
                               .= ({} \/ R) \/ ({} \/ S) by A10,A11,A12,Th16
                               .=f_entrance(M) by Def18;
  hence thesis;
 end;
   (f_entrance(M)) * (f_escape(M)) = f_entrance(M)
 proof
  set T = ((the Flow of M)~|(the Places of M));
  A13: T * S = T by Th17;
  A14: S * R = {} by Th17;
  A15: S * S = S by SYSREL:29;
    (f_entrance(M)) * (f_escape(M)) = (T \/ S) * (f_escape(M)) by Def18
                               .= (T \/ S) * (R \/ S) by Def19
                               .= (T * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
                               .= ((T * R) \/ (T * S)) \/ (S * (R \/ S))
                                                                by RELAT_1:51
                               .= ((T * R) \/ (T * S)) \/ ((S * R) \/ (S * S))
                                                                by RELAT_1:51
                               .= ({} \/ T) \/ ({} \/ S) by A13,A14,A15,Th16
                               .=f_entrance(M) by Def18;
  hence thesis;
 end;
 hence thesis by A1,A5,A9;
end;

theorem
          (f_escape(M)) * (f_escape(M) \ id(Elements(M))) = {} &
          (f_entrance(M)) * (f_entrance(M) \ id(Elements(M))) = {}
proof
 set R = (the Flow of M)|(the Places of M);
 set S = id(the Transitions of M);
 thus (f_escape(M)) * (f_escape(M) \ id(Elements(M))) = {}
 proof
  A1: S * R = {} by Th17;
    (f_escape(M)) * (f_escape(M) \ id(Elements(M))) =
                       (R \/ S) * (f_escape(M) \ id(Elements(M)))
                                                            by Def19
                    .= (R \/ S) * ((R \/ S) \ (id(Elements(M)))) by Def19
                    .= (R \/ S) * R by Th19
                    .= (R * R) \/ (S * R) by SYSREL:20
                    .= {} by A1,Th16;
  hence thesis;
 end;
  set R = ((the Flow of M)~|(the Places of M));
  A2: S * R = {} by Th17;
    (f_entrance(M)) * (f_entrance(M) \ id(Elements(M))) =
                       (R \/ S) * (f_entrance(M) \ id(Elements(M)))
                                               by Def18
                    .= (R \/ S) * ((R \/ S) \ (id(Elements(M)))) by Def18
                    .= (R \/ S) * R by Th19
                    .= (R * R) \/ (S * R) by SYSREL:20
                    .= {} by A2,Th16;
  hence thesis;
end;

::B [F ->R]
definition let M;
 func f_adjac(M) -> Relation equals
:Def20: ((the Flow of M)|(the Transitions of M) \/
                        (the Flow of M)~|(the Transitions of M)) \/
                                              id(the Transitions of M);
 correctness;

 redefine func f_flow(M);
  synonym f_circulation(M);
end;

theorem
          f_adjac(M) * f_adjac(M) = f_adjac(M) &
         (f_adjac(M) \ id(Elements(M))) * f_adjac(M) = {} &
           (f_adjac(M) \/ ((f_adjac(M))~)) \/ id(Elements(M)) =
                                         f_circulation(M) \/
 (f_circulation(M))~
proof
 set R = (the Flow of M)|(the Transitions of M);
 set S = (the Flow of M)~|(the Transitions of M);
 set T = id(the Transitions of M);
 set Q = id(Elements(M));
 A1:((R \/ S) \/ T) \ Q = R \/ S
 proof
    ((R \/ S) \/ T) \ Q = ((R \/ T) \/ (S \/ T)) \ Q by XBOOLE_1:5
                   .= ((R \/ T) \ (id(Elements(M))) \/
                       ((S \/ T) \ (id(Elements(M))))) by XBOOLE_1:42
                   .= R \/
                       ((S \/ T) \ (id(Elements(M)))) by Th19
                   .= R \/ S by Th19;
  hence thesis;
 end;
 A2:(R \/ S) * (R \/ S) = {}
 proof
    (R \/ S) * (R \/ S) = ((R \/ S) * R) \/ ((R \/ S) *S) by SYSREL:20
                   .= ((R * R) \/ (S * R)) \/ ((R \/ S) *S) by SYSREL:20
                   .= ((R * R) \/ (S * R)) \/ ((R * S) \/ (S *S)) by SYSREL:20
                   .= ({} \/ (S * R)) \/ ((R * S) \/ (S *S)) by Th16
                   .= ({} \/ {}) \/ ((R * S) \/ (S *S)) by Th16
                   .= ({} \/ {}) \/ ({} \/ (S *S)) by Th16
                   .= {} by Th16;
  hence thesis;
 end;
 A3:R \/ S~ = the Flow of M & R~ \/ S = (the Flow of M)~
 proof
  A4:R \/ S~ = R \/ (((the Flow of M)|(the Places of M))~)~ by Th20
          .= the Flow of M by Th21;
    R~ \/ S = R~ \/ ((the Flow of M)|(the Places of M))~ by Th20
        .= (the Flow of M)~ by Th21;
  hence thesis by A4;
 end;
 A5:(R \/ S)~ \/ (R \/ S) = (the Flow of M) \/ (the Flow of M)~
 proof
    (R \/ S)~ \/ (R \/ S) = (R~ \/ S~) \/ (R \/ S) by RELAT_1:40
                      .= (R~ \/ (S \/ R)) \/ S~ by XBOOLE_1:4
                      .= ((R~ \/ S) \/ R) \/ S~ by XBOOLE_1:4
                  .= (the Flow of M) \/ (the Flow of M)~ by A3,XBOOLE_1:4;
  hence thesis;
 end;
 A6:f_adjac(M) \/ (f_adjac(M))~ =
      ((the Flow of M) \/ (the Flow of M)~) \/ id(the Transitions of M)
 proof
    f_adjac(M) \/ (f_adjac(M))~ = ((R \/ S) \/ T) \/ (f_adjac(M))~ by Def20
                     .= ((R \/ S) \/ T) \/ ((R \/ S) \/ T)~ by Def20
                     .= ((R \/ S) \/ T) \/ ((R \/ S)~ \/ T~) by RELAT_1:40
                     .= (((R \/ S) \/ T) \/ (R \/ S)~) \/ T~ by XBOOLE_1:4
                     .= (((R \/ S) \/ (R \/ S)~) \/ T) \/ T~ by XBOOLE_1:4
                     .= ((R \/ S) \/ (R \/ S)~) \/ (T \/ T~) by XBOOLE_1:4
                     .= ((R \/ S) \/ (R \/ S)~) \/ (T \/ T) by RELAT_1:72
                     .= ((the Flow of M) \/ (the Flow of M)~) \/
                         id(the Transitions of M) by A5;
  hence thesis;
 end;
 A7:id(the Transitions of M) c= id(Elements(M))
 proof
    the Transitions of M c= Elements(M) by NET_1:5;
  hence thesis by SYSREL:33;
 end;
 A8:f_adjac(M) * f_adjac(M) = f_adjac(M) * ((R \/ S) \/ T) by Def20

   .= (((R \/ S) \/ T) * ((R \/ S) \/ T)) by Def20
   .= (((R \/ S) \/ T) * (R \/ S)) \/ (((R \/ S) \/ T) * T) by SYSREL:20
   .= ((((R \/ S) \/ T) * R ) \/ (((R \/ S) \/ T) * S)) \/
                            (((R \/ S) \/ T) * T) by SYSREL:20
   .= (((R \/ S) * R ) \/ (T * R )) \/ (((R \/ S) \/ T) * S) \/
                              (((R \/ S) \/ T) * T) by SYSREL:20
   .= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R \/ S) \/ T) * S) \/
                              (((R \/ S) \/ T) * T) by SYSREL:20
   .= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R \/ S) * S) \/ (T * S)) \/
                              (((R \/ S) \/ T) * T) by SYSREL:20
   .= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S))
\/
                              (((R \/ S) \/ T) * T) by SYSREL:20
   .= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S))
\/
                              (((R \/ S) * T) \/ (T * T)) by SYSREL:20
   .= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S))
\/
                              (((R * T) \/ (S * T)) \/ (T * T)) by SYSREL:20
   .= (({} \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S)) \/
                              (((R * T) \/ (S * T)) \/ (T * T)) by Th16
   .= (({} \/ {}) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S)) \/
                              (((R * T) \/ (S * T)) \/ (T * T)) by Th16
   .= (({} \/ {}) \/ (T * R )) \/ (({} \/ (S * S)) \/ (T * S)) \/
                              (((R * T) \/ (S * T)) \/ (T * T)) by Th16
   .= (T * R ) \/ ({} \/ (T * S)) \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th16
   .= R \/ (T * S) \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th17
   .= R \/ S \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th17
   .= R \/ S \/ (((R * T) \/ (S * T)) \/ T) by SYSREL:29
   .= R \/ S \/ (({} \/ (S * T)) \/ T) by Th17
   .= R \/ S \/ ({} \/ T) by Th17
   .= f_adjac(M) by Def20;

 A9: (f_adjac(M) \ id(Elements(M))) * f_adjac(M) =
     (f_adjac(M) \ id(Elements(M))) * ((R \/ S) \/ T) by Def20
   .= (R \/ S) * ((R \/ S) \/ T) by A1,Def20
   .= {} \/ ((R \/ S) * T) by A2,SYSREL:20
   .= (R * T) \/ (S * T) by SYSREL:20
   .= {} \/ (S * T) by Th17
   .= {} by Th17;

    (f_adjac(M) \/ (f_adjac(M))~) \/ id(Elements(M)) =
(((the Flow of M) \/ (the Flow of M)~) \/
         (id(the Transitions of M) \/ id(Elements(M)))) by A6,XBOOLE_1:4
    .= (((the Flow of M) \/ (the Flow of M)~) \/ id(Elements(M)))
                                                          by A7,XBOOLE_1:12
    .= ((the Flow of M) \/ id(Elements(M))) \/
                    ((the Flow of M)~ \/ id(Elements(M))) by XBOOLE_1:5
    .= ((the Flow of M) \/ id(Elements(M))) \/
                 ((the Flow of M)~ \/ (id(Elements(M)))~) by RELAT_1:72
    .= ((the Flow of M) \/ id(Elements(M))) \/
                 ((the Flow of M) \/ id(Elements(M)))~ by RELAT_1:40
    .= f_circulation(M) \/
                 ((the Flow of M) \/ id(Elements(M)))~ by Def13
    .= f_circulation(M) \/ (f_circulation(M))~ by Def13;
  hence thesis by A8,A9;
 end;

Back to top