bvfunc_4.miz



    begin

    reserve Y for non empty set;

    theorem :: BVFUNC_4:1

    for a,b,c be Function of Y, BOOLEAN holds a '<' (b 'imp' c) implies (a '&' b) '<' c

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      assume

       A1: a '<' (b 'imp' c);

      for x be Element of Y holds (((a '&' b) 'imp' c) . x) = TRUE

      proof

        let x be Element of Y;

        

         A2: ((a 'imp' (b 'imp' c)) . x) = (( 'not' (a . x)) 'or' ((b 'imp' c) . x)) by BVFUNC_1:def 8

        .= (( 'not' (a . x)) 'or' (( 'not' (b . x)) 'or' (c . x))) by BVFUNC_1:def 8

        .= ((( 'not' (a . x)) 'or' ( 'not' (b . x))) 'or' (c . x));

        

         A3: (((a '&' b) 'imp' c) . x) = (( 'not' ((a '&' b) . x)) 'or' (c . x)) by BVFUNC_1:def 8

        .= ((( 'not' (a . x)) 'or' ( 'not' (b . x))) 'or' (c . x)) by MARGREL1:def 20;

        (a 'imp' (b 'imp' c)) = ( I_el Y) by A1, BVFUNC_1: 16;

        hence thesis by A2, A3, BVFUNC_1:def 11;

      end;

      then ((a '&' b) 'imp' c) = ( I_el Y) by BVFUNC_1:def 11;

      hence thesis by BVFUNC_1: 16;

    end;

    theorem :: BVFUNC_4:2

    for a,b,c be Function of Y, BOOLEAN holds (a '&' b) '<' c implies a '<' (b 'imp' c)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      assume

       A1: (a '&' b) '<' c;

      for x be Element of Y holds ((a 'imp' (b 'imp' c)) . x) = TRUE

      proof

        let x be Element of Y;

        

         A2: ((a 'imp' (b 'imp' c)) . x) = (( 'not' (a . x)) 'or' ((b 'imp' c) . x)) by BVFUNC_1:def 8

        .= (( 'not' (a . x)) 'or' (( 'not' (b . x)) 'or' (c . x))) by BVFUNC_1:def 8

        .= ((( 'not' (a . x)) 'or' ( 'not' (b . x))) 'or' (c . x));

        

         A3: (((a '&' b) 'imp' c) . x) = (( 'not' ((a '&' b) . x)) 'or' (c . x)) by BVFUNC_1:def 8

        .= ((( 'not' (a . x)) 'or' ( 'not' (b . x))) 'or' (c . x)) by MARGREL1:def 20;

        ((a '&' b) 'imp' c) = ( I_el Y) by A1, BVFUNC_1: 16;

        hence thesis by A2, A3, BVFUNC_1:def 11;

      end;

      then (a 'imp' (b 'imp' c)) = ( I_el Y) by BVFUNC_1:def 11;

      hence thesis by BVFUNC_1: 16;

    end;

    theorem :: BVFUNC_4:3

    for a,b be Function of Y, BOOLEAN holds (a 'or' (a '&' b)) = a

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

      thus ((a 'or' (a '&' b)) . x) = ((a . x) 'or' ((a '&' b) . x)) by BVFUNC_1:def 4

      .= ((a . x) 'or' ((a . x) '&' (b . x))) by MARGREL1:def 20

      .= (a . x) by XBOOLEAN: 5;

    end;

    theorem :: BVFUNC_4:4

    for a,b be Function of Y, BOOLEAN holds (a '&' (a 'or' b)) = a

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

      thus ((a '&' (a 'or' b)) . x) = ((a . x) '&' ((a 'or' b) . x)) by MARGREL1:def 20

      .= ((a . x) '&' ((a . x) 'or' (b . x))) by BVFUNC_1:def 4

      .= (a . x) by XBOOLEAN: 6;

    end;

    theorem :: BVFUNC_4:5

    

     Th5: for a be Function of Y, BOOLEAN holds (a '&' ( 'not' a)) = ( O_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

      thus ((a '&' ( 'not' a)) . x) = ((a . x) '&' (( 'not' a) . x)) by MARGREL1:def 20

      .= ((a . x) '&' ( 'not' (a . x))) by MARGREL1:def 19

      .= FALSE by XBOOLEAN: 138

      .= (( O_el Y) . x) by BVFUNC_1:def 10;

    end;

    theorem :: BVFUNC_4:6

    for a be Function of Y, BOOLEAN holds (a 'or' ( 'not' a)) = ( I_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

      thus ((a 'or' ( 'not' a)) . x) = ((a . x) 'or' (( 'not' a) . x)) by BVFUNC_1:def 4

      .= ((a . x) 'or' ( 'not' (a . x))) by MARGREL1:def 19

      .= TRUE by XBOOLEAN: 102

      .= (( I_el Y) . x) by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_4:7

    

     Th7: for a,b be Function of Y, BOOLEAN holds (a 'eqv' b) = ((a 'imp' b) '&' (b 'imp' a))

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

      thus ((a 'eqv' b) . x) = ((a . x) <=> (b . x)) by BVFUNC_1:def 9

      .= (((a . x) => (b . x)) '&' ((b . x) => (a . x)))

      .= (((a 'imp' b) . x) '&' ((b . x) => (a . x))) by BVFUNC_1:def 8

      .= (((a 'imp' b) . x) '&' ((b 'imp' a) . x)) by BVFUNC_1:def 8

      .= (((a 'imp' b) '&' (b 'imp' a)) . x) by MARGREL1:def 20;

    end;

    theorem :: BVFUNC_4:8

    

     Th8: for a,b be Function of Y, BOOLEAN holds (a 'imp' b) = (( 'not' a) 'or' b)

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

      thus ((a 'imp' b) . x) = ((a . x) => (b . x)) by BVFUNC_1:def 8

      .= (( 'not' (a . x)) 'or' (b . x))

      .= ((( 'not' a) . x) 'or' (b . x)) by MARGREL1:def 19

      .= ((( 'not' a) 'or' b) . x) by BVFUNC_1:def 4;

    end;

    theorem :: BVFUNC_4:9

    for a,b be Function of Y, BOOLEAN holds (a 'xor' b) = ((( 'not' a) '&' b) 'or' (a '&' ( 'not' b)))

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

      thus ((a 'xor' b) . x) = ((a . x) 'xor' (b . x)) by BVFUNC_1:def 5

      .= ((( 'not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ( 'not' (b . x))))

      .= ((( 'not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' (( 'not' b) . x))) by MARGREL1:def 19

      .= (((( 'not' a) . x) '&' (b . x)) 'or' ((a . x) '&' (( 'not' b) . x))) by MARGREL1:def 19

      .= (((( 'not' a) '&' b) . x) 'or' ((a . x) '&' (( 'not' b) . x))) by MARGREL1:def 20

      .= (((( 'not' a) '&' b) . x) 'or' ((a '&' ( 'not' b)) . x)) by MARGREL1:def 20

      .= (((( 'not' a) '&' b) 'or' (a '&' ( 'not' b))) . x) by BVFUNC_1:def 4;

    end;

    theorem :: BVFUNC_4:10

    

     Th10: for a,b be Function of Y, BOOLEAN holds (a 'eqv' b) = ( I_el Y) iff (a 'imp' b) = ( I_el Y) & (b 'imp' a) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      thus (a 'eqv' b) = ( I_el Y) implies (a 'imp' b) = ( I_el Y) & (b 'imp' a) = ( I_el Y)

      proof

        assume (a 'eqv' b) = ( I_el Y);

        then a = b by BVFUNC_1: 17;

        hence thesis by BVFUNC_1: 16;

      end;

      assume (a 'imp' b) = ( I_el Y) & (b 'imp' a) = ( I_el Y);

      then (a 'eqv' b) = (( I_el Y) '&' ( I_el Y)) by Th7;

      hence thesis;

    end;

    theorem :: BVFUNC_4:11

    for a,b be Function of Y, BOOLEAN holds (a 'eqv' b) = ( I_el Y) implies (( 'not' a) 'eqv' ( 'not' b)) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      assume (a 'eqv' b) = ( I_el Y);

      then a = b by BVFUNC_1: 17;

      hence thesis by BVFUNC_1: 17;

    end;

    theorem :: BVFUNC_4:12

    for a,b,c,d be Function of Y, BOOLEAN holds (a 'eqv' b) = ( I_el Y) & (c 'eqv' d) = ( I_el Y) implies ((a '&' c) 'eqv' (b '&' d)) = ( I_el Y)

    proof

      let a,b,c,d be Function of Y, BOOLEAN ;

      assume (a 'eqv' b) = ( I_el Y) & (c 'eqv' d) = ( I_el Y);

      then a = b & c = d by BVFUNC_1: 17;

      hence thesis by BVFUNC_1: 17;

    end;

    theorem :: BVFUNC_4:13

    for a,b,c,d be Function of Y, BOOLEAN holds (a 'eqv' b) = ( I_el Y) & (c 'eqv' d) = ( I_el Y) implies ((a 'imp' c) 'eqv' (b 'imp' d)) = ( I_el Y)

    proof

      let a,b,c,d be Function of Y, BOOLEAN ;

      assume (a 'eqv' b) = ( I_el Y) & (c 'eqv' d) = ( I_el Y);

      then a = b & c = d by BVFUNC_1: 17;

      hence thesis by BVFUNC_1: 17;

    end;

    theorem :: BVFUNC_4:14

    for a,b,c,d be Function of Y, BOOLEAN holds (a 'eqv' b) = ( I_el Y) & (c 'eqv' d) = ( I_el Y) implies ((a 'or' c) 'eqv' (b 'or' d)) = ( I_el Y)

    proof

      let a,b,c,d be Function of Y, BOOLEAN ;

      assume (a 'eqv' b) = ( I_el Y) & (c 'eqv' d) = ( I_el Y);

      then a = b & c = d by BVFUNC_1: 17;

      hence thesis by BVFUNC_1: 17;

    end;

    theorem :: BVFUNC_4:15

    for a,b,c,d be Function of Y, BOOLEAN holds (a 'eqv' b) = ( I_el Y) & (c 'eqv' d) = ( I_el Y) implies ((a 'eqv' c) 'eqv' (b 'eqv' d)) = ( I_el Y)

    proof

      let a,b,c,d be Function of Y, BOOLEAN ;

      assume (a 'eqv' b) = ( I_el Y) & (c 'eqv' d) = ( I_el Y);

      then a = b & c = d by BVFUNC_1: 17;

      hence thesis by BVFUNC_1: 17;

    end;

    begin

    theorem :: BVFUNC_4:16

    for a,b be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y holds ( All ((a 'eqv' b),PA,G)) = (( All ((a 'imp' b),PA,G)) '&' ( All ((b 'imp' a),PA,G)))

    proof

      let a,b be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      let z be Element of Y;

      (( All ((a 'eqv' b),PA,G)) . z) = (( All (((a 'imp' b) '&' (b 'imp' a)),PA,G)) . z) by Th7

      .= ((( All ((a 'imp' b),PA,G)) '&' ( All ((b 'imp' a),PA,G))) . z) by BVFUNC_1: 39;

      hence thesis;

    end;

    theorem :: BVFUNC_4:17

    for a be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA,PB be a_partition of Y holds ( All (a,PA,G)) '<' ( Ex (a,PB,G))

    proof

      let a be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA,PB be a_partition of Y;

      ( All (a,PA,G)) '<' a & a '<' ( Ex (a,PB,G)) by BVFUNC_2: 11, BVFUNC_2: 12;

      hence thesis by BVFUNC_1: 15;

    end;

    theorem :: BVFUNC_4:18

    for a,u be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y st (a 'imp' u) = ( I_el Y) holds (( All (a,PA,G)) 'imp' u) = ( I_el Y)

    proof

      let a,u be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      assume

       A1: (a 'imp' u) = ( I_el Y);

      for x be Element of Y holds ((( All (a,PA,G)) 'imp' u) . x) = TRUE

      proof

        let x be Element of Y;

        ((a 'imp' u) . x) = TRUE by A1, BVFUNC_1:def 11;

        then

         A2: (( 'not' (a . x)) 'or' (u . x)) = TRUE by BVFUNC_1:def 8;

        

         A3: ( 'not' (a . x)) = TRUE or ( 'not' (a . x)) = FALSE by XBOOLEAN:def 3;

        now

          per cases by A2, A3;

            case

             A4: ( 'not' (a . x)) = TRUE ;

            x in ( EqClass (x,( CompF (PA,G)))) by EQREL_1:def 6;

            then (( B_INF (a,( CompF (PA,G)))) . x) = FALSE by A4, BVFUNC_1:def 16;

            

            then ((( All (a,PA,G)) 'imp' u) . x) = ( TRUE 'or' (u . x)) by BVFUNC_1:def 8

            .= TRUE ;

            hence thesis;

          end;

            case (u . x) = TRUE ;

            

            then ((( All (a,PA,G)) 'imp' u) . x) = (( 'not' (( All (a,PA,G)) . x)) 'or' TRUE ) by BVFUNC_1:def 8

            .= TRUE ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_4:19

    for u be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y st u is_independent_of (PA,G) holds ( Ex (u,PA,G)) '<' u

    proof

      let u be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      assume u is_independent_of (PA,G);

      then

       A1: u is_dependent_of ( CompF (PA,G));

      for z be Element of Y holds ((( Ex (u,PA,G)) 'imp' u) . z) = TRUE

      proof

        let z be Element of Y;

        

         A2: ((( Ex (u,PA,G)) 'imp' u) . z) = (( 'not' (( Ex (u,PA,G)) . z)) 'or' (u . z)) by BVFUNC_1:def 8;

        

         A3: z in ( EqClass (z,( CompF (PA,G)))) & ( EqClass (z,( CompF (PA,G)))) in ( CompF (PA,G)) by EQREL_1:def 6;

        now

          per cases by XBOOLEAN:def 3;

            case (u . z) = TRUE ;

            hence thesis by A2;

          end;

            case (u . z) = FALSE ;

            then not ex x1 be Element of Y st x1 in ( EqClass (z,( CompF (PA,G)))) & (u . x1) = TRUE by A1, A3;

            then (( B_SUP (u,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

            hence thesis by A2;

          end;

        end;

        hence thesis;

      end;

      then (( Ex (u,PA,G)) 'imp' u) = ( I_el Y) by BVFUNC_1:def 11;

      hence thesis by BVFUNC_1: 16;

    end;

    theorem :: BVFUNC_4:20

    for u be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y st u is_independent_of (PA,G) holds u '<' ( All (u,PA,G))

    proof

      let u be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      assume u is_independent_of (PA,G);

      then

       A1: u is_dependent_of ( CompF (PA,G));

      for z be Element of Y holds ((u 'imp' ( All (u,PA,G))) . z) = TRUE

      proof

        let z be Element of Y;

        

         A2: ((u 'imp' ( All (u,PA,G))) . z) = (( 'not' (u . z)) 'or' (( All (u,PA,G)) . z)) by BVFUNC_1:def 8;

        

         A3: z in ( EqClass (z,( CompF (PA,G)))) & ( EqClass (z,( CompF (PA,G)))) in ( CompF (PA,G)) by EQREL_1:def 6;

        now

          per cases by XBOOLEAN:def 3;

            case (u . z) = FALSE ;

            hence thesis by A2;

          end;

            case (u . z) = TRUE ;

            then for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (u . x) = TRUE by A1, A3;

            then (( All (u,PA,G)) . z) = TRUE by BVFUNC_1:def 16;

            hence thesis by A2;

          end;

        end;

        hence thesis;

      end;

      then (u 'imp' ( All (u,PA,G))) = ( I_el Y) by BVFUNC_1:def 11;

      hence thesis by BVFUNC_1: 16;

    end;

    theorem :: BVFUNC_4:21

    for u be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA,PB be a_partition of Y st u is_independent_of (PB,G) holds ( All (u,PA,G)) '<' ( All (u,PB,G))

    proof

      let u be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA,PB be a_partition of Y;

      assume u is_independent_of (PB,G);

      then

       A1: u is_dependent_of ( CompF (PB,G));

      for z be Element of Y holds ((( All (u,PA,G)) 'imp' ( All (u,PB,G))) . z) = TRUE

      proof

        let z be Element of Y;

        

         A2: z in ( EqClass (z,( CompF (PB,G)))) & ( EqClass (z,( CompF (PB,G)))) in ( CompF (PB,G)) by EQREL_1:def 6;

        

         A3: ((( All (u,PA,G)) 'imp' ( All (u,PB,G))) . z) = (( 'not' (( All (u,PA,G)) . z)) 'or' (( All (u,PB,G)) . z)) by BVFUNC_1:def 8;

        

         A4: z in ( EqClass (z,( CompF (PA,G)))) by EQREL_1:def 6;

        now

          per cases by XBOOLEAN:def 3;

            case (( All (u,PA,G)) . z) = FALSE ;

            hence thesis by A3;

          end;

            case (( All (u,PA,G)) . z) = TRUE ;

            then (u . z) = TRUE by A4, BVFUNC_1:def 16;

            then for x be Element of Y st x in ( EqClass (z,( CompF (PB,G)))) holds (u . x) = TRUE by A1, A2;

            then (( All (u,PB,G)) . z) = TRUE by BVFUNC_1:def 16;

            hence thesis by A3;

          end;

        end;

        hence thesis;

      end;

      then (( All (u,PA,G)) 'imp' ( All (u,PB,G))) = ( I_el Y) by BVFUNC_1:def 11;

      hence thesis by BVFUNC_1: 16;

    end;

    theorem :: BVFUNC_4:22

    for u be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA,PB be a_partition of Y st u is_independent_of (PA,G) holds ( Ex (u,PA,G)) '<' ( Ex (u,PB,G))

    proof

      let u be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA,PB be a_partition of Y;

      assume u is_independent_of (PA,G);

      then

       A1: u is_dependent_of ( CompF (PA,G));

      for z be Element of Y holds ((( Ex (u,PA,G)) 'imp' ( Ex (u,PB,G))) . z) = TRUE

      proof

        let z be Element of Y;

        

         A2: z in ( EqClass (z,( CompF (PB,G)))) by EQREL_1:def 6;

        

         A3: ((( Ex (u,PA,G)) 'imp' ( Ex (u,PB,G))) . z) = (( 'not' (( Ex (u,PA,G)) . z)) 'or' (( Ex (u,PB,G)) . z)) by BVFUNC_1:def 8;

        

         A4: z in ( EqClass (z,( CompF (PA,G)))) & ( EqClass (z,( CompF (PA,G)))) in ( CompF (PA,G)) by EQREL_1:def 6;

        now

          per cases by XBOOLEAN:def 3;

            case (( Ex (u,PB,G)) . z) = TRUE ;

            hence thesis by A3;

          end;

            case (( Ex (u,PB,G)) . z) = FALSE ;

            then (u . z) <> TRUE by A2, BVFUNC_1:def 17;

            then not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (u . x) = TRUE ) by A1, A4;

            then (( B_SUP (u,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

            hence thesis by A3;

          end;

        end;

        hence thesis;

      end;

      then (( Ex (u,PA,G)) 'imp' ( Ex (u,PB,G))) = ( I_el Y) by BVFUNC_1:def 11;

      hence thesis by BVFUNC_1: 16;

    end;

    theorem :: BVFUNC_4:23

    for a,b be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y holds ( All ((a 'eqv' b),PA,G)) '<' (( All (a,PA,G)) 'eqv' ( All (b,PA,G)))

    proof

      let a,b be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      let z be Element of Y;

      assume

       A1: (( All ((a 'eqv' b),PA,G)) . z) = TRUE ;

      

       A2: ((( All (a,PA,G)) 'eqv' ( All (b,PA,G))) . z) = ( 'not' ((( All (a,PA,G)) . z) 'xor' (( All (b,PA,G)) . z))) by BVFUNC_1:def 9

      .= ((((( All (a,PA,G)) . z) 'or' ( 'not' (( All (b,PA,G)) . z))) '&' ( 'not' (( All (a,PA,G)) . z))) 'or' (((( All (a,PA,G)) . z) 'or' ( 'not' (( All (b,PA,G)) . z))) '&' (( All (b,PA,G)) . z))) by XBOOLEAN: 8

      .= (((( 'not' (( All (a,PA,G)) . z)) '&' (( All (a,PA,G)) . z)) 'or' (( 'not' (( All (a,PA,G)) . z)) '&' ( 'not' (( All (b,PA,G)) . z)))) 'or' ((( All (b,PA,G)) . z) '&' ((( All (a,PA,G)) . z) 'or' ( 'not' (( All (b,PA,G)) . z))))) by XBOOLEAN: 8

      .= (((( 'not' (( All (a,PA,G)) . z)) '&' (( All (a,PA,G)) . z)) 'or' (( 'not' (( All (a,PA,G)) . z)) '&' ( 'not' (( All (b,PA,G)) . z)))) 'or' (((( All (b,PA,G)) . z) '&' (( All (a,PA,G)) . z)) 'or' ((( All (b,PA,G)) . z) '&' ( 'not' (( All (b,PA,G)) . z))))) by XBOOLEAN: 8

      .= (( FALSE 'or' (( 'not' (( All (a,PA,G)) . z)) '&' ( 'not' (( All (b,PA,G)) . z)))) 'or' (((( All (b,PA,G)) . z) '&' (( All (a,PA,G)) . z)) 'or' ((( All (b,PA,G)) . z) '&' ( 'not' (( All (b,PA,G)) . z))))) by XBOOLEAN: 138

      .= ((( 'not' (( All (a,PA,G)) . z)) '&' ( 'not' (( All (b,PA,G)) . z))) 'or' (((( All (b,PA,G)) . z) '&' (( All (a,PA,G)) . z)) 'or' FALSE )) by XBOOLEAN: 138

      .= ((( 'not' (( All (a,PA,G)) . z)) '&' ( 'not' (( All (b,PA,G)) . z))) 'or' ((( All (b,PA,G)) . z) '&' (( All (a,PA,G)) . z)));

      per cases ;

        suppose

         A3: (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE ) & for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE ;

        then (( B_INF (b,( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

        hence thesis by A2, A3, BVFUNC_1:def 16;

      end;

        suppose

         A4: (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE ) & not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

        then

        consider x1 be Element of Y such that

         A5: x1 in ( EqClass (z,( CompF (PA,G)))) and

         A6: (b . x1) <> TRUE ;

        

         A7: (a . x1) = TRUE by A4, A5;

        ((a 'eqv' b) . x1) = ( 'not' ((a . x1) 'xor' (b . x1))) by BVFUNC_1:def 9

        .= FALSE by A6, A7, XBOOLEAN:def 3;

        hence thesis by A1, A5, BVFUNC_1:def 16;

      end;

        suppose

         A8: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE ) & for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE ;

        then

        consider x1 be Element of Y such that

         A9: x1 in ( EqClass (z,( CompF (PA,G)))) and

         A10: (a . x1) <> TRUE ;

        

         A11: (b . x1) = TRUE by A8, A9;

        ((a 'eqv' b) . x1) = ( 'not' ((a . x1) 'xor' (b . x1))) by BVFUNC_1:def 9

        .= FALSE by A10, A11, XBOOLEAN:def 3;

        hence thesis by A1, A9, BVFUNC_1:def 16;

      end;

        suppose

         A12: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE ) & not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

        then (( B_INF (b,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        hence thesis by A2, A12, BVFUNC_1:def 16;

      end;

    end;

    theorem :: BVFUNC_4:24

    for a,b be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y holds ( All ((a '&' b),PA,G)) '<' (a '&' ( All (b,PA,G)))

    proof

      let a,b be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      let z be Element of Y;

      assume

       A1: (( All ((a '&' b),PA,G)) . z) = TRUE ;

       A2:

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE );

        then

        consider x1 be Element of Y such that

         A3: x1 in ( EqClass (z,( CompF (PA,G)))) and

         A4: (a . x1) <> TRUE ;

        ((a '&' b) . x1) = TRUE by A1, A3, BVFUNC_1:def 16;

        then

         A5: ((a . x1) '&' (b . x1)) = TRUE by MARGREL1:def 20;

        (a . x1) = FALSE by A4, XBOOLEAN:def 3;

        hence contradiction by A5;

      end;

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

        then

        consider x1 be Element of Y such that

         A6: x1 in ( EqClass (z,( CompF (PA,G)))) and

         A7: (b . x1) <> TRUE ;

        ((a '&' b) . x1) = TRUE by A1, A6, BVFUNC_1:def 16;

        then

         A8: ((a . x1) '&' (b . x1)) = TRUE by MARGREL1:def 20;

        (b . x1) = FALSE by A7, XBOOLEAN:def 3;

        hence contradiction by A8;

      end;

      then

       A9: (( B_INF (b,( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

      z in ( EqClass (z,( CompF (PA,G)))) by EQREL_1:def 6;

      then (a . z) = TRUE by A2;

      

      then ((a '&' ( All (b,PA,G))) . z) = ( TRUE '&' TRUE ) by A9, MARGREL1:def 20

      .= TRUE ;

      hence thesis;

    end;

    theorem :: BVFUNC_4:25

    for a,u be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y holds (( All (a,PA,G)) 'imp' u) '<' ( Ex ((a 'imp' u),PA,G))

    proof

      let a,u be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      let z be Element of Y;

      

       A1: z in ( EqClass (z,( CompF (PA,G)))) by EQREL_1:def 6;

      assume ((( All (a,PA,G)) 'imp' u) . z) = TRUE ;

      then

       A2: (( 'not' (( All (a,PA,G)) . z)) 'or' (u . z)) = TRUE by BVFUNC_1:def 8;

      

       A3: ( 'not' (( All (a,PA,G)) . z)) = TRUE or ( 'not' (( All (a,PA,G)) . z)) = FALSE by XBOOLEAN:def 3;

      now

        per cases by A2, A3;

          case ( 'not' (( All (a,PA,G)) . z)) = TRUE ;

          then

          consider x1 be Element of Y such that

           A4: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A5: (a . x1) <> TRUE by BVFUNC_1:def 16;

          now

            assume not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & ((a 'imp' u) . x) = TRUE );

            then ((a 'imp' u) . x1) <> TRUE by A4;

            then ((a 'imp' u) . x1) = FALSE by XBOOLEAN:def 3;

            then

             A6: (( 'not' (a . x1)) 'or' (u . x1)) = FALSE by BVFUNC_1:def 8;

            ( 'not' (a . x1)) = TRUE or ( 'not' (a . x1)) = FALSE by XBOOLEAN:def 3;

            hence contradiction by A5, A6;

          end;

          hence thesis by BVFUNC_1:def 17;

        end;

          case

           A7: (u . z) = TRUE ;

          now

            assume not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & ((a 'imp' u) . x) = TRUE );

            then ((a 'imp' u) . z) <> TRUE by A1;

            then ((a 'imp' u) . z) = FALSE by XBOOLEAN:def 3;

            then (( 'not' (a . z)) 'or' (u . z)) = FALSE by BVFUNC_1:def 8;

            hence contradiction by A7;

          end;

          hence thesis by BVFUNC_1:def 17;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_4:26

    for a,b be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y holds (a 'eqv' b) = ( I_el Y) implies (( All (a,PA,G)) 'eqv' ( All (b,PA,G))) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      assume

       A1: (a 'eqv' b) = ( I_el Y);

      then (b 'imp' a) = ( I_el Y) by Th10;

      then

       A2: (( 'not' b) 'or' a) = ( I_el Y) by Th8;

      (a 'imp' b) = ( I_el Y) by A1, Th10;

      then

       A3: (( 'not' a) 'or' b) = ( I_el Y) by Th8;

      for z be Element of Y holds ((( All (a,PA,G)) 'eqv' ( All (b,PA,G))) . z) = TRUE

      proof

        let z be Element of Y;

         A4:

        now

          assume that

           A5: for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE and

           A6: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

          consider x1 be Element of Y such that

           A7: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A8: (b . x1) <> TRUE by A6;

          

           A9: (a . x1) = TRUE by A5, A7;

          

           A10: (b . x1) = FALSE by A8, XBOOLEAN:def 3;

          ((( 'not' a) 'or' b) . x1) = ((( 'not' a) . x1) 'or' (b . x1)) by BVFUNC_1:def 4

          .= ( FALSE 'or' FALSE ) by A10, A9, MARGREL1:def 19

          .= FALSE ;

          hence thesis by A3, BVFUNC_1:def 11;

        end;

         A11:

        now

          assume that

           A12: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE ) and

           A13: for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE ;

          consider x1 be Element of Y such that

           A14: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A15: (a . x1) <> TRUE by A12;

          

           A16: (b . x1) = TRUE by A13, A14;

          

           A17: (a . x1) = FALSE by A15, XBOOLEAN:def 3;

          ((( 'not' b) 'or' a) . x1) = ((( 'not' b) . x1) 'or' (a . x1)) by BVFUNC_1:def 4

          .= ( FALSE 'or' FALSE ) by A17, A16, MARGREL1:def 19

          .= FALSE ;

          hence thesis by A2, BVFUNC_1:def 11;

        end;

        (( All (a,PA,G)) 'eqv' ( All (b,PA,G))) = ((( All (a,PA,G)) 'imp' ( All (b,PA,G))) '&' (( All (b,PA,G)) 'imp' ( All (a,PA,G)))) by Th7

        .= ((( 'not' ( All (a,PA,G))) 'or' ( All (b,PA,G))) '&' (( All (b,PA,G)) 'imp' ( All (a,PA,G)))) by Th8

        .= ((( 'not' ( All (a,PA,G))) 'or' ( All (b,PA,G))) '&' (( 'not' ( All (b,PA,G))) 'or' ( All (a,PA,G)))) by Th8

        .= (((( 'not' ( All (a,PA,G))) 'or' ( All (b,PA,G))) '&' ( 'not' ( All (b,PA,G)))) 'or' ((( 'not' ( All (a,PA,G))) 'or' ( All (b,PA,G))) '&' ( All (a,PA,G)))) by BVFUNC_1: 12

        .= (((( 'not' ( All (a,PA,G))) '&' ( 'not' ( All (b,PA,G)))) 'or' (( All (b,PA,G)) '&' ( 'not' ( All (b,PA,G))))) 'or' ((( 'not' ( All (a,PA,G))) 'or' ( All (b,PA,G))) '&' ( All (a,PA,G)))) by BVFUNC_1: 12

        .= (((( 'not' ( All (a,PA,G))) '&' ( 'not' ( All (b,PA,G)))) 'or' (( All (b,PA,G)) '&' ( 'not' ( All (b,PA,G))))) 'or' ((( 'not' ( All (a,PA,G))) '&' ( All (a,PA,G))) 'or' (( All (b,PA,G)) '&' ( All (a,PA,G))))) by BVFUNC_1: 12

        .= (((( 'not' ( All (a,PA,G))) '&' ( 'not' ( All (b,PA,G)))) 'or' ( O_el Y)) 'or' ((( 'not' ( All (a,PA,G))) '&' ( All (a,PA,G))) 'or' (( All (b,PA,G)) '&' ( All (a,PA,G))))) by Th5

        .= (((( 'not' ( All (a,PA,G))) '&' ( 'not' ( All (b,PA,G)))) 'or' ( O_el Y)) 'or' (( O_el Y) 'or' (( All (b,PA,G)) '&' ( All (a,PA,G))))) by Th5

        .= ((( 'not' ( All (a,PA,G))) '&' ( 'not' ( All (b,PA,G)))) 'or' (( O_el Y) 'or' (( All (b,PA,G)) '&' ( All (a,PA,G))))) by BVFUNC_1: 9

        .= ((( 'not' ( All (a,PA,G))) '&' ( 'not' ( All (b,PA,G)))) 'or' (( All (b,PA,G)) '&' ( All (a,PA,G)))) by BVFUNC_1: 9;

        

        then

         A18: ((( All (a,PA,G)) 'eqv' ( All (b,PA,G))) . z) = (((( 'not' ( All (a,PA,G))) '&' ( 'not' ( All (b,PA,G)))) . z) 'or' ((( All (b,PA,G)) '&' ( All (a,PA,G))) . z)) by BVFUNC_1:def 4

        .= (((( 'not' ( All (a,PA,G))) . z) '&' (( 'not' ( All (b,PA,G))) . z)) 'or' ((( All (b,PA,G)) '&' ( All (a,PA,G))) . z)) by MARGREL1:def 20

        .= (((( 'not' ( All (a,PA,G))) . z) '&' (( 'not' ( All (b,PA,G))) . z)) 'or' ((( All (b,PA,G)) . z) '&' (( All (a,PA,G)) . z))) by MARGREL1:def 20

        .= ((( 'not' (( All (a,PA,G)) . z)) '&' (( 'not' ( All (b,PA,G))) . z)) 'or' ((( All (b,PA,G)) . z) '&' (( All (a,PA,G)) . z))) by MARGREL1:def 19

        .= ((( 'not' (( All (a,PA,G)) . z)) '&' ( 'not' (( All (b,PA,G)) . z))) 'or' ((( All (b,PA,G)) . z) '&' (( All (a,PA,G)) . z))) by MARGREL1:def 19;

         A19:

        now

          assume that

           A20: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE ) and

           A21: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

          (( B_INF (b,( CompF (PA,G)))) . z) = FALSE by A21, BVFUNC_1:def 16;

          hence thesis by A18, A20, BVFUNC_1:def 16;

        end;

        now

          assume that

           A22: for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE and

           A23: for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE ;

          (( B_INF (b,( CompF (PA,G)))) . z) = TRUE by A23, BVFUNC_1:def 16;

          hence thesis by A18, A22, BVFUNC_1:def 16;

        end;

        hence thesis by A4, A11, A19;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_4:27

    for a,b be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y holds (a 'eqv' b) = ( I_el Y) implies (( Ex (a,PA,G)) 'eqv' ( Ex (b,PA,G))) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      assume

       A1: (a 'eqv' b) = ( I_el Y);

      then (b 'imp' a) = ( I_el Y) by Th10;

      then

       A2: (( 'not' b) 'or' a) = ( I_el Y) by Th8;

      (a 'imp' b) = ( I_el Y) by A1, Th10;

      then

       A3: (( 'not' a) 'or' b) = ( I_el Y) by Th8;

      for z be Element of Y holds ((( Ex (a,PA,G)) 'eqv' ( Ex (b,PA,G))) . z) = TRUE

      proof

        let z be Element of Y;

        (( Ex (a,PA,G)) 'eqv' ( Ex (b,PA,G))) = ((( Ex (a,PA,G)) 'imp' ( Ex (b,PA,G))) '&' (( Ex (b,PA,G)) 'imp' ( Ex (a,PA,G)))) by Th7

        .= ((( 'not' ( Ex (a,PA,G))) 'or' ( Ex (b,PA,G))) '&' (( Ex (b,PA,G)) 'imp' ( Ex (a,PA,G)))) by Th8

        .= ((( 'not' ( Ex (a,PA,G))) 'or' ( Ex (b,PA,G))) '&' (( 'not' ( Ex (b,PA,G))) 'or' ( Ex (a,PA,G)))) by Th8

        .= (((( 'not' ( Ex (a,PA,G))) 'or' ( Ex (b,PA,G))) '&' ( 'not' ( Ex (b,PA,G)))) 'or' ((( 'not' ( Ex (a,PA,G))) 'or' ( Ex (b,PA,G))) '&' ( Ex (a,PA,G)))) by BVFUNC_1: 12

        .= (((( 'not' ( Ex (a,PA,G))) '&' ( 'not' ( Ex (b,PA,G)))) 'or' (( Ex (b,PA,G)) '&' ( 'not' ( Ex (b,PA,G))))) 'or' ((( 'not' ( Ex (a,PA,G))) 'or' ( Ex (b,PA,G))) '&' ( Ex (a,PA,G)))) by BVFUNC_1: 12

        .= (((( 'not' ( Ex (a,PA,G))) '&' ( 'not' ( Ex (b,PA,G)))) 'or' (( Ex (b,PA,G)) '&' ( 'not' ( Ex (b,PA,G))))) 'or' ((( 'not' ( Ex (a,PA,G))) '&' ( Ex (a,PA,G))) 'or' (( Ex (b,PA,G)) '&' ( Ex (a,PA,G))))) by BVFUNC_1: 12

        .= (((( 'not' ( Ex (a,PA,G))) '&' ( 'not' ( Ex (b,PA,G)))) 'or' ( O_el Y)) 'or' ((( 'not' ( Ex (a,PA,G))) '&' ( Ex (a,PA,G))) 'or' (( Ex (b,PA,G)) '&' ( Ex (a,PA,G))))) by Th5

        .= (((( 'not' ( Ex (a,PA,G))) '&' ( 'not' ( Ex (b,PA,G)))) 'or' ( O_el Y)) 'or' (( O_el Y) 'or' (( Ex (b,PA,G)) '&' ( Ex (a,PA,G))))) by Th5

        .= ((( 'not' ( Ex (a,PA,G))) '&' ( 'not' ( Ex (b,PA,G)))) 'or' (( O_el Y) 'or' (( Ex (b,PA,G)) '&' ( Ex (a,PA,G))))) by BVFUNC_1: 9

        .= ((( 'not' ( Ex (a,PA,G))) '&' ( 'not' ( Ex (b,PA,G)))) 'or' (( Ex (b,PA,G)) '&' ( Ex (a,PA,G)))) by BVFUNC_1: 9;

        

        then

         A4: ((( Ex (a,PA,G)) 'eqv' ( Ex (b,PA,G))) . z) = (((( 'not' ( Ex (a,PA,G))) '&' ( 'not' ( Ex (b,PA,G)))) . z) 'or' ((( Ex (b,PA,G)) '&' ( Ex (a,PA,G))) . z)) by BVFUNC_1:def 4

        .= (((( 'not' ( Ex (a,PA,G))) . z) '&' (( 'not' ( Ex (b,PA,G))) . z)) 'or' ((( Ex (b,PA,G)) '&' ( Ex (a,PA,G))) . z)) by MARGREL1:def 20

        .= (((( 'not' ( Ex (a,PA,G))) . z) '&' (( 'not' ( Ex (b,PA,G))) . z)) 'or' ((( Ex (b,PA,G)) . z) '&' (( Ex (a,PA,G)) . z))) by MARGREL1:def 20

        .= ((( 'not' (( Ex (a,PA,G)) . z)) '&' (( 'not' ( Ex (b,PA,G))) . z)) 'or' ((( Ex (b,PA,G)) . z) '&' (( Ex (a,PA,G)) . z))) by MARGREL1:def 19

        .= ((( 'not' (( Ex (a,PA,G)) . z)) '&' ( 'not' (( Ex (b,PA,G)) . z))) 'or' ((( Ex (b,PA,G)) . z) '&' (( Ex (a,PA,G)) . z))) by MARGREL1:def 19;

        per cases ;

          suppose

           A5: (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (a . x) = TRUE ) & ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE ;

          then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 17;

          hence thesis by A4, A5, BVFUNC_1:def 17;

        end;

          suppose

           A6: (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (a . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE );

          then

          consider x1 be Element of Y such that

           A7: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A8: (a . x1) = TRUE ;

          (b . x1) <> TRUE by A6, A7;

          then

           A9: (b . x1) = FALSE by XBOOLEAN:def 3;

          ((( 'not' a) 'or' b) . x1) = ((( 'not' a) . x1) 'or' (b . x1)) by BVFUNC_1:def 4

          .= ( FALSE 'or' FALSE ) by A8, A9, MARGREL1:def 19

          .= FALSE ;

          hence thesis by A3, BVFUNC_1:def 11;

        end;

          suppose

           A10: not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (a . x) = TRUE ) & ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE ;

          then

          consider x1 be Element of Y such that

           A11: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A12: (b . x1) = TRUE ;

          (a . x1) <> TRUE by A10, A11;

          then

           A13: (a . x1) = FALSE by XBOOLEAN:def 3;

          ((( 'not' b) 'or' a) . x1) = ((( 'not' b) . x1) 'or' (a . x1)) by BVFUNC_1:def 4

          .= ( FALSE 'or' FALSE ) by A12, A13, MARGREL1:def 19

          .= FALSE ;

          hence thesis by A2, BVFUNC_1:def 11;

        end;

          suppose

           A14: not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (a . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE );

          then (( B_SUP (b,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

          hence thesis by A4, A14, BVFUNC_1:def 17;

        end;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;