ff_siec.miz

    begin

    reserve x,y for object,

X,Y for set;

    reserve M for Pnet;

    definition

      let X, Y;

      assume

       A1: X misses Y;

      :: FF_SIEC:def1

      func PTempty_f_net (X,Y) -> strict Pnet equals

      : Def1: PT_net_Str (# X, Y, ( {} (X,Y)), ( {} (Y,X)) #);

      correctness

      proof

        set M = PT_net_Str (# X, Y, ( {} (X,Y)), ( {} (Y,X)) #);

        ( Flow M) c= ( [:the carrier of M, the carrier' of M:] \/ [:the carrier' of M, the carrier of M:]) by XBOOLE_1: 13;

        hence thesis by A1, NET_1:def 2;

      end;

    end

    definition

      let X;

      :: FF_SIEC:def2

      func Tempty_f_net (X) -> strict Pnet equals ( PTempty_f_net (X, {} ));

      correctness ;

      :: FF_SIEC:def3

      func Pempty_f_net (X) -> strict Pnet equals ( PTempty_f_net ( {} ,X));

      correctness ;

    end

    definition

      let x;

      :: FF_SIEC:def4

      func Tsingle_f_net (x) -> strict Pnet equals ( PTempty_f_net ( {} , {x}));

      correctness ;

      :: FF_SIEC:def5

      func Psingle_f_net (x) -> strict Pnet equals ( PTempty_f_net ( {x}, {} ));

      correctness ;

    end

    definition

      :: FF_SIEC:def6

      func empty_f_net -> strict Pnet equals ( PTempty_f_net ( {} , {} ));

      correctness ;

    end

    theorem :: FF_SIEC:1

    X misses Y implies the carrier of ( PTempty_f_net (X,Y)) = X & the carrier' of ( PTempty_f_net (X,Y)) = Y & ( Flow ( PTempty_f_net (X,Y))) = {}

    proof

      assume X misses Y;

      then ( PTempty_f_net (X,Y)) = PT_net_Str (# X, Y, ( {} (X,Y)), ( {} (Y,X)) #) by Def1;

      hence thesis;

    end;

    theorem :: FF_SIEC:2

    the carrier of ( Tempty_f_net X) = X & the carrier' of ( Tempty_f_net X) = {} & ( Flow ( Tempty_f_net X)) = {}

    proof

      ( Tempty_f_net X) = PT_net_Str (# X, {} , ( {} (X, {} )), ( {} ( {} ,X)) #) by Def1, XBOOLE_1: 65;

      hence thesis;

    end;

    theorem :: FF_SIEC:3

    for X holds the carrier of ( Pempty_f_net X) = {} & the carrier' of ( Pempty_f_net X) = X & ( Flow ( Pempty_f_net X)) = {}

    proof

      let X;

       {} misses X by XBOOLE_1: 65;

      then ( Pempty_f_net X) = PT_net_Str (# {} , X, ( {} ( {} ,X)), ( {} (X, {} )) #) by Def1;

      hence thesis;

    end;

    theorem :: FF_SIEC:4

    for x holds the carrier of ( Tsingle_f_net x) = {} & the carrier' of ( Tsingle_f_net x) = {x} & ( Flow ( Tsingle_f_net x)) = {}

    proof

      let x;

       {} misses {x} by XBOOLE_1: 65;

      then ( Tsingle_f_net x) = PT_net_Str (# {} , {x}, ( {} ( {} , {x})), ( {} ( {x}, {} )) #) by Def1;

      hence thesis;

    end;

    theorem :: FF_SIEC:5

    for x holds the carrier of ( Psingle_f_net x) = {x} & the carrier' of ( Psingle_f_net x) = {} & ( Flow ( Psingle_f_net x)) = {}

    proof

      let x;

      ( Psingle_f_net x) = PT_net_Str (# {x}, {} , ( {} ( {x}, {} )), ( {} ( {} , {x})) #) by Def1, XBOOLE_1: 65;

      hence thesis;

    end;

    theorem :: FF_SIEC:6

    the carrier of empty_f_net = {} & the carrier' of empty_f_net = {} & ( Flow empty_f_net ) = {}

    proof

       empty_f_net = PT_net_Str (# {} , {} , ( {} ( {} , {} )), ( {} ( {} , {} )) #) by Def1, XBOOLE_1: 65;

      hence thesis;

    end;

    theorem :: FF_SIEC:7



     Th7: ( [x, y] in ( Flow M) & x in the carrier' of M implies not x in the carrier of M & not y in the carrier' of M & y in the carrier of M) & ( [x, y] in ( Flow M) & y in the carrier' of M implies not y in the carrier of M & not x in the carrier' of M & x in the carrier of M) & ( [x, y] in ( Flow M) & x in the carrier of M implies not y in the carrier of M & not x in the carrier' of M & y in the carrier' of M) & ( [x, y] in ( Flow M) & y in the carrier of M implies not x in the carrier of M & not y in the carrier' of M & x in the carrier' of M)

    proof



       A1: the carrier of M misses the carrier' of M by NET_1:def 2;

      ( Flow M) c= ( [:the carrier of M, the carrier' of M:] \/ [:the carrier' of M, the carrier of M:]) by NET_1:def 2;

      hence thesis by A1, SYSREL: 7;

    end;

    theorem :: FF_SIEC:8



     Th8: ( Flow M) c= [:( Elements M), ( Elements M):] & (( Flow M) ~ ) c= [:( Elements M), ( Elements M):]

    proof



       A1: the carrier of M c= ( Elements M) by XBOOLE_1: 7;



       A2: the carrier' of M c= ( Elements M) by XBOOLE_1: 7;

      then

       A3: [:the carrier of M, the carrier' of M:] c= [:( Elements M), ( Elements M):] by A1, ZFMISC_1: 96;

       [:the carrier' of M, the carrier of M:] c= [:( Elements M), ( Elements M):] by A1, A2, ZFMISC_1: 96;

      then

       A4: ( [:the carrier of M, the carrier' of M:] \/ [:the carrier' of M, the carrier of M:]) c= [:( Elements M), ( Elements M):] by A3, XBOOLE_1: 8;

      ( Flow M) c= ( [:the carrier of M, the carrier' of M:] \/ [:the carrier' of M, the carrier of M:]) by NET_1:def 2;

      then ( Flow M) c= [:( Elements M), ( Elements M):] by A4, XBOOLE_1: 1;

      hence thesis by SYSREL: 4;

    end;

    theorem :: FF_SIEC:9



     Th9: ( rng (( Flow M) | the carrier' of M)) c= the carrier of M & ( rng ((( Flow M) ~ ) | the carrier' of M)) c= the carrier of M & ( rng (( Flow M) | the carrier of M)) c= the carrier' of M & ( rng ((( Flow M) ~ ) | the carrier of M)) c= the carrier' of M & ( rng ( id the carrier' of M)) c= the carrier' of M & ( dom ( id the carrier' of M)) c= the carrier' of M & ( rng ( id the carrier of M)) c= the carrier of M & ( dom ( id the carrier of M)) c= the carrier of M

    proof



       A1: for x be object holds x in ( rng (( Flow M) | the carrier' of M)) implies x in the carrier of M

      proof

        let x be object;

        assume x in ( rng (( Flow M) | the carrier' of M));

        then

        consider y be object such that

         A2: [y, x] in (( Flow M) | the carrier' of M) by XTUPLE_0:def 13;



         A3: y in the carrier' of M by A2, RELAT_1:def 11;

         [y, x] in ( Flow M) by A2, RELAT_1:def 11;

        hence thesis by A3, Th7;

      end;



       A4: for x be object holds x in ( rng ((( Flow M) ~ ) | the carrier' of M)) implies x in the carrier of M

      proof

        let x be object;

        assume x in ( rng ((( Flow M) ~ ) | the carrier' of M));

        then

        consider y be object such that

         A5: [y, x] in ((( Flow M) ~ ) | the carrier' of M) by XTUPLE_0:def 13;



         A6: [y, x] in (( Flow M) ~ ) by A5, RELAT_1:def 11;



         A7: y in the carrier' of M by A5, RELAT_1:def 11;

         [x, y] in ( Flow M) by A6, RELAT_1:def 7;

        hence thesis by A7, Th7;

      end;



       A8: for x be object holds x in ( rng (( Flow M) | the carrier of M)) implies x in the carrier' of M

      proof

        let x be object;

        assume x in ( rng (( Flow M) | the carrier of M));

        then

        consider y be object such that

         A9: [y, x] in (( Flow M) | the carrier of M) by XTUPLE_0:def 13;



         A10: y in the carrier of M by A9, RELAT_1:def 11;

         [y, x] in ( Flow M) by A9, RELAT_1:def 11;

        hence thesis by A10, Th7;

      end;

      for x be object holds x in ( rng ((( Flow M) ~ ) | the carrier of M)) implies x in the carrier' of M

      proof

        let x be object;

        assume x in ( rng ((( Flow M) ~ ) | the carrier of M));

        then

        consider y be object such that

         A11: [y, x] in ((( Flow M) ~ ) | the carrier of M) by XTUPLE_0:def 13;



         A12: [y, x] in (( Flow M) ~ ) by A11, RELAT_1:def 11;



         A13: y in the carrier of M by A11, RELAT_1:def 11;

         [x, y] in ( Flow M) by A12, RELAT_1:def 7;

        hence thesis by A13, Th7;

      end;

      hence thesis by A1, A4, A8, TARSKI:def 3;

    end;

    theorem :: FF_SIEC:10



     Th10: ( rng (( Flow M) | the carrier' of M)) misses ( dom (( Flow M) | the carrier' of M)) & ( rng (( Flow M) | the carrier' of M)) misses ( dom ((( Flow M) ~ ) | the carrier' of M)) & ( rng (( Flow M) | the carrier' of M)) misses ( dom ( id the carrier' of M)) & ( rng ((( Flow M) ~ ) | the carrier' of M)) misses ( dom (( Flow M) | the carrier' of M)) & ( rng ((( Flow M) ~ ) | the carrier' of M)) misses ( dom ((( Flow M) ~ ) | the carrier' of M)) & ( rng ((( Flow M) ~ ) | the carrier' of M)) misses ( dom ( id the carrier' of M)) & ( dom (( Flow M) | the carrier' of M)) misses ( rng (( Flow M) | the carrier' of M)) & ( dom (( Flow M) | the carrier' of M)) misses ( rng ((( Flow M) ~ ) | the carrier' of M)) & ( dom (( Flow M) | the carrier' of M)) misses ( rng ( id the carrier of M)) & ( dom ((( Flow M) ~ ) | the carrier' of M)) misses ( rng (( Flow M) | the carrier' of M)) & ( dom ((( Flow M) ~ ) | the carrier' of M)) misses ( rng ((( Flow M) ~ ) | the carrier' of M)) & ( dom ((( Flow M) ~ ) | the carrier' of M)) misses ( rng ( id the carrier of M)) & ( rng (( Flow M) | the carrier of M)) misses ( dom (( Flow M) | the carrier of M)) & ( rng (( Flow M) | the carrier of M)) misses ( dom ((( Flow M) ~ ) | the carrier of M)) & ( rng (( Flow M) | the carrier of M)) misses ( dom ( id the carrier of M)) & ( rng ((( Flow M) ~ ) | the carrier of M)) misses ( dom (( Flow M) | the carrier of M)) & ( rng ((( Flow M) ~ ) | the carrier of M)) misses ( dom ((( Flow M) ~ ) | the carrier of M)) & ( rng ((( Flow M) ~ ) | the carrier of M)) misses ( dom ( id the carrier of M)) & ( dom (( Flow M) | the carrier of M)) misses ( rng (( Flow M) | the carrier of M)) & ( dom (( Flow M) | the carrier of M)) misses ( rng ((( Flow M) ~ ) | the carrier of M)) & ( dom (( Flow M) | the carrier of M)) misses ( rng ( id the carrier' of M)) & ( dom ((( Flow M) ~ ) | the carrier of M)) misses ( rng (( Flow M) | the carrier of M)) & ( dom ((( Flow M) ~ ) | the carrier of M)) misses ( rng ((( Flow M) ~ ) | the carrier of M)) & ( dom ((( Flow M) ~ ) | the carrier of M)) misses ( rng ( id the carrier' of M))

    proof

      set R = (( Flow M) | the carrier' of M);

      set S = ((( Flow M) ~ ) | the carrier' of M);

      set T = ( id the carrier' of M);

      set R1 = (( Flow M) | the carrier of M);

      set S1 = ((( Flow M) ~ ) | the carrier of M);

      set T1 = ( id the carrier of M);



       A1: ( dom R) c= the carrier' of M by RELAT_1: 58;



       A2: ( rng R) c= the carrier of M by Th9;



       A3: ( dom S) c= the carrier' of M by RELAT_1: 58;



       A4: ( rng S) c= the carrier of M by Th9;



       A5: ( dom R1) c= the carrier of M by RELAT_1: 58;



       A6: ( rng R1) c= the carrier' of M by Th9;



       A7: ( dom S1) c= the carrier of M by RELAT_1: 58;



       A8: ( rng S1) c= the carrier' of M by Th9;

      the carrier of M misses the carrier' of M by NET_1:def 2;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, XBOOLE_1: 64;

    end;

    theorem :: FF_SIEC:11



     Th11: ((( Flow M) | the carrier' of M) * (( Flow M) | the carrier' of M)) = {} & (((( Flow M) ~ ) | the carrier' of M) * ((( Flow M) ~ ) | the carrier' of M)) = {} & ((( Flow M) | the carrier' of M) * ((( Flow M) ~ ) | the carrier' of M)) = {} & (((( Flow M) ~ ) | the carrier' of M) * (( Flow M) | the carrier' of M)) = {} & ((( Flow M) | the carrier of M) * (( Flow M) | the carrier of M)) = {} & (((( Flow M) ~ ) | the carrier of M) * ((( Flow M) ~ ) | the carrier of M)) = {} & ((( Flow M) | the carrier of M) * ((( Flow M) ~ ) | the carrier of M)) = {} & (((( Flow M) ~ ) | the carrier of M) * (( Flow M) | the carrier of M)) = {}

    proof



       A1: ( rng (( Flow M) | the carrier' of M)) misses ( dom (( Flow M) | the carrier' of M)) by Th10;



       A2: ( rng ((( Flow M) ~ ) | the carrier' of M)) misses ( dom ((( Flow M) ~ ) | the carrier' of M)) by Th10;



       A3: ( rng (( Flow M) | the carrier' of M)) misses ( dom ((( Flow M) ~ ) | the carrier' of M)) by Th10;



       A4: ( rng ((( Flow M) ~ ) | the carrier' of M)) misses ( dom (( Flow M) | the carrier' of M)) by Th10;



       A5: ( rng (( Flow M) | the carrier of M)) misses ( dom (( Flow M) | the carrier of M)) by Th10;



       A6: ( rng ((( Flow M) ~ ) | the carrier of M)) misses ( dom ((( Flow M) ~ ) | the carrier of M)) by Th10;



       A7: ( rng (( Flow M) | the carrier of M)) misses ( dom ((( Flow M) ~ ) | the carrier of M)) by Th10;

      ( rng ((( Flow M) ~ ) | the carrier of M)) misses ( dom (( Flow M) | the carrier of M)) by Th10;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, RELAT_1: 44;

    end;

    theorem :: FF_SIEC:12



     Th12: ((( Flow M) | the carrier' of M) * ( id the carrier of M)) = (( Flow M) | the carrier' of M) & (((( Flow M) ~ ) | the carrier' of M) * ( id the carrier of M)) = ((( Flow M) ~ ) | the carrier' of M) & (( id the carrier' of M) * (( Flow M) | the carrier' of M)) = (( Flow M) | the carrier' of M) & (( id the carrier' of M) * ((( Flow M) ~ ) | the carrier' of M)) = ((( Flow M) ~ ) | the carrier' of M) & ((( Flow M) | the carrier of M) * ( id the carrier' of M)) = (( Flow M) | the carrier of M) & (((( Flow M) ~ ) | the carrier of M) * ( id the carrier' of M)) = ((( Flow M) ~ ) | the carrier of M) & (( id the carrier of M) * (( Flow M) | the carrier of M)) = (( Flow M) | the carrier of M) & (( id the carrier of M) * ((( Flow M) ~ ) | the carrier of M)) = ((( Flow M) ~ ) | the carrier of M) & ((( Flow M) | the carrier of M) * ( id the carrier' of M)) = (( Flow M) | the carrier of M) & (((( Flow M) ~ ) | the carrier of M) * ( id the carrier' of M)) = ((( Flow M) ~ ) | the carrier of M) & (( id the carrier' of M) * (( Flow M) | the carrier of M)) = {} & (( id the carrier' of M) * ((( Flow M) ~ ) | the carrier of M)) = {} & ((( Flow M) | the carrier of M) * ( id the carrier of M)) = {} & (((( Flow M) ~ ) | the carrier of M) * ( id the carrier of M)) = {} & (( id the carrier of M) * (( Flow M) | the carrier' of M)) = {} & (( id the carrier of M) * ((( Flow M) ~ ) | the carrier' of M)) = {} & ((( Flow M) | the carrier' of M) * ( id the carrier' of M)) = {} & (((( Flow M) ~ ) | the carrier' of M) * ( id the carrier' of M)) = {}

    proof



       A1: ( rng (( Flow M) | the carrier' of M)) c= the carrier of M by Th9;



       A2: ( rng ((( Flow M) ~ ) | the carrier' of M)) c= the carrier of M by Th9;



       A3: ( rng (( Flow M) | the carrier of M)) c= the carrier' of M by Th9;



       A4: ( rng ((( Flow M) ~ ) | the carrier of M)) c= the carrier' of M by Th9;



       A5: ( dom (( Flow M) | the carrier of M)) misses ( rng ( id the carrier' of M)) by Th10;



       A6: ( dom ((( Flow M) ~ ) | the carrier of M)) misses ( rng ( id the carrier' of M)) by Th10;



       A7: ( rng (( Flow M) | the carrier of M)) misses ( dom ( id the carrier of M)) by Th10;



       A8: ( rng ((( Flow M) ~ ) | the carrier of M)) misses ( dom ( id the carrier of M)) by Th10;



       A9: ( rng ( id the carrier of M)) misses ( dom (( Flow M) | the carrier' of M)) by Th10;



       A10: ( rng ( id the carrier of M)) misses ( dom ((( Flow M) ~ ) | the carrier' of M)) by Th10;



       A11: ( rng (( Flow M) | the carrier' of M)) misses ( dom ( id the carrier' of M)) by Th10;

      ( rng ((( Flow M) ~ ) | the carrier' of M)) misses ( dom ( id the carrier' of M)) by Th10;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, RELAT_1: 44, RELAT_1: 51, RELAT_1: 53, RELAT_1: 58;

    end;

    theorem :: FF_SIEC:13



     Th13: ((( Flow M) ~ ) | the carrier' of M) misses ( id ( Elements M)) & (( Flow M) | the carrier' of M) misses ( id ( Elements M)) & ((( Flow M) ~ ) | the carrier of M) misses ( id ( Elements M)) & (( Flow M) | the carrier of M) misses ( id ( Elements M))

    proof

      set T = ( id ( Elements M));

      thus ((( Flow M) ~ ) | the carrier' of M) misses ( id ( Elements M))

      proof

        set R = ((( Flow M) ~ ) | the carrier' of M);

        for x,y be object holds not [x, y] in (R /\ T)

        proof

          let x,y be object;

          assume

           A1: [x, y] in (R /\ T);

          then

           A2: [x, y] in R by XBOOLE_0:def 4;



           A3: [x, y] in T by A1, XBOOLE_0:def 4;



           A4: [x, y] in (( Flow M) ~ ) by A2, RELAT_1:def 11;



           A5: x in the carrier' of M by A2, RELAT_1:def 11;

           [y, x] in ( Flow M) by A4, RELAT_1:def 7;

          then x <> y by A5, Th7;

          hence thesis by A3, RELAT_1:def 10;

        end;

        then (R /\ T) = {} by RELAT_1: 37;

        hence thesis by XBOOLE_0:def 7;

      end;

      thus (( Flow M) | the carrier' of M) misses ( id ( Elements M))

      proof

        set R = (( Flow M) | the carrier' of M);

        for x,y be object holds not [x, y] in (R /\ T)

        proof

          let x,y be object;

          assume

           A6: [x, y] in (R /\ T);

          then

           A7: [x, y] in R by XBOOLE_0:def 4;



           A8: [x, y] in T by A6, XBOOLE_0:def 4;



           A9: x in the carrier' of M by A7, RELAT_1:def 11;

           [x, y] in ( Flow M) by A7, RELAT_1:def 11;

          then x <> y by A9, Th7;

          hence thesis by A8, RELAT_1:def 10;

        end;

        then (R /\ T) = {} by RELAT_1: 37;

        hence thesis by XBOOLE_0:def 7;

      end;

      thus ((( Flow M) ~ ) | the carrier of M) misses ( id ( Elements M))

      proof

        set R = ((( Flow M) ~ ) | the carrier of M);

        for x,y be object holds not [x, y] in (R /\ T)

        proof

          let x,y be object;

          assume

           A10: [x, y] in (R /\ T);

          then

           A11: [x, y] in R by XBOOLE_0:def 4;



           A12: [x, y] in T by A10, XBOOLE_0:def 4;



           A13: [x, y] in (( Flow M) ~ ) by A11, RELAT_1:def 11;



           A14: x in the carrier of M by A11, RELAT_1:def 11;

           [y, x] in ( Flow M) by A13, RELAT_1:def 7;

          then x <> y by A14, Th7;

          hence thesis by A12, RELAT_1:def 10;

        end;

        then (R /\ T) = {} by RELAT_1: 37;

        hence thesis by XBOOLE_0:def 7;

      end;

      set R = (( Flow M) | the carrier of M);

      for x,y be object holds not [x, y] in (R /\ T)

      proof

        let x,y be object;

        assume

         A15: [x, y] in (R /\ T);

        then

         A16: [x, y] in R by XBOOLE_0:def 4;



         A17: [x, y] in T by A15, XBOOLE_0:def 4;



         A18: x in the carrier of M by A16, RELAT_1:def 11;

         [x, y] in ( Flow M) by A16, RELAT_1:def 11;

        then x <> y by A18, Th7;

        hence thesis by A17, RELAT_1:def 10;

      end;

      then (R /\ T) = {} by RELAT_1: 37;

      hence thesis by XBOOLE_0:def 7;

    end;

    theorem :: FF_SIEC:14



     Th14: ((((( Flow M) ~ ) | the carrier' of M) \/ ( id the carrier of M)) \ ( id ( Elements M))) = ((( Flow M) ~ ) | the carrier' of M) & (((( Flow M) | the carrier' of M) \/ ( id the carrier of M)) \ ( id ( Elements M))) = (( Flow M) | the carrier' of M) & ((((( Flow M) ~ ) | the carrier of M) \/ ( id the carrier of M)) \ ( id ( Elements M))) = ((( Flow M) ~ ) | the carrier of M) & (((( Flow M) | the carrier of M) \/ ( id the carrier of M)) \ ( id ( Elements M))) = (( Flow M) | the carrier of M) & ((((( Flow M) ~ ) | the carrier of M) \/ ( id the carrier' of M)) \ ( id ( Elements M))) = ((( Flow M) ~ ) | the carrier of M) & (((( Flow M) | the carrier of M) \/ ( id the carrier' of M)) \ ( id ( Elements M))) = (( Flow M) | the carrier of M) & ((((( Flow M) ~ ) | the carrier' of M) \/ ( id the carrier' of M)) \ ( id ( Elements M))) = ((( Flow M) ~ ) | the carrier' of M) & (((( Flow M) | the carrier' of M) \/ ( id the carrier' of M)) \ ( id ( Elements M))) = (( Flow M) | the carrier' of M)

    proof



       A1: ((((( Flow M) ~ ) | the carrier' of M) \/ ( id the carrier of M)) \ ( id ( Elements M))) = ((( Flow M) ~ ) | the carrier' of M)

      proof

        set R = ((( Flow M) ~ ) | the carrier' of M);

        set S = ( id the carrier of M);

        set T = ( id ( Elements M));



         A2: S c= T by SYSREL: 15, XBOOLE_1: 7;



         A3: R misses T by Th13;

        ((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: (((( Flow M) | the carrier' of M) \/ ( id the carrier of M)) \ ( id ( Elements M))) = (( Flow M) | the carrier' of M)

      proof

        set R = (( Flow M) | the carrier' of M);

        set S = ( id the carrier of M);

        set T = ( id ( Elements M));



         A5: S c= T by SYSREL: 15, XBOOLE_1: 7;



         A6: R misses T by Th13;

        ((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: ((((( Flow M) ~ ) | the carrier of M) \/ ( id the carrier of M)) \ ( id ( Elements M))) = ((( Flow M) ~ ) | the carrier of M)

      proof

        set R = ((( Flow M) ~ ) | the carrier of M);

        set S = ( id the carrier of M);

        set T = ( id ( Elements M));



         A8: S c= T by SYSREL: 15, XBOOLE_1: 7;



         A9: R misses T by Th13;

        ((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: (((( Flow M) | the carrier of M) \/ ( id the carrier of M)) \ ( id ( Elements M))) = (( Flow M) | the carrier of M)

      proof

        set R = (( Flow M) | the carrier of M);

        set S = ( id the carrier of M);

        set T = ( id ( Elements M));



         A11: S c= T by SYSREL: 15, XBOOLE_1: 7;



         A12: R misses T by Th13;

        ((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: ((((( Flow M) ~ ) | the carrier of M) \/ ( id the carrier' of M)) \ ( id ( Elements M))) = ((( Flow M) ~ ) | the carrier of M)

      proof

        set R = ((( Flow M) ~ ) | the carrier of M);

        set S = ( id the carrier' of M);

        set T = ( id ( Elements M));



         A14: S c= T by SYSREL: 15, XBOOLE_1: 7;



         A15: R misses T by Th13;

        ((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: (((( Flow M) | the carrier of M) \/ ( id the carrier' of M)) \ ( id ( Elements M))) = (( Flow M) | the carrier of M)

      proof

        set R = (( Flow M) | the carrier of M);

        set S = ( id the carrier' of M);

        set T = ( id ( Elements M));



         A17: S c= T by SYSREL: 15, XBOOLE_1: 7;



         A18: R misses T by Th13;

        ((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: ((((( Flow M) ~ ) | the carrier' of M) \/ ( id the carrier' of M)) \ ( id ( Elements M))) = ((( Flow M) ~ ) | the carrier' of M)

      proof

        set R = ((( Flow M) ~ ) | the carrier' of M);

        set S = ( id the carrier' of M);

        set T = ( id ( Elements M));



         A20: S c= T by SYSREL: 15, XBOOLE_1: 7;



         A21: R misses T by Th13;

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

      (((( Flow M) | the carrier' of M) \/ ( id the carrier' of M)) \ ( id ( Elements M))) = (( Flow M) | the carrier' of M)

      proof

        set R = (( Flow M) | the carrier' of M);

        set S = ( id the carrier' of M);

        set T = ( id ( Elements M));



         A22: S c= T by SYSREL: 15, XBOOLE_1: 7;



         A23: R misses T by Th13;

        ((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 :: FF_SIEC:15



     Th15: ((( Flow M) | the carrier of M) ~ ) = ((( Flow M) ~ ) | the carrier' of M) & ((( Flow M) | the carrier' of M) ~ ) = ((( Flow M) ~ ) | the carrier of M)

    proof

      set R = ( Flow M);

      set X = the carrier of M;

      set Y = the carrier' of M;

      for x,y be object holds [x, y] in ((R | X) ~ ) implies [x, y] in ((R ~ ) | Y)

      proof

        let x,y be object;

        assume [x, y] in ((R | X) ~ );

        then

         A1: [y, x] in (R | X) by RELAT_1:def 7;

        then

         A2: [y, x] in R by RELAT_1:def 11;



         A3: y in X by A1, RELAT_1:def 11;



         A4: [x, y] in (R ~ ) by A2, RELAT_1:def 7;

        x in Y by A2, A3, Th7;

        hence thesis by A4, RELAT_1:def 11;

      end;

      then

       A5: ((R | X) ~ ) c= ((R ~ ) | Y) by RELAT_1:def 3;

      for x,y be object holds [x, y] in ((R ~ ) | Y) implies [x, y] in ((R | X) ~ )

      proof

        let x,y be object;

        assume

         A6: [x, y] in ((R ~ ) | Y);

        then [x, y] in (R ~ ) by RELAT_1:def 11;

        then

         A7: [y, x] in R by RELAT_1:def 7;

        x in Y by A6, RELAT_1:def 11;

        then y in X by A7, Th7;

        then [y, x] in (R | X) by A7, RELAT_1:def 11;

        hence thesis by RELAT_1:def 7;

      end;

      then

       A8: ((R ~ ) | Y) c= ((R | X) ~ ) by RELAT_1:def 3;

      for x,y be object holds [x, y] in ((R | Y) ~ ) implies [x, y] in ((R ~ ) | X)

      proof

        let x,y be object;

        assume [x, y] in ((R | Y) ~ );

        then

         A9: [y, x] in (R | Y) by RELAT_1:def 7;

        then

         A10: [y, x] in R by RELAT_1:def 11;



         A11: y in Y by A9, RELAT_1:def 11;



         A12: [x, y] in (R ~ ) by A10, RELAT_1:def 7;

        x in X by A10, A11, Th7;

        hence thesis by A12, RELAT_1:def 11;

      end;

      then

       A13: ((R | Y) ~ ) c= ((R ~ ) | X) by RELAT_1:def 3;

      for x,y be object holds [x, y] in ((R ~ ) | X) implies [x, y] in ((R | Y) ~ )

      proof

        let x,y be object;

        assume

         A14: [x, y] in ((R ~ ) | X);

        then [x, y] in (R ~ ) by RELAT_1:def 11;

        then

         A15: [y, x] in R by RELAT_1:def 7;

        x in X by A14, RELAT_1:def 11;

        then y in Y by A15, Th7;

        then [y, x] in (R | Y) by A15, RELAT_1:def 11;

        hence thesis by RELAT_1:def 7;

      end;

      then ((R ~ ) | X) c= ((R | Y) ~ ) by RELAT_1:def 3;

      hence thesis by A5, A8, A13, XBOOLE_0:def 10;

    end;

    theorem :: FF_SIEC:16



     Th16: ((( Flow M) | the carrier of M) \/ (( Flow M) | the carrier' of M)) = ( Flow M) & ((( Flow M) | the carrier' of M) \/ (( Flow M) | the carrier of M)) = ( Flow M) & (((( Flow M) | the carrier of M) ~ ) \/ ((( Flow M) | the carrier' of M) ~ )) = (( Flow M) ~ ) & (((( Flow M) | the carrier' of M) ~ ) \/ ((( Flow M) | the carrier of M) ~ )) = (( Flow M) ~ )

    proof

      set R = ( Flow M);

      ( Flow M) c= [:( Elements M), ( Elements M):] by Th8;

      then ((R | the carrier of M) \/ (R | the carrier' of M)) = R by SYSREL: 9;

      hence thesis by RELAT_1: 23;

    end;

    definition

      let M;

      :: FF_SIEC:def7

      func f_enter (M) -> Relation equals (((( Flow M) ~ ) | the carrier' of M) \/ ( id the carrier of M));

      correctness ;

      :: FF_SIEC:def8

      func f_exit (M) -> Relation equals ((( Flow M) | the carrier' of M) \/ ( id the carrier of M));

      correctness ;

    end

    theorem :: FF_SIEC:17

    ( f_exit M) c= [:( Elements M), ( Elements M):] & ( f_enter M) c= [:( Elements M), ( Elements M):]

    proof



       A1: ( id the carrier of M) c= ( id ( Elements M)) by SYSREL: 15, XBOOLE_1: 7;

      ( id ( Elements M)) c= [:( Elements M), ( Elements M):] by RELSET_1: 13;

      then

       A2: ( id the carrier of M) c= [:( Elements M), ( Elements M):] by A1, XBOOLE_1: 1;



       A3: (( Flow M) | the carrier' of M) c= ( Flow M) by RELAT_1: 59;

      ( Flow M) c= [:( Elements M), ( Elements M):] by Th8;

      then (( Flow M) | the carrier' of M) c= [:( Elements M), ( Elements M):] by A3, XBOOLE_1: 1;

      hence ( f_exit M) c= [:( Elements M), ( Elements M):] by A2, XBOOLE_1: 8;



       A4: ( id the carrier of M) c= ( id ( Elements M)) by SYSREL: 15, XBOOLE_1: 7;

      ( id ( Elements M)) c= [:( Elements M), ( Elements M):] by RELSET_1: 13;

      then

       A5: ( id the carrier of M) c= [:( Elements M), ( Elements M):] by A4, XBOOLE_1: 1;



       A6: ((( Flow M) ~ ) | the carrier' of M) c= (( Flow M) ~ ) by RELAT_1: 59;

      (( Flow M) ~ ) c= [:( Elements M), ( Elements M):] by Th8;

      then ((( Flow M) ~ ) | the carrier' of M) c= [:( Elements M), ( Elements M):] by A6, XBOOLE_1: 1;

      hence thesis by A5, XBOOLE_1: 8;

    end;

    theorem :: FF_SIEC:18

    ( 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 be object holds x in ( dom ( f_exit M)) implies x in ( Elements M)

      proof

        let x be object;

        assume x in ( dom ( f_exit M));

        then x in (( dom (( Flow M) | the carrier' of M)) \/ ( dom ( id the carrier of M))) by XTUPLE_0: 23;

        then x in ( dom (( Flow M) | the carrier' of M)) or x in ( dom ( id the carrier of M)) by XBOOLE_0:def 3;

        then x in the carrier' of M or x in the carrier of M by RELAT_1: 57;

        hence thesis by XBOOLE_0:def 3;

      end;



       A2: for x be object holds x in ( rng ( f_exit M)) implies x in ( Elements M)

      proof

        let x be object;

        assume x in ( rng ( f_exit M));

        then

         A3: x in (( rng (( Flow M) | the carrier' of M)) \/ ( rng ( id the carrier of M))) by RELAT_1: 12;



         A4: x in ( rng (( Flow M) | the carrier' of M)) implies thesis

        proof

          assume x in ( rng (( Flow M) | the carrier' of M));

          then

          consider y be object such that

           A5: [y, x] in (( Flow M) | the carrier' of M) by XTUPLE_0:def 13;



           A6: y in the carrier' of M by A5, RELAT_1:def 11;

           [y, x] in ( Flow M) by A5, RELAT_1:def 11;

          then x in the carrier' of M or x in the carrier of M by A6, Th7;

          hence thesis by XBOOLE_0:def 3;

        end;

        x in ( rng ( id the carrier of M)) implies thesis by XBOOLE_0:def 3;

        hence thesis by A3, A4, XBOOLE_0:def 3;

      end;



       A7: for x be object holds x in ( dom ( f_enter M)) implies x in ( Elements M)

      proof

        let x be object;

        assume x in ( dom ( f_enter M));

        then x in (( dom ((( Flow M) ~ ) | the carrier' of M)) \/ ( dom ( id the carrier of M))) by XTUPLE_0: 23;

        then x in ( dom ((( Flow M) ~ ) | the carrier' of M)) or x in ( dom ( id the carrier of M)) by XBOOLE_0:def 3;

        then x in the carrier' of M or x in the carrier of M by RELAT_1: 57;

        hence thesis by XBOOLE_0:def 3;

      end;

      for x be object holds x in ( rng ( f_enter M)) implies x in ( Elements M)

      proof

        let x be object;

        assume x in ( rng ( f_enter M));

        then

         A8: x in (( rng ((( Flow M) ~ ) | the carrier' of M)) \/ ( rng ( id the carrier of M))) by RELAT_1: 12;



         A9: x in ( rng ((( Flow M) ~ ) | the carrier' of M)) implies thesis

        proof

          assume x in ( rng ((( Flow M) ~ ) | the carrier' of M));

          then

          consider y be object such that

           A10: [y, x] in ((( Flow M) ~ ) | the carrier' of M) by XTUPLE_0:def 13;



           A11: [y, x] in (( Flow M) ~ ) by A10, RELAT_1:def 11;



           A12: y in the carrier' of M by A10, RELAT_1:def 11;

           [x, y] in ( Flow M) by A11, RELAT_1:def 7;

          then x in the carrier' of M or x in the carrier of M by A12, Th7;

          hence thesis by XBOOLE_0:def 3;

        end;

        x in ( rng ( id the carrier of M)) implies thesis by XBOOLE_0:def 3;

        hence thesis by A8, A9, XBOOLE_0:def 3;

      end;

      hence thesis by A1, A2, A7, TARSKI:def 3;

    end;

    theorem :: FF_SIEC:19

    (( 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 = (( Flow M) | the carrier' of M);

        set S = ( id the carrier of M);



         A2: (S * R) = {} by Th12;



         A3: (R * S) = R by Th12;



         A4: (S * S) = S by SYSREL: 12;

        (( f_exit M) * ( f_exit M)) = ((R * (R \/ S)) \/ (S * (R \/ S))) by SYSREL: 6

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

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

        .= (( {} \/ R) \/ ( {} \/ S)) by A2, A3, A4, Th11

        .= ( f_exit M);

        hence thesis;

      end;



       A5: (( f_exit M) * ( f_enter M)) = ( f_exit M)

      proof

        set R = (( Flow M) | the carrier' of M);

        set S = ( id the carrier of M);

        set T = ((( Flow M) ~ ) | the carrier' of M);



         A6: (S * T) = {} by Th12;



         A7: (R * S) = R by Th12;



         A8: (S * S) = S by SYSREL: 12;

        (( f_exit M) * ( f_enter M)) = ((R * (T \/ S)) \/ (S * (T \/ S))) by SYSREL: 6

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

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

        .= (( {} \/ R) \/ ( {} \/ S)) by A6, A7, A8, Th11

        .= ( f_exit M);

        hence thesis;

      end;



       A9: (( f_enter M) * ( f_enter M)) = ( f_enter M)

      proof

        set R = ((( Flow M) ~ ) | the carrier' of M);

        set S = ( id the carrier of M);



         A10: (S * R) = {} by Th12;



         A11: (R * S) = R by Th12;



         A12: (S * S) = S by SYSREL: 12;

        (( f_enter M) * ( f_enter M)) = ((R * (R \/ S)) \/ (S * (R \/ S))) by SYSREL: 6

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

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

        .= (( {} \/ R) \/ ( {} \/ S)) by A10, A11, A12, Th11

        .= ( f_enter M);

        hence thesis;

      end;

      (( f_enter M) * ( f_exit M)) = ( f_enter M)

      proof

        set R = (( Flow M) | the carrier' of M);

        set S = ( id the carrier of M);

        set T = ((( Flow M) ~ ) | the carrier' of M);



         A13: (T * S) = T by Th12;



         A14: (S * R) = {} by Th12;



         A15: (S * S) = S by SYSREL: 12;

        (( f_enter M) * ( f_exit M)) = ((T * (R \/ S)) \/ (S * (R \/ S))) by SYSREL: 6

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

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

        .= (( {} \/ T) \/ ( {} \/ S)) by A13, A14, A15, Th11

        .= ( f_enter M);

        hence thesis;

      end;

      hence thesis by A1, A5, A9;

    end;

    theorem :: FF_SIEC:20

    (( f_exit M) * (( f_exit M) \ ( id ( Elements M)))) = {} & (( f_enter M) * (( f_enter M) \ ( id ( Elements M)))) = {}

    proof

      set S = ( id the carrier of M);

      thus (( f_exit M) * (( f_exit M) \ ( id ( Elements M)))) = {}

      proof

        set R = (( Flow M) | the carrier' of M);



         A1: (S * R) = {} by Th12;

        (( f_exit M) * (( f_exit M) \ ( id ( Elements M)))) = ((R \/ S) * R) by Th14

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

        .= {} by A1, Th11;

        hence thesis;

      end;

      set R = ((( Flow M) ~ ) | the carrier' of M);



       A2: (S * R) = {} by Th12;

      (( f_enter M) * (( f_enter M) \ ( id ( Elements M)))) = ((R \/ S) * R) by Th14

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

      .= {} by A2, Th11;

      hence thesis;

    end;

    definition

      let M;

      :: FF_SIEC:def9

      func f_prox (M) -> Relation equals (((( Flow M) | the carrier of M) \/ ((( Flow M) ~ ) | the carrier of M)) \/ ( id the carrier of M));

      correctness ;

      :: FF_SIEC:def10

      func f_flow (M) -> Relation equals (( Flow M) \/ ( id ( Elements M)));

      correctness ;

    end

    theorem :: FF_SIEC:21

    (( 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 = (( Flow M) | the carrier of M);

      set S = ((( Flow M) ~ ) | the carrier of M);

      set T = ( id the carrier of M);

      set Q = ( id ( Elements M));



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

      .= (R \/ S) by Th14;



       A2: ((R \/ S) * (R \/ S)) = (((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

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

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

      .= (( {} \/ {} ) \/ ( {} \/ (S * S))) by Th11

      .= {} by Th11;



       A3: (R \/ (S ~ )) = (R \/ (((( Flow M) | the carrier' of M) ~ ) ~ )) by Th15

      .= ( Flow M) by Th16;



       A4: ((R ~ ) \/ S) = ((R ~ ) \/ ((( Flow M) | the carrier' of M) ~ )) by Th15

      .= (( Flow M) ~ ) by Th16;



       A5: (((R \/ S) ~ ) \/ (R \/ S)) = (((R ~ ) \/ (S ~ )) \/ (R \/ S)) by RELAT_1: 23

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

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

      .= (( Flow M) \/ (( Flow M) ~ )) by A3, A4, XBOOLE_1: 4;



       A6: (( f_prox M) \/ (( f_prox M) ~ )) = (((R \/ S) \/ T) \/ (((R \/ S) ~ ) \/ (T ~ ))) by RELAT_1: 23

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

      .= ((( Flow M) \/ (( Flow M) ~ )) \/ ( id the carrier of M)) by A5;



       A7: ( id the carrier of M) c= ( id ( Elements M)) by SYSREL: 15, XBOOLE_1: 7;



       A8: (( f_prox M) * ( f_prox M)) = ((((R \/ S) \/ T) * (R \/ S)) \/ (((R \/ S) \/ T) * T)) by RELAT_1: 32

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

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

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

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

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

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

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

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

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

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

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

      .= ((R \/ (T * S)) \/ (((R * T) \/ (S * T)) \/ (T * T))) by Th12

      .= ((R \/ S) \/ (((R * T) \/ (S * T)) \/ (T * T))) by Th12

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

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

      .= ((R \/ S) \/ ( {} \/ T)) by Th12

      .= ( f_prox M);



       A9: ((( f_prox M) \ ( id ( Elements M))) * ( f_prox M)) = ( {} \/ ((R \/ S) * T)) by A1, A2, RELAT_1: 32

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

      .= ( {} \/ (S * T)) by Th12

      .= {} by Th12;

      ((( f_prox M) \/ (( f_prox M) ~ )) \/ ( id ( Elements M))) = ((( Flow M) \/ (( Flow M) ~ )) \/ (( id the carrier of M) \/ ( id ( Elements M)))) by A6, XBOOLE_1: 4

      .= ((( Flow M) \/ (( Flow M) ~ )) \/ ( id ( Elements M))) by A7, XBOOLE_1: 12

      .= ((( Flow M) \/ ( id ( Elements M))) \/ ((( Flow M) ~ ) \/ ( id ( Elements M)))) by XBOOLE_1: 5

      .= ((( Flow M) \/ ( id ( Elements M))) \/ ((( Flow M) ~ ) \/ (( id ( Elements M)) ~ )))

      .= (( f_flow M) \/ (( f_flow M) ~ )) by RELAT_1: 23;

      hence thesis by A8, A9;

    end;

    definition

      let M;

      :: FF_SIEC:def11

      func f_places (M) -> set equals the carrier of M;

      correctness ;

      :: FF_SIEC:def12

      func f_transitions (M) -> set equals the carrier' of M;

      correctness ;

      :: FF_SIEC:def13

      func f_pre (M) -> Relation equals (( Flow M) | the carrier' of M);

      correctness ;

      :: FF_SIEC:def14

      func f_post (M) -> Relation equals ((( Flow M) ~ ) | the carrier' of M);

      correctness ;

    end

    theorem :: FF_SIEC:22

    ( 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 be object holds [x, y] in ( f_pre M) implies [x, y] in [:( f_transitions M), ( f_places M):]

      proof

        let x,y be object;

        assume

         A2: [x, y] in ( f_pre M);

        then

         A3: x in the carrier' of M by RELAT_1:def 11;

         [x, y] in ( Flow M) by A2, RELAT_1:def 11;

        then y in the carrier of M by A3, Th7;

        hence thesis by A3, ZFMISC_1: 87;

      end;

      for x,y be object holds [x, y] in ( f_post M) implies [x, y] in [:( f_transitions M), ( f_places M):]

      proof

        let x,y be object;

        assume

         A4: [x, y] in ( f_post M);

        then

         A5: [x, y] in (( Flow M) ~ ) by RELAT_1:def 11;



         A6: x in the carrier' of M by A4, RELAT_1:def 11;

         [y, x] in ( Flow M) by A5, RELAT_1:def 7;

        then y in the carrier of M by A6, Th7;

        hence thesis by A6, ZFMISC_1: 87;

      end;

      hence thesis by A1, RELAT_1:def 3;

    end;

    theorem :: FF_SIEC:23

    ( f_prox M) c= [:( Elements M), ( Elements M):] & ( f_flow M) c= [:( Elements M), ( Elements M):]

    proof



       A1: (( Flow M) | the carrier of M) c= ( Flow M) by RELAT_1: 59;

      ( Flow M) c= [:( Elements M), ( Elements M):] by Th8;

      then

       A2: (( Flow M) | the carrier of M) c= [:( Elements M), ( Elements M):] by A1, XBOOLE_1: 1;



       A3: ((( Flow M) ~ ) | the carrier of M) c= (( Flow M) ~ ) by RELAT_1: 59;

      (( Flow M) ~ ) c= [:( Elements M), ( Elements M):] by Th8;

      then

       A4: ((( Flow M) ~ ) | the carrier of M) c= [:( Elements M), ( Elements M):] by A3, XBOOLE_1: 1;

      the carrier of M c= ( Elements M) by XBOOLE_1: 7;

      then

       A5: [:the carrier of M, the carrier of M:] c= [:( Elements M), ( Elements M):] by ZFMISC_1: 96;

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

      then

       A6: ( id the carrier of M) c= [:( Elements M), ( Elements M):] by A5, XBOOLE_1: 1;

      ((( Flow M) | the carrier of M) \/ ((( Flow M) ~ ) | the carrier of M)) c= [:( Elements M), ( Elements M):] by A2, A4, XBOOLE_1: 8;

      hence ( f_prox M) c= [:( Elements M), ( Elements M):] by A6, XBOOLE_1: 8;



       A7: ( Flow M) c= [:( Elements M), ( Elements M):] by Th8;

      ( id ( Elements M)) c= [:( Elements M), ( Elements M):] by RELSET_1: 13;

      hence thesis by A7, XBOOLE_1: 8;

    end;

    definition

      let M;

      :: FF_SIEC:def15

      func f_entrance (M) -> Relation equals (((( Flow M) ~ ) | the carrier of M) \/ ( id the carrier' of M));

      correctness ;

      :: FF_SIEC:def16

      func f_escape (M) -> Relation equals ((( Flow M) | the carrier of M) \/ ( id the carrier' of M));

      correctness ;

    end

    theorem :: FF_SIEC:24

    ( f_escape M) c= [:( Elements M), ( Elements M):] & ( f_entrance M) c= [:( Elements M), ( Elements M):]

    proof



       A1: ( id the carrier' of M) c= ( id ( Elements M)) by SYSREL: 15, XBOOLE_1: 7;

      ( id ( Elements M)) c= [:( Elements M), ( Elements M):] by RELSET_1: 13;

      then

       A2: ( id the carrier' of M) c= [:( Elements M), ( Elements M):] by A1, XBOOLE_1: 1;



       A3: (( Flow M) | the carrier of M) c= ( Flow M) by RELAT_1: 59;

      ( Flow M) c= [:( Elements M), ( Elements M):] by Th8;

      then (( Flow M) | the carrier of M) c= [:( Elements M), ( Elements M):] by A3, XBOOLE_1: 1;

      hence ( f_escape M) c= [:( Elements M), ( Elements M):] by A2, XBOOLE_1: 8;



       A4: ( id the carrier' of M) c= ( id ( Elements M)) by SYSREL: 15, XBOOLE_1: 7;

      ( id ( Elements M)) c= [:( Elements M), ( Elements M):] by RELSET_1: 13;

      then

       A5: ( id the carrier' of M) c= [:( Elements M), ( Elements M):] by A4, XBOOLE_1: 1;



       A6: ((( Flow M) ~ ) | the carrier of M) c= (( Flow M) ~ ) by RELAT_1: 59;

      (( Flow M) ~ ) c= [:( Elements M), ( Elements M):] by Th8;

      then ((( Flow M) ~ ) | the carrier of M) c= [:( Elements M), ( Elements M):] by A6, XBOOLE_1: 1;

      hence thesis by A5, XBOOLE_1: 8;

    end;

    theorem :: FF_SIEC:25

    ( 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 be object holds x in ( dom ( f_escape M)) implies x in ( Elements M)

      proof

        let x be object;

        assume x in ( dom ( f_escape M));

        then x in (( dom (( Flow M) | the carrier of M)) \/ ( dom ( id the carrier' of M))) by XTUPLE_0: 23;

        then x in ( dom (( Flow M) | the carrier of M)) or x in ( dom ( id the carrier' of M)) by XBOOLE_0:def 3;

        then x in the carrier of M or x in the carrier' of M by RELAT_1: 57;

        hence thesis by XBOOLE_0:def 3;

      end;



       A2: for x be object holds x in ( rng ( f_escape M)) implies x in ( Elements M)

      proof

        let x be object;

        assume x in ( rng ( f_escape M));

        then

         A3: x in (( rng (( Flow M) | the carrier of M)) \/ ( rng ( id the carrier' of M))) by RELAT_1: 12;



         A4: x in ( rng (( Flow M) | the carrier of M)) implies thesis

        proof

          assume x in ( rng (( Flow M) | the carrier of M));

          then

          consider y be object such that

           A5: [y, x] in (( Flow M) | the carrier of M) by XTUPLE_0:def 13;



           A6: y in the carrier of M by A5, RELAT_1:def 11;

           [y, x] in ( Flow M) by A5, RELAT_1:def 11;

          then x in the carrier of M or x in the carrier' of M by A6, Th7;

          hence thesis by XBOOLE_0:def 3;

        end;

        x in ( rng ( id the carrier' of M)) implies thesis by XBOOLE_0:def 3;

        hence thesis by A3, A4, XBOOLE_0:def 3;

      end;



       A7: for x be object holds x in ( dom ( f_entrance M)) implies x in ( Elements M)

      proof

        let x be object;

        assume x in ( dom ( f_entrance M));

        then x in (( dom ((( Flow M) ~ ) | the carrier of M)) \/ ( dom ( id the carrier' of M))) by XTUPLE_0: 23;

        then x in ( dom ((( Flow M) ~ ) | the carrier of M)) or x in ( dom ( id the carrier' of M)) by XBOOLE_0:def 3;

        then x in the carrier of M or x in the carrier' of M by RELAT_1: 57;

        hence thesis by XBOOLE_0:def 3;

      end;

      for x be object holds x in ( rng ( f_entrance M)) implies x in ( Elements M)

      proof

        let x be object;

        assume x in ( rng ( f_entrance M));

        then

         A8: x in (( rng ((( Flow M) ~ ) | the carrier of M)) \/ ( rng ( id the carrier' of M))) by RELAT_1: 12;



         A9: x in ( rng ((( Flow M) ~ ) | the carrier of M)) implies thesis

        proof

          assume x in ( rng ((( Flow M) ~ ) | the carrier of M));

          then

          consider y be object such that

           A10: [y, x] in ((( Flow M) ~ ) | the carrier of M) by XTUPLE_0:def 13;



           A11: [y, x] in (( Flow M) ~ ) by A10, RELAT_1:def 11;



           A12: y in the carrier of M by A10, RELAT_1:def 11;

           [x, y] in ( Flow M) by A11, RELAT_1:def 7;

          then x in the carrier of M or x in the carrier' of M by A12, Th7;

          hence thesis by XBOOLE_0:def 3;

        end;

        x in ( rng ( id the carrier' of M)) implies thesis by XBOOLE_0:def 3;

        hence thesis by A8, A9, XBOOLE_0:def 3;

      end;

      hence thesis by A1, A2, A7, TARSKI:def 3;

    end;

    theorem :: FF_SIEC:26

    (( 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 = (( Flow M) | the carrier of M);

      set S = ( id the carrier' of M);



       A1: (S * R) = {} by Th12;



       A2: (R * S) = R by Th12;



       A3: (S * S) = S by SYSREL: 12;



       A4: (( f_escape M) * ( f_escape M)) = ((R * (R \/ S)) \/ (S * (R \/ S))) by SYSREL: 6

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

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

      .= (( {} \/ R) \/ ( {} \/ S)) by A1, A2, A3, Th11

      .= ( f_escape M);



       A5: (( f_escape M) * ( f_entrance M)) = ( f_escape M)

      proof

        set T = ((( Flow M) ~ ) | the carrier of M);



         A6: (S * T) = {} by Th12;



         A7: (R * S) = R by Th12;



         A8: (S * S) = S by SYSREL: 12;

        (( f_escape M) * ( f_entrance M)) = ((R * (T \/ S)) \/ (S * (T \/ S))) by SYSREL: 6

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

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

        .= (( {} \/ R) \/ ( {} \/ S)) by A6, A7, A8, Th11

        .= ( f_escape M);

        hence thesis;

      end;



       A9: (( f_entrance M) * ( f_entrance M)) = ( f_entrance M)

      proof

        set R = ((( Flow M) ~ ) | the carrier of M);



         A10: (S * R) = {} by Th12;



         A11: (R * S) = R by Th12;



         A12: (S * S) = S by SYSREL: 12;

        (( f_entrance M) * ( f_entrance M)) = ((R * (R \/ S)) \/ (S * (R \/ S))) by SYSREL: 6

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

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

        .= (( {} \/ R) \/ ( {} \/ S)) by A10, A11, A12, Th11

        .= ( f_entrance M);

        hence thesis;

      end;

      (( f_entrance M) * ( f_escape M)) = ( f_entrance M)

      proof

        set T = ((( Flow M) ~ ) | the carrier of M);



         A13: (T * S) = T by Th12;



         A14: (S * R) = {} by Th12;



         A15: (S * S) = S by SYSREL: 12;

        (( f_entrance M) * ( f_escape M)) = ((T * (R \/ S)) \/ (S * (R \/ S))) by SYSREL: 6

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

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

        .= (( {} \/ T) \/ ( {} \/ S)) by A13, A14, A15, Th11

        .= ( f_entrance M);

        hence thesis;

      end;

      hence thesis by A4, A5, A9;

    end;

    theorem :: FF_SIEC:27

    (( f_escape M) * (( f_escape M) \ ( id ( Elements M)))) = {} & (( f_entrance M) * (( f_entrance M) \ ( id ( Elements M)))) = {}

    proof

      set R = (( Flow M) | the carrier of M);

      set S = ( id the carrier' of M);



       A1: (S * R) = {} by Th12;

      (( f_escape M) * (( f_escape M) \ ( id ( Elements M)))) = ((R \/ S) * R) by Th14

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

      .= {} by A1, Th11;

      hence (( f_escape M) * (( f_escape M) \ ( id ( Elements M)))) = {} ;

      set R = ((( Flow M) ~ ) | the carrier of M);



       A2: (S * R) = {} by Th12;

      (( f_entrance M) * (( f_entrance M) \ ( id ( Elements M)))) = ((R \/ S) * R) by Th14

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

      .= {} by A2, Th11;

      hence thesis;

    end;

    notation

      let M;

      synonym f_circulation (M) for f_flow (M);

    end

    definition

      let M;

      :: FF_SIEC:def17

      func f_adjac (M) -> Relation equals (((( Flow M) | the carrier' of M) \/ ((( Flow M) ~ ) | the carrier' of M)) \/ ( id the carrier' of M));

      correctness ;

    end

    theorem :: FF_SIEC:28

    (( 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 = (( Flow M) | the carrier' of M);

      set S = ((( Flow M) ~ ) | the carrier' of M);

      set T = ( id the carrier' of M);

      set Q = ( id ( Elements M));



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

      .= (R \/ S) by Th14;



       A2: ((R \/ S) * (R \/ S)) = (((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

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

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

      .= (( {} \/ {} ) \/ ( {} \/ (S * S))) by Th11

      .= {} by Th11;



       A3: (R \/ (S ~ )) = (R \/ (((( Flow M) | the carrier of M) ~ ) ~ )) by Th15

      .= ( Flow M) by Th16;



       A4: ((R ~ ) \/ S) = ((R ~ ) \/ ((( Flow M) | the carrier of M) ~ )) by Th15

      .= (( Flow M) ~ ) by Th16;



       A5: (((R \/ S) ~ ) \/ (R \/ S)) = (((R ~ ) \/ (S ~ )) \/ (R \/ S)) by RELAT_1: 23

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

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

      .= (( Flow M) \/ (( Flow M) ~ )) by A3, A4, XBOOLE_1: 4;



       A6: (( f_adjac M) \/ (( f_adjac M) ~ )) = (((R \/ S) \/ T) \/ (((R \/ S) ~ ) \/ (T ~ ))) by RELAT_1: 23

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

      .= ((( Flow M) \/ (( Flow M) ~ )) \/ ( id the carrier' of M)) by A5;



       A7: ( id the carrier' of M) c= ( id ( Elements M)) by SYSREL: 15, XBOOLE_1: 7;



       A8: (( f_adjac M) * ( f_adjac M)) = ((((R \/ S) \/ T) * (R \/ S)) \/ (((R \/ S) \/ T) * T)) by RELAT_1: 32

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

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

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

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

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

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

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

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

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

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

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

      .= ((R \/ (T * S)) \/ (((R * T) \/ (S * T)) \/ (T * T))) by Th12

      .= ((R \/ S) \/ (((R * T) \/ (S * T)) \/ (T * T))) by Th12

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

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

      .= ((R \/ S) \/ ( {} \/ T)) by Th12

      .= ( f_adjac M);



       A9: ((( f_adjac M) \ ( id ( Elements M))) * ( f_adjac M)) = ( {} \/ ((R \/ S) * T)) by A1, A2, RELAT_1: 32

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

      .= ( {} \/ (S * T)) by Th12

      .= {} by Th12;

      ((( f_adjac M) \/ (( f_adjac M) ~ )) \/ ( id ( Elements M))) = ((( Flow M) \/ (( Flow M) ~ )) \/ (( id the carrier' of M) \/ ( id ( Elements M)))) by A6, XBOOLE_1: 4

      .= ((( Flow M) \/ (( Flow M) ~ )) \/ ( id ( Elements M))) by A7, XBOOLE_1: 12

      .= ((( Flow M) \/ ( id ( Elements M))) \/ ((( Flow M) ~ ) \/ ( id ( Elements M)))) by XBOOLE_1: 5

      .= ((( Flow M) \/ ( id ( Elements M))) \/ ((( Flow M) ~ ) \/ (( id ( Elements M)) ~ )))

      .= (( f_circulation M) \/ (( f_circulation M) ~ )) by RELAT_1: 23;

      hence thesis by A8, A9;

    end;