e_siec.miz



    begin

    reserve x,y,z for object,

X,Y for set;

    definition

      struct ( 1-sorted) G_Net (# the carrier -> set,

the entrance, escape -> Relation #)

       attr strict strict;

    end

    definition

      let IT be G_Net;

      :: E_SIEC:def1

      attr IT is GG means

      : Def1: 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

    registration

      cluster GG for G_Net;

      existence

      proof

        take N = G_Net (# {} , {} , {} #);

        the escape of N c= [:the carrier of N, the carrier of N:] & (the entrance of N * the entrance of N) = {} by XBOOLE_1: 2;

        hence thesis;

      end;

    end

    definition

      mode gg_net is GG G_Net;

    end

    definition

      let IT be G_Net;

      :: E_SIEC:def2

      attr IT is EE means

      : Def2: (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

    registration

      cluster EE for G_Net;

      existence

      proof

        take N = G_Net (# {} , {} , {} #);

        thus thesis;

      end;

    end

    registration

      cluster strict GG EE for G_Net;

      existence

      proof

        take N = G_Net (# {} , {} , {} #);

        the entrance of N c= [:the carrier of N, the carrier of N:] & (the escape of N * (the escape of N \ ( id N))) = {} by XBOOLE_1: 2;

        hence thesis;

      end;

    end

    definition

      mode e_net is EE GG G_Net;

    end

    reserve N for e_net;

    theorem :: E_SIEC:1

    for R,S be 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))) = {} by Def1, Def2;

    theorem :: E_SIEC:2

    

     Th2: G_Net (# X, {} , {} #) is e_net

    proof

       {} c= [:X, X:] & ( {} * ( {} \ ( id X))) = {} by XBOOLE_1: 2;

      hence thesis by Def1, Def2;

    end;

    theorem :: E_SIEC:3

    

     Th3: G_Net (# X, ( id X), ( id X) #) is e_net

    proof

      

       A1: (( id X) * (( id X) \ ( id X))) = (( id X) * {} ) by XBOOLE_1: 37

      .= {} ;

      ( id X) c= [:X, X:] & (( id X) * ( id X)) = ( id X) by RELSET_1: 13, SYSREL: 12;

      hence thesis by A1, Def1, Def2;

    end;

    theorem :: E_SIEC:4

     G_Net (# {} , {} , {} #) is e_net by Th2;

    theorem :: E_SIEC:5

     G_Net (# X, ( id (X \ Y)), ( id (X \ Y)) #) is e_net

    proof

      

       A1: (( id (X \ Y)) * (( id (X \ Y)) \ ( id X))) = (( id (X \ Y)) * {} ) by SYSREL: 16

      .= {} ;

      (X \ Y) c= X by XBOOLE_1: 36;

      then

       A2: [:(X \ Y), (X \ Y):] c= [:X, X:] by ZFMISC_1: 96;

      ( id (X \ Y)) c= [:(X \ Y), (X \ Y):] by RELSET_1: 13;

      then

       A3: ( id (X \ Y)) c= [:X, X:] by A2, XBOOLE_1: 1;

      (( id (X \ Y)) * ( id (X \ Y))) = ( id (X \ Y)) by SYSREL: 12;

      hence thesis by A3, A1, Def1, Def2;

    end;

    definition

      :: E_SIEC:def3

      func empty_e_net -> strict e_net equals G_Net (# {} , {} , {} #);

      correctness by Th2;

    end

    definition

      let X;

      :: E_SIEC:def4

      func Tempty_e_net X -> strict e_net equals G_Net (# X, ( id X), ( id X) #);

      coherence by Th3;

      :: E_SIEC:def5

      func Pempty_e_net (X) -> strict e_net equals G_Net (# X, {} , {} #);

      coherence by Th2;

    end

    theorem :: E_SIEC:6

    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:7

    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;

      :: E_SIEC:def6

      func Psingle_e_net (x) -> strict e_net equals G_Net (# {x}, ( id {x}), ( id {x}) #);

      coherence by Th3;

      :: E_SIEC:def7

      func Tsingle_e_net (x) -> strict e_net equals G_Net (# {x}, {} , {} #);

      coherence by Th2;

    end

    theorem :: E_SIEC:8

    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:9

    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:10

    

     Th10: G_Net (# (X \/ Y), ( id X), ( id X) #) is e_net

    proof

      X c= (X \/ Y) by XBOOLE_1: 7;

      then ( id X) c= [:X, X:] & [:X, X:] c= [:(X \/ Y), (X \/ Y):] by RELSET_1: 13, ZFMISC_1: 96;

      then

       A1: ( id X) c= [:(X \/ Y), (X \/ Y):] by XBOOLE_1: 1;

      ( id X) c= (( id X) \/ ( id Y)) by XBOOLE_1: 7;

      then ( id X) c= ( id (X \/ Y)) by SYSREL: 14;

      

      then

       A2: (( id X) * (( id X) \ ( id (X \/ Y)))) = (( id X) * {} ) by XBOOLE_1: 37

      .= {} ;

      (( id X) * ( id X)) = ( id X) by SYSREL: 12;

      hence thesis by A1, A2, Def1, Def2;

    end;

    definition

      let X, Y;

      :: E_SIEC:def8

      func PTempty_e_net (X,Y) -> strict e_net equals G_Net (# (X \/ Y), ( id X), ( id X) #);

      coherence by Th10;

    end

    theorem :: E_SIEC:11

    

     Th11: (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))

    proof

      the entrance of N c= [:the carrier of N, the carrier of N:] & the escape of N c= [:the carrier of N, the carrier of N:] by Def1;

      hence thesis by SYSREL: 20;

    end;

    theorem :: E_SIEC:12

    

     Th12: ( CL the entrance of N) = ( CL the escape of N)

    proof

      (the escape of N * (the escape of N \ ( id N))) = {} by Def2;

      then

       A1: (the escape of N * (the escape of N \ ( id ( dom the escape of N)))) = {} by Th11;

      (the entrance of N * (the entrance of N \ ( id N))) = {} by Def2;

      then

       A2: (the entrance of N * (the entrance of N \ ( id ( dom the entrance of N)))) = {} by Th11;

      (the entrance of N * the escape of N) = the entrance of N & (the escape of N * the entrance of N) = the escape of N by Def1;

      hence thesis by A1, A2, SYSREL: 40;

    end;

    theorem :: E_SIEC:13

    

     Th13: ( 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)

    proof

      (the entrance of N * (the entrance of N \ ( id the carrier of N))) = {} by Def2;

      then

       A1: (the entrance of N * (the entrance of N \ ( id ( dom the entrance of N)))) = {} by Th11;

      (the escape of N * (the escape of N \ ( id the carrier of N))) = {} by Def2;

      then

       A2: (the escape of N * (the escape of N \ ( id ( dom the escape of N)))) = {} by Th11;

      

       A3: (the escape of N * the escape of N) = the escape of N by Def1;

      then

       A4: ( rng the escape of N) = ( rng ( CL the escape of N)) by A2, SYSREL: 31;

      

       A5: (the entrance of N * the entrance of N) = the entrance of N by Def1;

      then ( rng the entrance of N) = ( rng ( CL the entrance of N)) by A1, SYSREL: 31;

      hence thesis by A5, A1, A3, A2, A4, Th12, SYSREL: 31;

    end;

    theorem :: E_SIEC:14

    

     Th14: ( 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

    proof

      the entrance of N c= [:the carrier of N, the carrier of N:] & the escape of N c= [:the carrier of N, the carrier of N:] by Def1;

      hence thesis by SYSREL: 3;

    end;

    theorem :: E_SIEC:15

    

     Th15: (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))) = {}

    proof

      set R = the entrance of N;

      set S = the escape of N;

      set T = ( id the carrier of N);

      

       A1: (S * (R \ T)) = (S * (R \ ( id ( dom R)))) by Th11

      .= ((S * R) * (R \ ( id ( dom R)))) by Def1

      .= (S * (R * (R \ ( id ( dom R))))) by RELAT_1: 36

      .= (S * (R * (R \ T))) by Th11

      .= (S * {} ) by Def2

      .= {} ;

      (R * (S \ T)) = (R * (S \ ( id ( dom S)))) by Th11

      .= ((R * S) * (S \ ( id ( dom S)))) by Def1

      .= (R * (S * (S \ ( id ( dom S))))) by RELAT_1: 36

      .= (R * (S * (S \ T))) by Th11

      .= (R * {} ) by Def2

      .= {} ;

      hence thesis by A1;

    end;

    theorem :: E_SIEC:16

    ((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))) = {}

    proof

      set R = the entrance of N;

      set S = the escape of N;

      set T = ( id the carrier of N);

      ((R \ T) * (S \ T)) c= (R * (S \ T)) by RELAT_1: 30, XBOOLE_1: 36;

      then

       A1: ((R \ T) * (S \ T)) c= {} by Th15;

      ((S \ T) * (S \ T)) c= (S * (S \ T)) by RELAT_1: 30, XBOOLE_1: 36;

      then

       A2: ((S \ T) * (S \ T)) c= {} by Def2;

      ((S \ T) * (R \ T)) c= (S * (R \ T)) by RELAT_1: 30, XBOOLE_1: 36;

      then

       A3: ((S \ T) * (R \ T)) c= {} by Th15;

      ((R \ T) * (R \ T)) c= (R * (R \ T)) by RELAT_1: 30, XBOOLE_1: 36;

      then ((R \ T) * (R \ T)) c= {} by Def2;

      hence thesis by A1, A2, A3, XBOOLE_1: 3;

    end;

    definition

      let N;

      :: E_SIEC:def9

      func e_Places (N) -> set equals ( rng the entrance of N);

      correctness ;

    end

    definition

      let N;

      :: E_SIEC:def10

      func e_Transitions (N) -> set equals (the carrier of N \ ( e_Places N));

      correctness ;

    end

    theorem :: E_SIEC:17

    

     Th17: ( [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)

    proof

      

       A1: [x, y] in the escape of N & x <> y implies x in ( e_Transitions N) & y in ( e_Places N)

      proof

        (the escape of N * (the escape of N \ ( id the carrier of N))) = {} by Def2;

        then

         A2: (the escape of N * (the escape of N \ ( id ( dom the escape of N)))) = {} by Th11;

        ( dom the escape of N) c= the carrier of N by Th14;

        then

         A3: (( dom the escape of N) \ ( dom ( CL the escape of N))) c= (the carrier of N \ ( dom ( CL the escape of N))) by XBOOLE_1: 33;

        assume

         A4: [x, y] in the escape of N & x <> y;

        

         A5: (the escape of N * the escape of N) = the escape of N by Def1;

        then x in (( dom the escape of N) \ ( dom ( CL the escape of N))) by A4, A2, SYSREL: 30;

        then x in (the carrier of N \ ( dom ( CL the escape of N))) by A3;

        then

         A6: x in (the carrier of N \ ( rng the escape of N)) by Th13;

        y in ( dom ( CL the escape of N)) by A4, A5, A2, SYSREL: 30;

        then y in ( rng the escape of N) by Th13;

        hence thesis by A6, Th13;

      end;

       [x, y] in the entrance of N & x <> y implies x in ( e_Transitions N) & y in ( e_Places N)

      proof

        (the entrance of N * (the entrance of N \ ( id the carrier of N))) = {} by Def2;

        then

         A7: (the entrance of N * (the entrance of N \ ( id ( dom the entrance of N)))) = {} by Th11;

        ( dom the entrance of N) c= the carrier of N by Th14;

        then

         A8: (( dom the entrance of N) \ ( dom ( CL the entrance of N))) c= (the carrier of N \ ( dom ( CL the entrance of N))) by XBOOLE_1: 33;

        assume

         A9: [x, y] in the entrance of N & x <> y;

        

         A10: (the entrance of N * the entrance of N) = the entrance of N by Def1;

        then x in (( dom the entrance of N) \ ( dom ( CL the entrance of N))) by A9, A7, SYSREL: 30;

        then

         A11: x in (the carrier of N \ ( dom ( CL the entrance of N))) by A8;

        y in ( dom ( CL the entrance of N)) by A9, A10, A7, SYSREL: 30;

        hence thesis by A11, Th13;

      end;

      hence thesis by A1;

    end;

    theorem :: E_SIEC:18

    

     Th18: (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):]

    proof

      

       A1: for x,y be object holds [x, y] in (the entrance of N \ ( id the carrier of N)) implies [x, y] in [:( e_Transitions N), ( e_Places N):]

      proof

        let x,y be object;

        assume

         A2: [x, y] in (the entrance of N \ ( id the carrier of N));

        then [x, y] in the entrance of N by XBOOLE_0:def 5;

        then

         A3: x in ( dom the entrance of N) by XTUPLE_0:def 12;

         not [x, y] in ( id the carrier of N) by A2, XBOOLE_0:def 5;

        then

         A4: not x in the carrier of N or x <> y by RELAT_1:def 10;

        

         A5: [x, y] in the entrance of N by A2, XBOOLE_0:def 5;

        then

         A6: y in ( e_Places N) by XTUPLE_0:def 13;

        ( dom the entrance of N) c= the carrier of N by Th14;

        then x in ( e_Transitions N) by A5, A4, A3, Th17;

        hence thesis by A6, ZFMISC_1: 87;

      end;

      for x,y be object holds [x, y] in (the escape of N \ ( id the carrier of N)) implies [x, y] in [:( e_Transitions N), ( e_Places N):]

      proof

        let x,y be object;

        

         A7: ( dom the escape of N) c= the carrier of N by Th14;

        assume

         A8: [x, y] in (the escape of N \ ( id the carrier of N));

        then [x, y] in the escape of N by XBOOLE_0:def 5;

        then

         A9: x in ( dom the escape of N) by XTUPLE_0:def 12;

         not [x, y] in ( id the carrier of N) by A8, XBOOLE_0:def 5;

        then

         A10: not x in the carrier of N or x <> y by RELAT_1:def 10;

         [x, y] in the escape of N by A8, XBOOLE_0:def 5;

        then x in ( e_Transitions N) & y in ( e_Places N) by A10, A9, A7, Th17;

        hence thesis by ZFMISC_1: 87;

      end;

      hence thesis by A1, RELAT_1:def 3;

    end;

    definition

      let N;

      :: E_SIEC:def11

      func e_Flow N -> Relation equals (((the entrance of N ~ ) \/ the escape of N) \ ( id N));

      correctness ;

    end

    theorem :: E_SIEC:19

    ( e_Flow N) c= ( [:( e_Places N), ( e_Transitions N):] \/ [:( e_Transitions N), ( e_Places N):])

    proof

      

       A1: ((the entrance of N ~ ) \ ( id N)) = ((the entrance of N ~ ) \ (( id the carrier of N) ~ ))

      .= ((the entrance of N \ ( id the carrier of N)) ~ ) by RELAT_1: 24;

      

       A2: ( e_Flow 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)) c= [:( e_Transitions N), ( e_Places N):] by Th18, XBOOLE_1: 42;

      (the entrance of N \ ( id the carrier of N)) c= [:( e_Transitions N), ( e_Places N):] by Th18;

      then ((the entrance of N ~ ) \ ( id the carrier of N)) c= [:( e_Places N), ( e_Transitions N):] by A1, SYSREL: 4;

      hence thesis by A2, XBOOLE_1: 13;

    end;

    definition

      let N;

      :: E_SIEC:def12

      func e_pre (N) -> Relation equals (the entrance of N \ ( id the carrier of N));

      correctness ;

      :: E_SIEC:def13

      func e_post (N) -> Relation equals (the escape of N \ ( id the carrier of N));

      correctness ;

    end

    theorem :: E_SIEC:20

    ( e_pre N) c= [:( e_Transitions N), ( e_Places N):] & ( e_post N) c= [:( e_Transitions N), ( e_Places N):] by Th18;

    definition

      let N;

      :: E_SIEC:def14

      func e_shore (N) -> set equals the carrier of N;

      correctness ;

      :: E_SIEC:def15

      func e_prox (N) -> Relation equals ((the entrance of N \/ the escape of N) ~ );

      correctness ;

      :: E_SIEC:def16

      func e_flow (N) -> Relation equals (((the entrance of N ~ ) \/ the escape of N) \/ ( id the carrier of N));

      correctness ;

    end

    theorem :: E_SIEC:21

    ( e_prox N) c= [:( e_shore N), ( e_shore N):] & ( e_flow N) c= [:( e_shore N), ( e_shore N):]

    proof

      

       A1: ( id the carrier of N) c= [:the carrier of N, the carrier of N:] by RELSET_1: 13;

      

       A2: the escape of N c= [:the carrier of N, the carrier of N:] by Def1;

      

       A3: the entrance of N c= [:the carrier of N, the carrier of N:] by Def1;

      then (the entrance of N ~ ) c= [:the carrier of N, the carrier of N:] by SYSREL: 4;

      then

       A4: ((the entrance of N ~ ) \/ the escape of N) c= [:the carrier of N, the carrier of N:] by A2, XBOOLE_1: 8;

      (the entrance of N \/ the escape of N) c= [:the carrier of N, the carrier of N:] by A3, A2, XBOOLE_1: 8;

      hence thesis by A4, A1, SYSREL: 4, XBOOLE_1: 8;

    end;

    theorem :: E_SIEC:22

    (( 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) ~ ))

    proof

      set R = the entrance of N;

      set S = the escape of N;

      set T = ( id the carrier of N);

      

       A1: ((( e_prox N) \/ (( e_prox N) ~ )) \/ ( id ( e_shore N))) = ((((R ~ ) \/ (S ~ )) \/ (S \/ R)) \/ T) by RELAT_1: 23

      .= (((((R ~ ) \/ (S ~ )) \/ S) \/ R) \/ T) by XBOOLE_1: 4

      .= ((((R ~ ) \/ ((S ~ ) \/ S)) \/ R) \/ T) by XBOOLE_1: 4

      .= (((R ~ ) \/ ((S \/ (S ~ )) \/ R)) \/ T) by XBOOLE_1: 4

      .= (((R ~ ) \/ (S \/ ((S ~ ) \/ R))) \/ T) by XBOOLE_1: 4

      .= ((((R ~ ) \/ S) \/ ((S ~ ) \/ R)) \/ T) by XBOOLE_1: 4

      .= (( e_flow N) \/ (((S ~ ) \/ ((R ~ ) ~ )) \/ T)) by XBOOLE_1: 5

      .= (( e_flow N) \/ ((((R ~ ) \/ S) ~ ) \/ T)) by RELAT_1: 23

      .= (( e_flow N) \/ ((((R ~ ) \/ S) ~ ) \/ (T ~ )))

      .= (( e_flow N) \/ (( e_flow N) ~ )) by RELAT_1: 23;

      

       A2: ((( e_prox N) \ T) * ( e_prox N)) = ((((R ~ ) \/ (S ~ )) \ T) * ((R \/ S) ~ )) by RELAT_1: 23

      .= ((((R ~ ) \ T) \/ ((S ~ ) \ T)) * ((R \/ S) ~ )) by XBOOLE_1: 42

      .= ((((R ~ ) \ T) \/ ((S ~ ) \ T)) * ((R ~ ) \/ (S ~ ))) by RELAT_1: 23

      .= (((((R ~ ) \ T) \/ ((S ~ ) \ T)) * (R ~ )) \/ ((((R ~ ) \ T) \/ ((S ~ ) \ T)) * (S ~ ))) by RELAT_1: 32

      .= (((((R ~ ) \ T) * (R ~ )) \/ (((S ~ ) \ T) * (R ~ ))) \/ ((((R ~ ) \ T) \/ ((S ~ ) \ T)) * (S ~ ))) by SYSREL: 6

      .= (((((R ~ ) \ T) * (R ~ )) \/ (((S ~ ) \ T) * (R ~ ))) \/ ((((R ~ ) \ T) * (S ~ )) \/ (((S ~ ) \ T) * (S ~ )))) by SYSREL: 6

      .= (((((R ~ ) \ (T ~ )) * (R ~ )) \/ (((S ~ ) \ T) * (R ~ ))) \/ ((((R ~ ) \ T) * (S ~ )) \/ (((S ~ ) \ T) * (S ~ ))))

      .= (((((R ~ ) \ (T ~ )) * (R ~ )) \/ (((S ~ ) \ (T ~ )) * (R ~ ))) \/ ((((R ~ ) \ T) * (S ~ )) \/ (((S ~ ) \ T) * (S ~ ))))

      .= (((((R ~ ) \ (T ~ )) * (R ~ )) \/ (((S ~ ) \ (T ~ )) * (R ~ ))) \/ ((((R ~ ) \ (T ~ )) * (S ~ )) \/ (((S ~ ) \ T) * (S ~ ))))

      .= (((((R ~ ) \ (T ~ )) * (R ~ )) \/ (((S ~ ) \ (T ~ )) * (R ~ ))) \/ ((((R ~ ) \ (T ~ )) * (S ~ )) \/ (((S ~ ) \ (T ~ )) * (S ~ ))))

      .= (((((R \ T) ~ ) * (R ~ )) \/ (((S ~ ) \ (T ~ )) * (R ~ ))) \/ ((((R ~ ) \ (T ~ )) * (S ~ )) \/ (((S ~ ) \ (T ~ )) * (S ~ )))) by RELAT_1: 24

      .= (((((R \ T) ~ ) * (R ~ )) \/ (((S \ T) ~ ) * (R ~ ))) \/ ((((R ~ ) \ (T ~ )) * (S ~ )) \/ (((S ~ ) \ (T ~ )) * (S ~ )))) by RELAT_1: 24

      .= (((((R \ T) ~ ) * (R ~ )) \/ (((S \ T) ~ ) * (R ~ ))) \/ ((((R \ T) ~ ) * (S ~ )) \/ (((S ~ ) \ (T ~ )) * (S ~ )))) by RELAT_1: 24

      .= (((((R \ T) ~ ) * (R ~ )) \/ (((S \ T) ~ ) * (R ~ ))) \/ ((((R \ T) ~ ) * (S ~ )) \/ (((S \ T) ~ ) * (S ~ )))) by RELAT_1: 24

      .= ((((R * (R \ T)) ~ ) \/ (((S \ T) ~ ) * (R ~ ))) \/ ((((R \ T) ~ ) * (S ~ )) \/ (((S \ T) ~ ) * (S ~ )))) by RELAT_1: 35

      .= ((((R * (R \ T)) ~ ) \/ ((R * (S \ T)) ~ )) \/ ((((R \ T) ~ ) * (S ~ )) \/ (((S \ T) ~ ) * (S ~ )))) by RELAT_1: 35

      .= ((((R * (R \ T)) ~ ) \/ ((R * (S \ T)) ~ )) \/ (((S * (R \ T)) ~ ) \/ (((S \ T) ~ ) * (S ~ )))) by RELAT_1: 35

      .= ((((R * (R \ T)) ~ ) \/ ((R * (S \ T)) ~ )) \/ (((S * (R \ T)) ~ ) \/ ((S * (S \ T)) ~ ))) by RELAT_1: 35

      .= ((( {} ~ ) \/ ((R * (S \ T)) ~ )) \/ (((S * (R \ T)) ~ ) \/ ((S * (S \ T)) ~ ))) by Def2

      .= ((( {} ~ ) \/ ((R * (S \ T)) ~ )) \/ (((S * (R \ T)) ~ ) \/ ( {} ~ ))) by Def2

      .= ((( {} ~ ) \/ ( {} ~ )) \/ (((S * (R \ T)) ~ ) \/ ( {} ~ ))) by Th15

      .= {} by Th15;

      (( e_prox N) * ( e_prox N)) = (((R \/ S) * (R \/ S)) ~ ) by RELAT_1: 35

      .= ((((R \/ S) * R) \/ ((R \/ S) * S)) ~ ) by RELAT_1: 32

      .= ((((R * R) \/ (S * R)) \/ ((R \/ S) * S)) ~ ) by SYSREL: 6

      .= ((((R * R) \/ (S * R)) \/ ((R * S) \/ (S * S))) ~ ) by SYSREL: 6

      .= (((R \/ (S * R)) \/ ((R * S) \/ (S * S))) ~ ) by Def1

      .= (((R \/ S) \/ ((R * S) \/ (S * S))) ~ ) by Def1

      .= (((R \/ S) \/ (R \/ (S * S))) ~ ) by Def1

      .= (((R \/ S) \/ (R \/ S)) ~ ) by Def1

      .= ( e_prox N);

      hence thesis by A2, A1;

    end;

    theorem :: E_SIEC:23

    

     Th23: (( 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))

    proof

      set T = the entrance of N, C = the carrier of N;

      set E = the escape of N, I = ( id C);

      for x,y be object holds [x, y] in (E \ I) implies [x, y] in (( id (C \ ( rng E))) * (E \ I))

      proof

        let x,y be object;

        assume

         A1: [x, y] in (E \ I);

        then [x, y] in E by XBOOLE_0:def 5;

        then

         A2: x in ( dom E) by XTUPLE_0:def 12;

        

         A3: not x in ( rng E)

        proof

          assume x in ( rng E);

          then ex z be object st [z, x] in E by XTUPLE_0:def 13;

          then (E * (E \ I)) <> {} by A1, RELAT_1:def 8;

          hence thesis by Def2;

        end;

        ( dom E) c= C by Th14;

        then x in (C \ ( rng E)) by A2, A3, XBOOLE_0:def 5;

        then [x, x] in ( id (C \ ( rng E))) by RELAT_1:def 10;

        hence thesis by A1, RELAT_1:def 8;

      end;

      then

       A4: (E \ I) c= (( id (C \ ( rng E))) * (E \ I)) by RELAT_1:def 3;

      for x,y be object holds [x, y] in (T \ I) implies [x, y] in (( id (C \ ( rng T))) * (T \ I))

      proof

        let x,y be object;

        assume

         A5: [x, y] in (T \ I);

        then [x, y] in T by XBOOLE_0:def 5;

        then

         A6: x in ( dom T) by XTUPLE_0:def 12;

        

         A7: not x in ( rng T)

        proof

          assume x in ( rng T);

          then ex z be object st [z, x] in T by XTUPLE_0:def 13;

          then (T * (T \ I)) <> {} by A5, RELAT_1:def 8;

          hence thesis by Def2;

        end;

        ( dom T) c= C by Th14;

        then x in (C \ ( rng T)) by A6, A7, XBOOLE_0:def 5;

        then [x, x] in ( id (C \ ( rng T))) by RELAT_1:def 10;

        hence thesis by A5, RELAT_1:def 8;

      end;

      then

       A8: (T \ I) c= (( id (C \ ( rng T))) * (T \ I)) by RELAT_1:def 3;

      (( id (C \ ( rng E))) * (E \ I)) c= (E \ I) & (( id (C \ ( rng T))) * (T \ I)) c= (T \ I) by RELAT_1: 50;

      hence thesis by A4, A8, XBOOLE_0:def 10;

    end;

    theorem :: E_SIEC:24

    

     Th24: ((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))) = {}

    proof

      set T = the entrance of N, C = the carrier of N;

      set E = the escape of N, I = ( id C);

      ((T \ I) * (T \ I)) c= (T * (T \ I)) by RELAT_1: 30, XBOOLE_1: 36;

      then

       A1: ((T \ I) * (T \ I)) c= {} by Def2;

      ((E \ I) * (T \ I)) c= (E * (T \ I)) by RELAT_1: 30, XBOOLE_1: 36;

      then

       A2: ((E \ I) * (T \ I)) c= {} by Th15;

      ((T \ I) * (E \ I)) c= (T * (E \ I)) by RELAT_1: 30, XBOOLE_1: 36;

      then

       A3: ((T \ I) * (E \ I)) c= {} by Th15;

      ((E \ I) * (E \ I)) c= (E * (E \ I)) by RELAT_1: 30, XBOOLE_1: 36;

      then ((E \ I) * (E \ I)) c= {} by Def2;

      hence thesis by A1, A2, A3, XBOOLE_1: 3;

    end;

    theorem :: E_SIEC:25

    

     Th25: (((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)) ~ )) = {}

    proof

      

       A1: (((the entrance 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 entrance of N \ ( id the carrier of N))) ~ ) by RELAT_1: 35

      .= {} by Th24, RELAT_1: 43;

      (((the escape 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 escape of N \ ( id the carrier of N))) ~ ) by RELAT_1: 35

      .= {} by Th24, RELAT_1: 43;

      hence thesis by A1;

    end;

    theorem :: E_SIEC:26

    (((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)) ~ )

    proof

      

       A1: (((the entrance of N \ ( id the carrier of N)) ~ ) * (( id (the carrier of N \ ( rng the entrance of N))) ~ )) = ((( id (the carrier of N \ ( rng the entrance of N))) * (the entrance of N \ ( id the carrier of N))) ~ ) by RELAT_1: 35

      .= ((the entrance of N \ ( id the carrier of N)) ~ ) by Th23;

      (((the escape of N \ ( id the carrier of N)) ~ ) * (( id (the carrier of N \ ( rng the escape of N))) ~ )) = ((( id (the carrier of N \ ( rng the escape of N))) * (the escape of N \ ( id the carrier of N))) ~ ) by RELAT_1: 35

      .= ((the escape of N \ ( id the carrier of N)) ~ ) by Th23;

      hence thesis by A1;

    end;

    theorem :: E_SIEC:27

    

     Th27: ((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)))) = {}

    proof

      

       A1: for x,y be object holds not [x, y] in ((the entrance of N \ ( id the carrier of N)) * ( id (the carrier of N \ ( rng the entrance of N))))

      proof

        let x,y be object;

        assume [x, y] in ((the entrance of N \ ( id the carrier of N)) * ( id (the carrier of N \ ( rng the entrance of N))));

        then

        consider z be object such that

         A2: [x, z] in (the entrance of N \ ( id the carrier of N)) and

         A3: [z, y] in ( id (the carrier of N \ ( rng the entrance of N))) by RELAT_1:def 8;

        z in (the carrier of N \ ( rng the entrance of N)) by A3, RELAT_1:def 10;

        then

         A4: not z in ( rng the entrance of N) by XBOOLE_0:def 5;

         [x, z] in the entrance of N by A2, XBOOLE_0:def 5;

        hence thesis by A4, XTUPLE_0:def 13;

      end;

      for x,y be object holds not [x, y] in ((the escape of N \ ( id the carrier of N)) * ( id (the carrier of N \ ( rng the escape of N))))

      proof

        let x,y be object;

        assume [x, y] in ((the escape of N \ ( id the carrier of N)) * ( id (the carrier of N \ ( rng the escape of N))));

        then

        consider z be object such that

         A5: [x, z] in (the escape of N \ ( id the carrier of N)) and

         A6: [z, y] in ( id (the carrier of N \ ( rng the escape of N))) by RELAT_1:def 8;

        z in (the carrier of N \ ( rng the escape of N)) by A6, RELAT_1:def 10;

        then

         A7: not z in ( rng the escape of N) by XBOOLE_0:def 5;

         [x, z] in the escape of N by A5, XBOOLE_0:def 5;

        hence thesis by A7, XTUPLE_0:def 13;

      end;

      hence thesis by A1, RELAT_1: 37;

    end;

    theorem :: E_SIEC:28

    

     Th28: (( 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)) ~ )) = {}

    proof

      

       A1: (( id (the carrier of N \ ( rng the entrance 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)) ~ ))

      .= (((the entrance of N \ ( id the carrier of N)) * ( id (the carrier of N \ ( rng the entrance of N)))) ~ ) by RELAT_1: 35

      .= {} by Th27, RELAT_1: 43;

      (( 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 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 escape of N)))) ~ ) by RELAT_1: 35

      .= {} by Th27, RELAT_1: 43;

      hence thesis by A1;

    end;

    definition

      let N;

      :: E_SIEC:def17

      func e_entrance (N) -> Relation equals (((the escape of N \ ( id the carrier of N)) ~ ) \/ ( id (the carrier of N \ ( rng the escape of N))));

      correctness ;

      :: E_SIEC:def18

      func e_escape (N) -> Relation equals (((the entrance of N \ ( id the carrier of N)) ~ ) \/ ( id (the carrier of N \ ( rng the entrance of N))));

      correctness ;

    end

    theorem :: E_SIEC:29

    (( 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)

    proof

      set P = (the escape of N \ ( id the carrier of N));

      set Q = (the entrance of N \ ( id the carrier of N));

      set S = ( id (the carrier of N \ ( rng the entrance of N)));

      set T = ( id (the carrier of N \ ( rng the escape of N)));

      

       A1: (( e_entrance N) * ( e_entrance N)) = (((P ~ ) * ((P ~ ) \/ T)) \/ (T * ((P ~ ) \/ T))) by SYSREL: 6

      .= ((((P ~ ) * (P ~ )) \/ ((P ~ ) * T)) \/ (T * ((P ~ ) \/ T))) by RELAT_1: 32

      .= ((((P ~ ) * (P ~ )) \/ ((P ~ ) * T)) \/ ((T * (P ~ )) \/ (T * T))) by RELAT_1: 32

      .= ((((P * P) ~ ) \/ ((P ~ ) * T)) \/ ((T * (P ~ )) \/ (T * T))) by RELAT_1: 35

      .= ((((P * P) ~ ) \/ ((P ~ ) * (T ~ ))) \/ ((T * (P ~ )) \/ (T * T)))

      .= ((((P * P) ~ ) \/ ((P ~ ) * (T ~ ))) \/ (((T ~ ) * (P ~ )) \/ (T * T)))

      .= ((((P * P) ~ ) \/ ((P ~ ) * (T ~ ))) \/ (((T ~ ) * (P ~ )) \/ T)) by SYSREL: 12

      .= ((((P * P) ~ ) \/ ((T * P) ~ )) \/ (((T ~ ) * (P ~ )) \/ T)) by RELAT_1: 35

      .= ((((P * P) ~ ) \/ ((T * P) ~ )) \/ (((P * T) ~ ) \/ T)) by RELAT_1: 35

      .= ((( {} ~ ) \/ ((T * P) ~ )) \/ (((P * T) ~ ) \/ T)) by Th24

      .= ((( {} ~ ) \/ (P ~ )) \/ (((P * T) ~ ) \/ T)) by Th23

      .= (( {} \/ (P ~ )) \/ ( {} \/ T)) by Th27

      .= ( e_entrance N);

      

       A2: (( e_escape N) * ( e_escape N)) = (((Q ~ ) * ((Q ~ ) \/ S)) \/ (S * ((Q ~ ) \/ S))) by SYSREL: 6

      .= ((((Q ~ ) * (Q ~ )) \/ ((Q ~ ) * S)) \/ (S * ((Q ~ ) \/ S))) by RELAT_1: 32

      .= ((((Q ~ ) * (Q ~ )) \/ ((Q ~ ) * S)) \/ ((S * (Q ~ )) \/ (S * S))) by RELAT_1: 32

      .= ((((Q * Q) ~ ) \/ ((Q ~ ) * S)) \/ ((S * (Q ~ )) \/ (S * S))) by RELAT_1: 35

      .= ((((Q * Q) ~ ) \/ ((Q ~ ) * (S ~ ))) \/ ((S * (Q ~ )) \/ (S * S)))

      .= ((((Q * Q) ~ ) \/ ((Q ~ ) * (S ~ ))) \/ (((S ~ ) * (Q ~ )) \/ (S * S)))

      .= ((((Q * Q) ~ ) \/ ((Q ~ ) * (S ~ ))) \/ (((S ~ ) * (Q ~ )) \/ S)) by SYSREL: 12

      .= ((((Q * Q) ~ ) \/ ((S * Q) ~ )) \/ (((S ~ ) * (Q ~ )) \/ S)) by RELAT_1: 35

      .= ((((Q * Q) ~ ) \/ ((S * Q) ~ )) \/ (((Q * S) ~ ) \/ S)) by RELAT_1: 35

      .= ((( {} ~ ) \/ ((S * Q) ~ )) \/ (((Q * S) ~ ) \/ S)) by Th24

      .= ((( {} ~ ) \/ (Q ~ )) \/ (((Q * S) ~ ) \/ S)) by Th23

      .= (( {} \/ (Q ~ )) \/ ( {} \/ S)) by Th27

      .= ( e_escape N);

      

       A3: (( e_escape N) * ( e_entrance N)) = (((Q ~ ) * ((P ~ ) \/ T)) \/ (S * ((P ~ ) \/ T))) by SYSREL: 6

      .= ((((Q ~ ) * (P ~ )) \/ ((Q ~ ) * T)) \/ (S * ((P ~ ) \/ T))) by RELAT_1: 32

      .= ((((Q ~ ) * (P ~ )) \/ ((Q ~ ) * T)) \/ ((S * (P ~ )) \/ (S * T))) by RELAT_1: 32

      .= ((((P * Q) ~ ) \/ ((Q ~ ) * T)) \/ ((S * (P ~ )) \/ (S * T))) by RELAT_1: 35

      .= ((((P * Q) ~ ) \/ ((Q ~ ) * (T ~ ))) \/ ((S * (P ~ )) \/ (S * T)))

      .= ((((P * Q) ~ ) \/ ((Q ~ ) * (T ~ ))) \/ (((S ~ ) * (P ~ )) \/ (S * T)))

      .= ((((P * Q) ~ ) \/ ((Q ~ ) * (T ~ ))) \/ (((S ~ ) * (P ~ )) \/ (S * S))) by Th13

      .= ((((P * Q) ~ ) \/ ((Q ~ ) * (T ~ ))) \/ (((S ~ ) * (P ~ )) \/ S)) by SYSREL: 12

      .= ((((P * Q) ~ ) \/ ((T * Q) ~ )) \/ (((S ~ ) * (P ~ )) \/ S)) by RELAT_1: 35

      .= ((((P * Q) ~ ) \/ ((T * Q) ~ )) \/ (((P * S) ~ ) \/ S)) by RELAT_1: 35

      .= ((((P * Q) ~ ) \/ ((S * Q) ~ )) \/ (((P * S) ~ ) \/ S)) by Th13

      .= ((((P * Q) ~ ) \/ ((S * Q) ~ )) \/ (((P * T) ~ ) \/ S)) by Th13

      .= ((( {} ~ ) \/ ((S * Q) ~ )) \/ (((P * T) ~ ) \/ S)) by Th24

      .= ((( {} ~ ) \/ (Q ~ )) \/ (((P * T) ~ ) \/ S)) by Th23

      .= (( {} \/ (Q ~ )) \/ ( {} \/ S)) by Th27

      .= ( e_escape N);

      (( e_entrance N) * ( e_escape N)) = (((P ~ ) * ((Q ~ ) \/ S)) \/ (T * ((Q ~ ) \/ S))) by SYSREL: 6

      .= ((((P ~ ) * (Q ~ )) \/ ((P ~ ) * S)) \/ (T * ((Q ~ ) \/ S))) by RELAT_1: 32

      .= ((((P ~ ) * (Q ~ )) \/ ((P ~ ) * S)) \/ ((T * (Q ~ )) \/ (T * S))) by RELAT_1: 32

      .= ((((Q * P) ~ ) \/ ((P ~ ) * S)) \/ ((T * (Q ~ )) \/ (T * S))) by RELAT_1: 35

      .= ((((Q * P) ~ ) \/ ((P ~ ) * (S ~ ))) \/ ((T * (Q ~ )) \/ (T * S)))

      .= ((((Q * P) ~ ) \/ ((P ~ ) * (S ~ ))) \/ (((T ~ ) * (Q ~ )) \/ (T * S)))

      .= ((((Q * P) ~ ) \/ ((P ~ ) * (S ~ ))) \/ (((T ~ ) * (Q ~ )) \/ (T * T))) by Th13

      .= ((((Q * P) ~ ) \/ ((P ~ ) * (S ~ ))) \/ (((T ~ ) * (Q ~ )) \/ T)) by SYSREL: 12

      .= ((((Q * P) ~ ) \/ ((S * P) ~ )) \/ (((T ~ ) * (Q ~ )) \/ T)) by RELAT_1: 35

      .= ((((Q * P) ~ ) \/ ((S * P) ~ )) \/ (((Q * T) ~ ) \/ T)) by RELAT_1: 35

      .= ((((Q * P) ~ ) \/ ((T * P) ~ )) \/ (((Q * T) ~ ) \/ T)) by Th13

      .= ((((Q * P) ~ ) \/ ((T * P) ~ )) \/ (((Q * S) ~ ) \/ T)) by Th13

      .= ((( {} ~ ) \/ ((T * P) ~ )) \/ (((Q * S) ~ ) \/ T)) by Th24

      .= ((( {} ~ ) \/ (P ~ )) \/ (((Q * S) ~ ) \/ T)) by Th23

      .= (( {} \/ (P ~ )) \/ ( {} \/ T)) by Th27

      .= ( e_entrance N);

      hence thesis by A1, A3, A2;

    end;

    theorem :: E_SIEC:30

    (( e_entrance N) * (( e_entrance N) \ ( id ( e_shore N)))) = {} & (( e_escape N) * (( e_escape N) \ ( id ( e_shore N)))) = {}

    proof

      set P = (the escape of N \ ( id N));

      set Q = (the entrance of N \ ( id the carrier of N));

      set S = ( id (the carrier of N \ ( rng the entrance of N)));

      set T = ( id (the carrier of N \ ( rng the escape of N)));

      set R = ( id the carrier of N);

      

       A1: S c= R by SYSREL: 15, XBOOLE_1: 36;

      ((Q ~ ) * ((Q ~ ) \ R)) c= ((Q ~ ) * (Q ~ )) by RELAT_1: 29, XBOOLE_1: 36;

      then ((Q ~ ) * ((Q ~ ) \ R)) c= {} by Th25;

      then

       A2: ((Q ~ ) * ((Q ~ ) \ R)) = {} by XBOOLE_1: 3;

      (S * ((Q ~ ) \ R)) c= (S * (Q ~ )) by RELAT_1: 29, XBOOLE_1: 36;

      then (S * ((Q ~ ) \ R)) c= {} by Th28;

      then

       A3: (S * ((Q ~ ) \ R)) = {} by XBOOLE_1: 3;

      

       A4: (( e_escape N) * (( e_escape N) \ ( id ( e_shore N)))) = (((Q ~ ) \/ S) * (((Q ~ ) \ R) \/ (S \ R))) by XBOOLE_1: 42

      .= (((Q ~ ) \/ S) * (((Q ~ ) \ R) \/ {} )) by A1, XBOOLE_1: 37

      .= ( {} \/ {} ) by A2, A3, SYSREL: 6

      .= {} ;

      

       A5: T c= R by SYSREL: 15, XBOOLE_1: 36;

      (T * ((P ~ ) \ R)) c= (T * (P ~ )) by RELAT_1: 29, XBOOLE_1: 36;

      then (T * ((P ~ ) \ R)) c= {} by Th28;

      then

       A6: (T * ((P ~ ) \ R)) = {} by XBOOLE_1: 3;

      ((P ~ ) * ((P ~ ) \ R)) c= ((P ~ ) * (P ~ )) by RELAT_1: 29, XBOOLE_1: 36;

      then ((P ~ ) * ((P ~ ) \ R)) c= {} by Th25;

      then

       A7: ((P ~ ) * ((P ~ ) \ R)) = {} by XBOOLE_1: 3;

      (( e_entrance N) * (( e_entrance N) \ ( id ( e_shore N)))) = (((P ~ ) \/ T) * (((P ~ ) \ R) \/ (T \ R))) by XBOOLE_1: 42

      .= (((P ~ ) \/ T) * (((P ~ ) \ R) \/ {} )) by A5, XBOOLE_1: 37

      .= ( {} \/ {} ) by A7, A6, SYSREL: 6

      .= {} ;

      hence thesis by A4;

    end;

    definition

      let N;

      :: E_SIEC:def19

      func e_adjac (N) -> Relation equals (((the entrance of N \/ the escape of N) \ ( id the carrier of N)) \/ ( id (the carrier of N \ ( rng the entrance of N))));

      correctness ;

    end

    theorem :: E_SIEC:31

    ( e_adjac N) c= [:( e_shore N), ( e_shore N):] & ( e_flow N) c= [:( e_shore N), ( e_shore N):]

    proof

      

       A1: ((the entrance of N \/ the escape of N) \ ( id the carrier of N)) c= (the entrance of N \/ the escape of N) by XBOOLE_1: 36;

      

       A2: the escape of N c= [:the carrier of N, the carrier of N:] by Def1;

      

       A3: the entrance of N c= [:the carrier of N, the carrier of N:] by Def1;

      then (the entrance of N ~ ) c= [:the carrier of N, the carrier of N:] by SYSREL: 4;

      then

       A4: ( id the carrier of N) c= [:the carrier of N, the carrier of N:] & ((the entrance of N ~ ) \/ the escape of N) c= [:the carrier of N, the carrier of N:] by A2, RELSET_1: 13, XBOOLE_1: 8;

      ( id (the carrier of N \ ( rng the entrance of N))) c= ( id the carrier of N) & ( id the carrier of N) c= [:the carrier of N, the carrier of N:] by RELSET_1: 13, SYSREL: 15, XBOOLE_1: 36;

      then

       A5: ( id (the carrier of N \ ( rng the entrance of N))) c= [:the carrier of N, the carrier of N:] by XBOOLE_1: 1;

      (the entrance of N \/ the escape of N) c= [:the carrier of N, the carrier of N:] by A3, A2, XBOOLE_1: 8;

      then ((the entrance of N \/ the escape of N) \ ( id the carrier of N)) c= [:the carrier of N, the carrier of N:] by A1, XBOOLE_1: 1;

      hence thesis by A5, A4, XBOOLE_1: 8;

    end;

    theorem :: E_SIEC:32

    (( e_adjac N) * ( e_adjac N)) = ( e_adjac N) & ((( e_adjac N) \ ( id ( e_shore N))) * ( e_adjac N)) = {} & ((( e_adjac N) \/ (( e_adjac N) ~ )) \/ ( id ( e_shore N))) = (( e_flow N) \/ (( e_flow N) ~ ))

    proof

      set P = the entrance of N;

      set Q = the escape of N;

      set R = ( id the carrier of N);

      set S = ( id (the carrier of N \ ( rng the entrance of N)));

      set T = ( id (the carrier of N \ ( rng the escape of N)));

      

       A1: S c= R by SYSREL: 15, XBOOLE_1: 36;

      (( e_adjac N) \/ (( e_adjac N) ~ )) = ((((P \/ Q) \ R) \/ S) \/ ((((P \/ Q) \ R) ~ ) \/ (S ~ ))) by RELAT_1: 23

      .= ((((P \/ Q) \ R) \/ S) \/ ((((P \/ Q) \ R) ~ ) \/ S))

      .= ((((P \/ Q) \ R) \/ (((P \/ Q) \ R) ~ )) \/ S) by XBOOLE_1: 5

      .= ((((P \/ Q) \ R) \/ (((P \/ Q) ~ ) \ (R ~ ))) \/ S) by RELAT_1: 24

      .= ((((P \/ Q) \ R) \/ (((P \/ Q) ~ ) \ R)) \/ S)

      .= ((((P \/ Q) \/ ((P \/ Q) ~ )) \ R) \/ S) by XBOOLE_1: 42;

      

      then

       A2: ((( e_adjac N) \/ (( e_adjac N) ~ )) \/ ( id ( e_shore N))) = ((((P \/ Q) \/ ((P \/ Q) ~ )) \ R) \/ (S \/ R)) by XBOOLE_1: 4

      .= ((((P \/ Q) \/ ((P \/ Q) ~ )) \ R) \/ R) by A1, XBOOLE_1: 12

      .= (((((P ~ ) \/ (Q ~ )) \/ (P \/ Q)) \ R) \/ R) by RELAT_1: 23

      .= ((((P ~ ) \/ ((Q \/ P) \/ (Q ~ ))) \ R) \/ R) by XBOOLE_1: 4

      .= ((((P ~ ) \/ (Q \/ (P \/ (Q ~ )))) \ R) \/ R) by XBOOLE_1: 4

      .= (((((P ~ ) \/ Q) \/ (P \/ (Q ~ ))) \ R) \/ R) by XBOOLE_1: 4

      .= ((((P ~ ) \/ Q) \/ (P \/ (Q ~ ))) \/ R) by XBOOLE_1: 39

      .= (( e_flow N) \/ ((((P \/ (Q ~ )) ~ ) ~ ) \/ R)) by XBOOLE_1: 5

      .= (( e_flow N) \/ ((((P ~ ) \/ ((Q ~ ) ~ )) ~ ) \/ R)) by RELAT_1: 23

      .= (( e_flow N) \/ ((((P ~ ) \/ Q) ~ ) \/ (R ~ )))

      .= (( e_flow N) \/ (( e_flow N) ~ )) by RELAT_1: 23;

      S c= R by SYSREL: 15, XBOOLE_1: 36;

      then

       A3: (S \ R) = {} by XBOOLE_1: 37;

      ((P \ R) * (Q \ R)) c= (P * (Q \ R)) by RELAT_1: 30, XBOOLE_1: 36;

      then ((P \ R) * (Q \ R)) c= {} by Th15;

      then

       A4: ((P \ R) * (Q \ R)) = {} by XBOOLE_1: 3;

      ((P \ R) * (P \ R)) c= (P * (P \ R)) by RELAT_1: 30, XBOOLE_1: 36;

      then ((P \ R) * (P \ R)) c= {} by Def2;

      then

       A5: ((P \ R) * (P \ R)) = {} by XBOOLE_1: 3;

      ((Q \ R) * (P \ R)) c= (Q * (P \ R)) by RELAT_1: 30, XBOOLE_1: 36;

      then ((Q \ R) * (P \ R)) c= {} by Th15;

      then

       A6: ((Q \ R) * (P \ R)) = {} by XBOOLE_1: 3;

      ((Q \ R) * (Q \ R)) c= (Q * (Q \ R)) by RELAT_1: 30, XBOOLE_1: 36;

      then ((Q \ R) * (Q \ R)) c= {} by Def2;

      then

       A7: ((Q \ R) * (Q \ R)) = {} by XBOOLE_1: 3;

      

       A8: ((( e_adjac N) \ R) * ( e_adjac N)) = ((((((P \/ Q) \ R) \/ S) \ R) * ((P \/ Q) \ R)) \/ (((((P \/ Q) \ R) \/ S) \ R) * S)) by RELAT_1: 32

      .= ((((((P \ R) \/ (Q \ R)) \/ S) \ R) * ((P \/ Q) \ R)) \/ (((((P \/ Q) \ R) \/ S) \ R) * S)) by XBOOLE_1: 42

      .= ((((((P \ R) \/ (Q \ R)) \ R) \/ (S \ R)) * ((P \/ Q) \ R)) \/ (((((P \/ Q) \ R) \/ S) \ R) * S)) by XBOOLE_1: 42

      .= ((((((P \ R) \ R) \/ ((Q \ R) \ R)) \/ (S \ R)) * ((P \/ Q) \ R)) \/ (((((P \/ Q) \ R) \/ S) \ R) * S)) by XBOOLE_1: 42

      .= (((((P \ (R \/ R)) \/ ((Q \ R) \ R)) \/ (S \ R)) * ((P \/ Q) \ R)) \/ (((((P \/ Q) \ R) \/ S) \ R) * S)) by XBOOLE_1: 41

      .= (((((P \ R) \/ (Q \ (R \/ R))) \/ (S \ R)) * ((P \/ Q) \ R)) \/ (((((P \/ Q) \ R) \/ S) \ R) * S)) by XBOOLE_1: 41

      .= (((((P \ R) \/ (Q \ R)) \/ (S \ R)) * ((P \ R) \/ (Q \ R))) \/ (((((P \/ Q) \ R) \/ S) \ R) * S)) by XBOOLE_1: 42

      .= (((((P \ R) \/ (Q \ R)) \/ (S \ R)) * ((P \ R) \/ (Q \ R))) \/ (((((P \ R) \/ (Q \ R)) \/ S) \ R) * S)) by XBOOLE_1: 42

      .= ((((((P \ R) \/ (Q \ R)) \/ (S \ R)) * (P \ R)) \/ ((((P \ R) \/ (Q \ R)) \/ (S \ R)) * (Q \ R))) \/ (((((P \ R) \/ (Q \ R)) \/ S) \ R) * S)) by RELAT_1: 32

      .= ((((((P \ R) \/ (Q \ R)) \/ (S \ R)) * (P \ R)) \/ ((((P \ R) \/ (Q \ R)) * (Q \ R)) \/ ((S \ R) * (Q \ R)))) \/ (((((P \ R) \/ (Q \ R)) \/ S) \ R) * S)) by SYSREL: 6

      .= ((((((P \ R) \/ (Q \ R)) * (P \ R)) \/ ((S \ R) * (P \ R))) \/ ((((P \ R) \/ (Q \ R)) * (Q \ R)) \/ ((S \ R) * (Q \ R)))) \/ (((((P \ R) \/ (Q \ R)) \/ S) \ R) * S)) by SYSREL: 6

      .= (((( {} \/ {} ) \/ ((S \ R) * (P \ R))) \/ ((((P \ R) \/ (Q \ R)) * (Q \ R)) \/ ((S \ R) * (Q \ R)))) \/ (((((P \ R) \/ (Q \ R)) \/ S) \ R) * S)) by A5, A6, SYSREL: 6

      .= ((( {} * (P \ R)) \/ ( {} * (Q \ R))) \/ (((((P \ R) \/ (Q \ R)) \/ S) \ R) * S)) by A3, A4, A7, SYSREL: 6

      .= (((((P \ R) \/ (Q \ R)) \ R) \/ (S \ R)) * S) by XBOOLE_1: 42

      .= (((((P \ R) \ R) \/ ((Q \ R) \ R)) \/ (S \ R)) * S) by XBOOLE_1: 42

      .= ((((P \ (R \/ R)) \/ ((Q \ R) \ R)) \/ (S \ R)) * S) by XBOOLE_1: 41

      .= ((((P \ R) \/ (Q \ (R \/ R))) \/ (S \ R)) * S) by XBOOLE_1: 41

      .= (((P \ R) * S) \/ ((Q \ R) * S)) by A3, SYSREL: 6

      .= ( {} \/ ((Q \ R) * S)) by Th27

      .= ( {} \/ ((Q \ R) * T)) by Th13

      .= {} by Th27;

      (( e_adjac N) * ( e_adjac N)) = ((((P \/ Q) \ R) * (((P \/ Q) \ R) \/ S)) \/ (S * (((P \/ Q) \ R) \/ S))) by SYSREL: 6

      .= (((((P \/ Q) \ R) * ((P \/ Q) \ R)) \/ (((P \/ Q) \ R) * S)) \/ (S * (((P \/ Q) \ R) \/ S))) by RELAT_1: 32

      .= (((((P \/ Q) \ R) * ((P \/ Q) \ R)) \/ (((P \/ Q) \ R) * S)) \/ ((S * ((P \/ Q) \ R)) \/ (S * S))) by RELAT_1: 32

      .= (((((P \ R) \/ (Q \ R)) * ((P \/ Q) \ R)) \/ (((P \/ Q) \ R) * S)) \/ ((S * ((P \/ Q) \ R)) \/ (S * S))) by XBOOLE_1: 42

      .= (((((P \ R) \/ (Q \ R)) * ((P \ R) \/ (Q \ R))) \/ (((P \/ Q) \ R) * S)) \/ ((S * ((P \/ Q) \ R)) \/ (S * S))) by XBOOLE_1: 42

      .= (((((P \ R) \/ (Q \ R)) * ((P \ R) \/ (Q \ R))) \/ (((P \ R) \/ (Q \ R)) * S)) \/ ((S * ((P \/ Q) \ R)) \/ (S * S))) by XBOOLE_1: 42

      .= (((((P \ R) \/ (Q \ R)) * ((P \ R) \/ (Q \ R))) \/ (((P \ R) \/ (Q \ R)) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S * S))) by XBOOLE_1: 42

      .= ((((((P \ R) \/ (Q \ R)) * (P \ R)) \/ (((P \ R) \/ (Q \ R)) * (Q \ R))) \/ (((P \ R) \/ (Q \ R)) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S * S))) by RELAT_1: 32

      .= (((( {} \/ {} ) \/ (((P \ R) \/ (Q \ R)) * (Q \ R))) \/ (((P \ R) \/ (Q \ R)) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S * S))) by A5, A6, SYSREL: 6

      .= (( {} \/ (((P \ R) \/ (Q \ R)) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S * S))) by A4, A7, SYSREL: 6

      .= ((((P \ R) \/ (Q \ R)) * S) \/ ((S * ((P \ R) \/ (Q \ R))) \/ S)) by SYSREL: 12

      .= ((((P \ R) * S) \/ ((Q \ R) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ S)) by SYSREL: 6

      .= ((((P \ R) * S) \/ ((Q \ R) * S)) \/ (((S * (P \ R)) \/ (S * (Q \ R))) \/ S)) by RELAT_1: 32

      .= (( {} \/ ((Q \ R) * S)) \/ (((S * (P \ R)) \/ (S * (Q \ R))) \/ S)) by Th27

      .= (((Q \ R) * T) \/ (((S * (P \ R)) \/ (S * (Q \ R))) \/ S)) by Th13

      .= ( {} \/ (((S * (P \ R)) \/ (S * (Q \ R))) \/ S)) by Th27

      .= (((P \ R) \/ (S * (Q \ R))) \/ S) by Th23

      .= (((P \ R) \/ (T * (Q \ R))) \/ S) by Th13

      .= (((P \ R) \/ (Q \ R)) \/ S) by Th23

      .= ( e_adjac N) by XBOOLE_1: 42;

      hence thesis by A8, A2;

    end;

    reserve N for e_net;

    theorem :: E_SIEC:33

    

     Th33: ((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):]

    proof

      (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):] by Th18;

      hence thesis by SYSREL: 4;

    end;

    definition

      let N be G_Net;

      :: E_SIEC:def20

      func s_pre (N) -> Relation equals ((the escape of N \ ( id the carrier of N)) ~ );

      coherence ;

      :: E_SIEC:def21

      func s_post (N) -> Relation equals ((the entrance of N \ ( id the carrier of N)) ~ );

      coherence ;

    end

    theorem :: E_SIEC:34

    ( s_post N) c= [:( e_Places N), ( e_Transitions N):] & ( s_pre N) c= [:( e_Places N), ( e_Transitions N):] by Th33;