bvfunc_2.miz



    begin

    reserve Y for non empty set,

G for Subset of ( PARTITIONS Y);

    definition

      let X be set;

      :: original: PARTITIONS

      redefine

      func PARTITIONS X -> Part-Family of X ;

      coherence

      proof

        

         A1: ( PARTITIONS X) c= ( bool ( bool X))

        proof

          let x be object;

          assume x in ( PARTITIONS X);

          then x is a_partition of X by PARTIT1:def 3;

          hence thesis;

        end;

        for S be set st S in ( PARTITIONS X) holds S is a_partition of X by PARTIT1:def 3;

        hence thesis by A1, EQREL_1:def 7;

      end;

    end

    definition

      let X be set;

      let F be non empty Part-Family of X;

      :: original: Element

      redefine

      mode Element of F -> a_partition of X ;

      coherence by EQREL_1:def 7;

    end

    theorem :: BVFUNC_2:1

    

     Th1: for y be Element of Y holds ex X be Subset of Y st y in X & ex h be Function, F be Subset-Family of Y st ( dom h) = G & ( rng h) = F & (for d be set st d in G holds (h . d) in d) & X = ( Intersect F) & X <> {}

    proof

      let y be Element of Y;

      deffunc F( Element of ( PARTITIONS Y)) = ( EqClass (y,$1));

      defpred P[ set] means $1 in G;

      consider h be PartFunc of ( PARTITIONS Y), ( bool Y) such that

       A1: for d be Element of ( PARTITIONS Y) holds d in ( dom h) iff P[d] and

       A2: for d be Element of ( PARTITIONS Y) st d in ( dom h) holds (h /. d) = F(d) from PARTFUN2:sch 2;

      

       A3: G c= ( dom h) by A1;

      

       A4: for d be set st d in G holds (h . d) in d

      proof

        let d be set;

        assume

         A5: d in G;

        then

        reconsider d as a_partition of Y by PARTIT1:def 3;

        (h /. d) = (h . d) by A3, A5, PARTFUN1:def 6;

        then (h . d) = ( EqClass (y,d)) by A2, A3, A5;

        hence thesis;

      end;

      ( dom h) c= G by A1;

      then

       A6: ( dom h) = G by A3, XBOOLE_0:def 10;

      reconsider rr = ( rng h) as Subset-Family of Y;

      

       A7: for d be Element of ( PARTITIONS Y) st d in ( dom h) holds y in (h . d)

      proof

        let d be Element of ( PARTITIONS Y);

        assume

         A8: d in ( dom h);

        then (h /. d) = ( EqClass (y,d)) by A2;

        then (h . d) = ( EqClass (y,d)) by A8, PARTFUN1:def 6;

        hence thesis by EQREL_1:def 6;

      end;

      

       A9: for c be set holds c in ( rng h) implies y in c

      proof

        let c be set;

        assume c in ( rng h);

        then ex a be object st a in ( dom h) & c = (h . a) by FUNCT_1:def 3;

        hence thesis by A7;

      end;

      per cases ;

        suppose ( rng h) = {} ;

        then ( Intersect rr) = Y by SETFAM_1:def 9;

        hence thesis by A6, A4;

      end;

        suppose ( rng h) <> {} ;

        then y in ( meet ( rng h)) & ( Intersect rr) = ( meet ( rng h)) by A9, SETFAM_1:def 1, SETFAM_1:def 9;

        hence thesis by A6, A4;

      end;

    end;

    definition

      let Y;

      let G be Subset of ( PARTITIONS Y);

      :: BVFUNC_2:def1

      func '/\' G -> a_partition of Y means

      : Def1: for x be set holds x in it iff ex h be Function, F be Subset-Family of Y st ( dom h) = G & ( rng h) = F & (for d be set st d in G holds (h . d) in d) & x = ( Intersect F) & x <> {} ;

      existence

      proof

        defpred P[ set] means (ex h be Function, F be Subset-Family of Y st ( dom h) = G & ( rng h) = F & (for d be set st d in G holds (h . d) in d) & $1 = ( Intersect F) & $1 <> {} );

        consider X be set such that

         A1: for x be set holds x in X iff x in ( bool Y) & P[x] from XFAMILY:sch 1;

        

         A2: for A be Subset of Y st A in X holds A <> {} & for B be Subset of Y st B in X holds A = B or A misses B

        proof

          let A be Subset of Y;

          assume A in X;

          then

          consider h1 be Function, F1 be Subset-Family of Y such that

           A3: ( dom h1) = G and

           A4: ( rng h1) = F1 and

           A5: for d be set st d in G holds (h1 . d) in d and

           A6: A = ( Intersect F1) and

           A7: A <> {} by A1;

          thus A <> {} by A7;

          let B be Subset of Y;

          assume B in X;

          then

          consider h2 be Function, F2 be Subset-Family of Y such that

           A8: ( dom h2) = G and

           A9: ( rng h2) = F2 and

           A10: for d be set st d in G holds (h2 . d) in d and

           A11: B = ( Intersect F2) and B <> {} by A1;

          per cases ;

            suppose

             A12: G = {} ;

            then ( rng h1) = {} by A3, RELAT_1: 42;

            hence thesis by A4, A6, A8, A9, A11, A12, RELAT_1: 42;

          end;

            suppose

             A13: G <> {} ;

            now

              assume A meets B;

              then

              consider p be object such that

               A14: p in A and

               A15: p in B by XBOOLE_0: 3;

              

               A16: p in ( meet ( rng h2)) by A9, A11, A13, A15, A8, RELAT_1: 42, SETFAM_1:def 9;

              

               A17: p in ( meet ( rng h1)) by A4, A6, A3, A13, A14, RELAT_1: 42, SETFAM_1:def 9;

              for g be object st g in G holds (h1 . g) = (h2 . g)

              proof

                let g be object;

                assume

                 A18: g in G;

                then

                reconsider g as a_partition of Y by PARTIT1:def 3;

                (h1 . g) in ( rng h1) by A3, A18, FUNCT_1:def 3;

                then

                 A19: p in (h1 . g) by A17, SETFAM_1:def 1;

                (h2 . g) in ( rng h2) by A8, A18, FUNCT_1:def 3;

                then

                 A20: p in (h2 . g) by A16, SETFAM_1:def 1;

                (h1 . g) in g & (h2 . g) in g by A5, A10, A18;

                hence thesis by A19, A20, EQREL_1:def 4, XBOOLE_0: 3;

              end;

              hence thesis by A3, A4, A6, A8, A9, A11, FUNCT_1: 2;

            end;

            hence thesis;

          end;

        end;

        

         A21: Y c= ( union X)

        proof

          let y be object;

          assume y in Y;

          then

          reconsider y as Element of Y;

          consider a be Subset of Y such that

           A22: y in a and

           A23: ex h be Function, F be Subset-Family of Y st ( dom h) = G & ( rng h) = F & (for d be set st d in G holds (h . d) in d) & a = ( Intersect F) & a <> {} by Th1;

          a in X by A1, A23;

          hence thesis by A22, TARSKI:def 4;

        end;

        

         A24: ( union X) c= Y

        proof

          let a be object;

          assume a in ( union X);

          then

          consider p be set such that

           A25: a in p and

           A26: p in X by TARSKI:def 4;

          ex h be Function, F be Subset-Family of Y st ( dom h) = G & ( rng h) = F & (for d be set st d in G holds (h . d) in d) & p = ( Intersect F) & p <> {} by A1, A26;

          hence thesis by A25;

        end;

        take X;

        X c= ( bool Y) by A1;

        then

        reconsider X as Subset-Family of Y;

        X is a_partition of Y by A24, A2, A21, EQREL_1:def 4, XBOOLE_0:def 10;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let A1,A2 be a_partition of Y such that

         A27: for x be set holds x in A1 iff ex h be Function, F be Subset-Family of Y st ( dom h) = G & ( rng h) = F & (for d be set st d in G holds (h . d) in d) & x = ( Intersect F) & x <> {} and

         A28: for x be set holds x in A2 iff ex h be Function, F be Subset-Family of Y st ( dom h) = G & ( rng h) = F & (for d be set st d in G holds (h . d) in d) & x = ( Intersect F) & x <> {} ;

        now

          let y be object;

          y in A1 iff ex h be Function, F be Subset-Family of Y st ( dom h) = G & ( rng h) = F & (for d be set st d in G holds (h . d) in d) & y = ( Intersect F) & y <> {} by A27;

          hence y in A1 iff y in A2 by A28;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let Y;

      let G be Subset of ( PARTITIONS Y), b be set;

      :: BVFUNC_2:def2

      pred b is_upper_min_depend_of G means (for d be a_partition of Y st d in G holds b is_a_dependent_set_of d) & for e be set st e c= b & (for d be a_partition of Y st d in G holds e is_a_dependent_set_of d) holds e = b;

    end

    theorem :: BVFUNC_2:2

    

     Th2: for y be Element of Y st G <> {} holds ex X be Subset of Y st y in X & X is_upper_min_depend_of G

    proof

      let y be Element of Y;

      defpred P[ set] means y in $1 & for d be a_partition of Y st d in G holds $1 is_a_dependent_set_of d;

      reconsider XX = { X where X be Subset of Y : P[X] } as Subset-Family of Y from DOMAIN_1:sch 7;

      reconsider XX as Subset-Family of Y;

      assume G <> {} ;

      then

      consider g be object such that

       A1: g in G by XBOOLE_0:def 1;

      reconsider g as a_partition of Y by A1, PARTIT1:def 3;

      

       A2: ( union g) = Y by EQREL_1:def 4;

      take ( Intersect XX);

      Y c= Y & for d be a_partition of Y st d in G holds Y is_a_dependent_set_of d by PARTIT1: 7;

      then

       A3: Y in XX;

      

       A4: for A be set st A in g holds A <> {} & for B be set st B in g holds A = B or A misses B by EQREL_1:def 4;

      

       A5: for e be set st e c= ( Intersect XX) & (for d be a_partition of Y st d in G holds e is_a_dependent_set_of d) holds e = ( Intersect XX)

      proof

        let e be set;

        assume that

         A6: e c= ( Intersect XX) and

         A7: for d be a_partition of Y st d in G holds e is_a_dependent_set_of d;

        consider Ad be set such that

         A8: Ad c= g and

         A9: Ad <> {} and

         A10: e = ( union Ad) by A1, A7, PARTIT1:def 1;

        

         A11: e c= Y by A2, A8, A10, ZFMISC_1: 77;

        per cases ;

          suppose y in e;

          then

           A12: e in XX by A7, A11;

          ( Intersect XX) c= e

          proof

            let X1 be object;

            assume X1 in ( Intersect XX);

            then X1 in ( meet XX) by A3, SETFAM_1:def 9;

            hence thesis by A12, SETFAM_1:def 1;

          end;

          hence thesis by A6, XBOOLE_0:def 10;

        end;

          suppose

           A13: not y in e;

          reconsider e as Subset of Y by A2, A8, A10, ZFMISC_1: 77;

          (e ` ) = (Y \ e) by SUBSET_1:def 4;

          then

           A14: y in (e ` ) by A13, XBOOLE_0:def 5;

          e <> Y by A13;

          then for d be a_partition of Y st d in G holds (e ` ) is_a_dependent_set_of d by A7, PARTIT1: 10;

          then

           A15: (e ` ) in XX by A14;

          

           A16: ( Intersect XX) c= (e ` )

          proof

            let X1 be object;

            assume X1 in ( Intersect XX);

            then X1 in ( meet XX) by A3, SETFAM_1:def 9;

            hence thesis by A15, SETFAM_1:def 1;

          end;

          

           A17: (e /\ e) = e;

          consider ad be object such that

           A18: ad in Ad by A9, XBOOLE_0:def 1;

          reconsider ad as set by TARSKI: 1;

          (e /\ (e ` )) = {} by SUBSET_1: 24, XBOOLE_0:def 7;

          then (e /\ ( Intersect XX)) = {} by A16, XBOOLE_1: 3, XBOOLE_1: 26;

          then e c= {} by A6, A17, XBOOLE_1: 26;

          then ( union Ad) = {} by A10;

          then

           A19: ad c= {} by A18, ZFMISC_1: 74;

          ad <> {} by A4, A8, A18;

          hence thesis by A19;

        end;

      end;

      for X1 be set st X1 in XX holds y in X1

      proof

        let X1 be set;

        assume X1 in XX;

        then ex X be Subset of Y st X = X1 & y in X & for d be a_partition of Y st d in G holds X is_a_dependent_set_of d;

        hence thesis;

      end;

      then

       A20: y in ( meet XX) by A3, SETFAM_1:def 1;

      then

       A21: ( Intersect XX) <> {} by SETFAM_1:def 9;

      for d be a_partition of Y st d in G holds ( Intersect XX) is_a_dependent_set_of d

      proof

        let d be a_partition of Y;

        assume

         A22: d in G;

        for X1 be set st X1 in XX holds X1 is_a_dependent_set_of d

        proof

          let X1 be set;

          assume X1 in XX;

          then ex X be Subset of Y st X = X1 & y in X & for d be a_partition of Y st d in G holds X is_a_dependent_set_of d;

          hence thesis by A22;

        end;

        hence thesis by A21, PARTIT1: 8;

      end;

      hence thesis by A3, A20, A5, SETFAM_1:def 9;

    end;

    definition

      let Y;

      let G be Subset of ( PARTITIONS Y);

      :: BVFUNC_2:def3

      func '\/' G -> a_partition of Y means

      : Def3: for x be set holds x in it iff x is_upper_min_depend_of G if G <> {}

      otherwise it = ( %I Y);

      existence

      proof

        thus G <> {} implies ex X be a_partition of Y st for x be set holds x in X iff x is_upper_min_depend_of G

        proof

          defpred P[ set] means $1 is_upper_min_depend_of G;

          consider X be set such that

           A1: for x be set holds x in X iff x in ( bool Y) & P[x] from XFAMILY:sch 1;

          

           A2: ( union X) c= Y

          proof

            let y be object;

            assume y in ( union X);

            then

            consider a be set such that

             A3: y in a and

             A4: a in X by TARSKI:def 4;

            a in ( bool Y) by A1, A4;

            hence thesis by A3;

          end;

          assume

           A5: G <> {} ;

          then

          consider g be object such that

           A6: g in G by XBOOLE_0:def 1;

          reconsider g as a_partition of Y by A6, PARTIT1:def 3;

          

           A7: ( union g) = Y by EQREL_1:def 4;

          

           A8: for x be set holds x in X iff x is_upper_min_depend_of G

          proof

            let x be set;

            for x be set holds x is_upper_min_depend_of G implies x in ( bool Y)

            proof

              let x be set;

              assume x is_upper_min_depend_of G;

              then ex A be set st A c= g & A <> {} & x = ( union A) by A6, PARTIT1:def 1;

              then x c= ( union g) by ZFMISC_1: 77;

              hence thesis by A7;

            end;

            hence thesis by A1;

          end;

          

           A9: Y c= ( union X)

          proof

            let y be object;

            assume y in Y;

            then

            reconsider y as Element of Y;

            consider a be Subset of Y such that

             A10: y in a and

             A11: a is_upper_min_depend_of G by A5, Th2;

            a in X by A8, A11;

            hence thesis by A10, TARSKI:def 4;

          end;

          

           A12: for A be set st A in g holds A <> {} & for B be set st B in g holds A = B or A misses B by EQREL_1:def 4;

          

           A13: for A be Subset of Y st A in X holds A <> {} & for B be Subset of Y st B in X holds A = B or A misses B

          proof

            let A be Subset of Y;

            assume A in X;

            then

             A14: A is_upper_min_depend_of G by A8;

            then

            consider Aa be set such that

             A15: Aa c= g and

             A16: Aa <> {} and

             A17: A = ( union Aa) by A6, PARTIT1:def 1;

            consider aa be object such that

             A18: aa in Aa by A16, XBOOLE_0:def 1;

            reconsider aa as set by TARSKI: 1;

            

             A19: aa c= ( union Aa) by A18, ZFMISC_1: 74;

            aa <> {} by A12, A15, A18;

            hence A <> {} by A17, A19;

            let B be Subset of Y;

            assume B in X;

            then

             A20: B is_upper_min_depend_of G by A8;

            now

              assume

               A21: A meets B;

              

               A22: for d be a_partition of Y st d in G holds (A /\ B) is_a_dependent_set_of d

              proof

                let d be a_partition of Y;

                assume d in G;

                then A is_a_dependent_set_of d & B is_a_dependent_set_of d by A14, A20;

                hence thesis by A21, PARTIT1: 9;

              end;

              

               A23: (A /\ B) = B by A20, A22, XBOOLE_1: 17;

              

               A24: B c= A by A23, XBOOLE_0:def 4;

              

               A25: (A /\ B) = A by A14, A22, XBOOLE_1: 17;

              A c= B by A25, XBOOLE_0:def 4;

              hence A = B by A24, XBOOLE_0:def 10;

            end;

            hence thesis;

          end;

          take X;

          X c= ( bool Y) by A1;

          then

          reconsider X as Subset-Family of Y;

          X is a_partition of Y by A9, A13, A2, EQREL_1:def 4, XBOOLE_0:def 10;

          hence thesis by A8;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let A1,A2 be a_partition of Y;

        now

          assume that G <> {} and

           A26: for x be set holds x in A1 iff x is_upper_min_depend_of G and

           A27: for x be set holds x in A2 iff x is_upper_min_depend_of G;

          for y be object holds y in A1 iff y in A2 by A27, A26;

          hence A1 = A2 by TARSKI: 2;

        end;

        hence thesis;

      end;

      consistency ;

    end

    theorem :: BVFUNC_2:3

    for G be Subset of ( PARTITIONS Y), PA be a_partition of Y st PA in G holds PA '>' ( '/\' G)

    proof

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      assume

       A1: PA in G;

      for x be set st x in ( '/\' G) holds ex a be set st a in PA & x c= a

      proof

        let x be set;

        assume x in ( '/\' G);

        then

        consider h be Function, F be Subset-Family of Y such that

         A2: ( dom h) = G and

         A3: ( rng h) = F and

         A4: for d be set st d in G holds (h . d) in d and

         A5: x = ( Intersect F) and x <> {} by Def1;

        set a = (h . PA);

        

         A6: a in PA by A1, A4;

        

         A7: a in ( rng h) by A1, A2, FUNCT_1:def 3;

        then ( Intersect F) = ( meet F) by A3, SETFAM_1:def 9;

        hence thesis by A3, A5, A6, A7, SETFAM_1: 3;

      end;

      hence thesis by SETFAM_1:def 2;

    end;

    theorem :: BVFUNC_2:4

    for G be Subset of ( PARTITIONS Y), PA be a_partition of Y st PA in G holds PA '<' ( '\/' G)

    proof

      let G be Subset of ( PARTITIONS Y);

      let PA be a_partition of Y;

      assume

       A1: PA in G;

      for a be set st a in PA holds ex b be set st b in ( '\/' G) & a c= b

      proof

        let a be set;

        set x = the Element of a;

        

         A2: ( union ( '\/' G)) = Y by EQREL_1:def 4;

        assume

         A3: a in PA;

        then

         A4: a <> {} by EQREL_1:def 4;

        then x in Y by A3, TARSKI:def 3;

        then

        consider b be set such that

         A5: x in b and

         A6: b in ( '\/' G) by A2, TARSKI:def 4;

        b is_upper_min_depend_of G by A1, A6, Def3;

        then

        consider B be set such that

         A7: B c= PA and B <> {} and

         A8: b = ( union B) by A1, PARTIT1:def 1;

        a in B

        proof

          consider u be set such that

           A9: x in u and

           A10: u in B by A5, A8, TARSKI:def 4;

          

           A11: (a /\ u) <> {} by A4, A9, XBOOLE_0:def 4;

          u in PA by A7, A10;

          hence thesis by A3, A10, A11, EQREL_1:def 4, XBOOLE_0:def 7;

        end;

        hence thesis by A6, A8, ZFMISC_1: 74;

      end;

      hence thesis by SETFAM_1:def 2;

    end;

    begin

    definition

      let Y;

      let G be Subset of ( PARTITIONS Y);

      :: BVFUNC_2:def4

      attr G is generating means ( '/\' G) = ( %I Y);

    end

    definition

      let Y;

      let G be Subset of ( PARTITIONS Y);

      :: BVFUNC_2:def5

      attr G is independent means for h be Function, F be Subset-Family of Y st ( dom h) = G & ( rng h) = F & (for d be set st d in G holds (h . d) in d) holds ( Intersect F) <> {} ;

    end

    definition

      let Y;

      let G be Subset of ( PARTITIONS Y);

      :: BVFUNC_2:def6

      pred G is_a_coordinate means G is independent generating;

    end

    definition

      let Y;

      let PA be a_partition of Y;

      :: original: {

      redefine

      func {PA} -> Subset of ( PARTITIONS Y) ;

      coherence

      proof

        PA in ( PARTITIONS Y) by PARTIT1:def 3;

        hence thesis by ZFMISC_1: 31;

      end;

    end

    definition

      let Y;

      let PA be a_partition of Y;

      let G be Subset of ( PARTITIONS Y);

      :: BVFUNC_2:def7

      func CompF (PA,G) -> a_partition of Y equals ( '/\' (G \ {PA}));

      correctness ;

    end

    definition

      let Y;

      let a be Function of Y, BOOLEAN ;

      let G be Subset of ( PARTITIONS Y), PA be a_partition of Y;

      :: BVFUNC_2:def8

      pred a is_independent_of PA,G means a is_dependent_of ( CompF (PA,G));

    end

    definition

      let Y;

      let a be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y;

      :: BVFUNC_2:def9

      func All (a,PA,G) -> Function of Y, BOOLEAN equals ( B_INF (a,( CompF (PA,G))));

      correctness ;

    end

    definition

      let Y;

      let a be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y;

      :: BVFUNC_2:def10

      func Ex (a,PA,G) -> Function of Y, BOOLEAN equals ( B_SUP (a,( CompF (PA,G))));

      correctness ;

    end

    theorem :: BVFUNC_2:5

    for a be Function of Y, BOOLEAN , PA be a_partition of Y holds ( All (a,PA,G)) is_dependent_of ( CompF (PA,G))

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      let F be set;

      assume

       A1: F in ( CompF (PA,G));

      thus for x1,x2 be set st x1 in F & x2 in F holds (( All (a,PA,G)) . x1) = (( All (a,PA,G)) . x2)

      proof

        let x1,x2 be set;

        assume

         A2: x1 in F & x2 in F;

        then

        reconsider x1, x2 as Element of Y by A1;

        

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

        F = ( EqClass (x2,( CompF (PA,G)))) or F misses ( EqClass (x2,( CompF (PA,G)))) by A1, EQREL_1:def 4;

        then

         A4: ( EqClass (x1,( CompF (PA,G)))) = ( EqClass (x2,( CompF (PA,G)))) by A2, A3, EQREL_1:def 6, XBOOLE_0: 3;

        per cases ;

          suppose

           A5: (for x be Element of Y st x in ( EqClass (x1,( CompF (PA,G)))) holds (a . x) = TRUE ) & for x be Element of Y st x in ( EqClass (x2,( CompF (PA,G)))) holds (a . x) = TRUE ;

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

          hence thesis by A5, BVFUNC_1:def 16;

        end;

          suppose (for x be Element of Y st x in ( EqClass (x1,( CompF (PA,G)))) holds (a . x) = TRUE ) & not (for x be Element of Y st x in ( EqClass (x2,( CompF (PA,G)))) holds (a . x) = TRUE );

          hence thesis by A4;

        end;

          suppose not (for x be Element of Y st x in ( EqClass (x1,( CompF (PA,G)))) holds (a . x) = TRUE ) & for x be Element of Y st x in ( EqClass (x2,( CompF (PA,G)))) holds (a . x) = TRUE ;

          hence thesis by A4;

        end;

          suppose

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

          then (( All (a,PA,G)) . x2) = FALSE by BVFUNC_1:def 16;

          hence thesis by A6, BVFUNC_1:def 16;

        end;

      end;

    end;

    theorem :: BVFUNC_2:6

    for a be Function of Y, BOOLEAN , PA be a_partition of Y holds ( Ex (a,PA,G)) is_dependent_of ( CompF (PA,G))

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      let F be set;

      assume

       A1: F in ( CompF (PA,G));

      thus for x1,x2 be set st x1 in F & x2 in F holds (( Ex (a,PA,G)) . x1) = (( Ex (a,PA,G)) . x2)

      proof

        let x1,x2 be set;

        assume

         A2: x1 in F & x2 in F;

        then

        reconsider x1, x2 as Element of Y by A1;

        

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

        F = ( EqClass (x2,( CompF (PA,G)))) or F misses ( EqClass (x2,( CompF (PA,G)))) by A1, EQREL_1:def 4;

        then

         A4: ( EqClass (x1,( CompF (PA,G)))) = ( EqClass (x2,( CompF (PA,G)))) by A2, A3, EQREL_1:def 6, XBOOLE_0: 3;

        per cases ;

          suppose

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

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

          hence thesis by A5, BVFUNC_1:def 17;

        end;

          suppose (ex x be Element of Y st x in ( EqClass (x1,( CompF (PA,G)))) & (a . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (x2,( CompF (PA,G)))) & (a . x) = TRUE );

          hence thesis by A4;

        end;

          suppose not (ex x be Element of Y st x in ( EqClass (x1,( CompF (PA,G)))) & (a . x) = TRUE ) & ex x be Element of Y st x in ( EqClass (x2,( CompF (PA,G)))) & (a . x) = TRUE ;

          hence thesis by A4;

        end;

          suppose

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

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

          hence thesis by A6, BVFUNC_1:def 17;

        end;

      end;

    end;

    theorem :: BVFUNC_2:7

    for a be Function of Y, BOOLEAN , PA be a_partition of Y holds ( All (( I_el Y),PA,G)) = ( I_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

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

      proof

        let z be Element of Y;

        for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (( I_el Y) . x) = TRUE by BVFUNC_1:def 11;

        hence thesis by BVFUNC_1:def 16;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_2:8

    for a be Function of Y, BOOLEAN , PA be a_partition of Y holds ( Ex (( I_el Y),PA,G)) = ( I_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

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

      proof

        let z be Element of Y;

        z in ( EqClass (z,( CompF (PA,G)))) & (( I_el Y) . z) = TRUE by BVFUNC_1:def 11, EQREL_1:def 6;

        hence thesis by BVFUNC_1:def 17;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_2:9

    for a be Function of Y, BOOLEAN , PA be a_partition of Y holds ( All (( O_el Y),PA,G)) = ( O_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      for z be Element of Y holds (( All (( O_el Y),PA,G)) . z) = FALSE

      proof

        let z be Element of Y;

        z in ( EqClass (z,( CompF (PA,G)))) & (( O_el Y) . z) = FALSE by BVFUNC_1:def 10, EQREL_1:def 6;

        hence thesis by BVFUNC_1:def 16;

      end;

      hence thesis by BVFUNC_1:def 10;

    end;

    theorem :: BVFUNC_2:10

    for a be Function of Y, BOOLEAN , PA be a_partition of Y holds ( Ex (( O_el Y),PA,G)) = ( O_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      for z be Element of Y holds (( Ex (( O_el Y),PA,G)) . z) = FALSE

      proof

        let z be Element of Y;

        for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (( O_el Y) . x) <> TRUE by BVFUNC_1:def 10;

        hence thesis by BVFUNC_1:def 17;

      end;

      hence thesis by BVFUNC_1:def 10;

    end;

    theorem :: BVFUNC_2:11

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

    proof

      let a be Function of Y, BOOLEAN ;

      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)) . z) = TRUE ;

      hence (a . z) = TRUE by A1, BVFUNC_1:def 16;

    end;

    theorem :: BVFUNC_2:12

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

    proof

      let a be Function of Y, BOOLEAN ;

      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 (a . z) = TRUE ;

      hence (( Ex (a,PA,G)) . z) = TRUE by A1, BVFUNC_1:def 17;

    end;

    theorem :: BVFUNC_2:13

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

    proof

      let a,b be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      let z be Element of Y;

      assume ((( All (a,PA,G)) 'or' ( All (b,PA,G))) . z) = TRUE ;

      then

       A1: ((( All (a,PA,G)) . z) 'or' (( All (b,PA,G)) . z)) = TRUE by BVFUNC_1:def 4;

      

       A2: (( All (b,PA,G)) . z) = TRUE or (( All (b,PA,G)) . z) = FALSE by XBOOLEAN:def 3;

      now

        per cases by A1, A2, BINARITH: 3;

          case

           A3: (( All (a,PA,G)) . z) = TRUE ;

          for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((a 'or' b) . x) = TRUE

          proof

            let x be Element of Y;

            assume

             A4: x in ( EqClass (z,( CompF (PA,G))));

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

            .= ( TRUE 'or' (b . x)) by A3, A4, BVFUNC_1:def 16

            .= TRUE by BINARITH: 10;

            hence thesis;

          end;

          hence thesis by BVFUNC_1:def 16;

        end;

          case

           A5: (( All (b,PA,G)) . z) = TRUE ;

          for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((a 'or' b) . x) = TRUE

          proof

            let x be Element of Y;

            assume

             A6: x in ( EqClass (z,( CompF (PA,G))));

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

            .= ((a . x) 'or' TRUE ) by A5, A6, BVFUNC_1:def 16

            .= TRUE by BINARITH: 10;

            hence thesis;

          end;

          hence thesis by BVFUNC_1:def 16;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_2:14

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

    proof

      let a,b be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      let z be Element of Y;

      assume

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

      

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

      per cases ;

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

        

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

        .= TRUE by BINARITH: 10;

        hence thesis;

      end;

        suppose

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

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

         A5: (b . x1) <> TRUE ;

        

         A6: (a . x1) = TRUE by A3, A4;

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

        .= (( 'not' TRUE ) 'or' FALSE ) by A5, A6, XBOOLEAN:def 3

        .= ( FALSE 'or' FALSE ) by MARGREL1: 11

        .= FALSE ;

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

      end;

        suppose 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 ((( All (a,PA,G)) 'imp' ( All (b,PA,G))) . z) = (( 'not' (( All (a,PA,G)) . z)) 'or' TRUE ) by A2, BVFUNC_1:def 16

        .= TRUE by BINARITH: 10;

        hence thesis;

      end;

        suppose 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 ((( All (a,PA,G)) 'imp' ( All (b,PA,G))) . z) = ( TRUE 'or' (( All (b,PA,G)) . z)) by A2, BVFUNC_1:def 16, MARGREL1: 11

        .= TRUE by BINARITH: 10;

        hence thesis;

      end;

    end;

    theorem :: BVFUNC_2:15

    for a,b be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), PA be a_partition of Y holds ( Ex ((a '&' b),PA,G)) '<' (( Ex (a,PA,G)) '&' ( Ex (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 (( Ex ((a '&' b),PA,G)) . z) = TRUE ;

      then

      consider x1 be Element of Y such that

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

       A2: ((a '&' b) . x1) = TRUE by BVFUNC_1:def 17;

      

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

      then

       A4: (b . x1) = TRUE by MARGREL1: 12;

      (a . x1) = TRUE by A3, MARGREL1: 12;

      then

       A5: (( Ex (a,PA,G)) . z) = TRUE by A1, BVFUNC_1:def 17;

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

      .= ( TRUE '&' TRUE ) by A1, A4, A5, BVFUNC_1:def 17

      .= TRUE ;

      hence thesis;

    end;

    theorem :: BVFUNC_2:16

    for a,b be Function of Y, BOOLEAN , PA be a_partition of Y holds (( Ex (a,PA,G)) 'xor' ( Ex (b,PA,G))) '<' ( Ex ((a 'xor' b),PA,G))

    proof

      let a,b be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      let z be Element of Y;

      

       A1: ((( Ex (a,PA,G)) 'xor' ( Ex (b,PA,G))) . z) = ((( Ex (a,PA,G)) . z) 'xor' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 5

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

      

       A2: (( 'not' (( Ex (a,PA,G)) . z)) '&' (( Ex (b,PA,G)) . z)) = TRUE or (( 'not' (( Ex (a,PA,G)) . z)) '&' (( Ex (b,PA,G)) . z)) = FALSE by XBOOLEAN:def 3;

      

       A3: ( 'not' FALSE ) = TRUE by MARGREL1: 11;

      assume

       A4: ((( Ex (a,PA,G)) 'xor' ( Ex (b,PA,G))) . z) = TRUE ;

      now

        per cases by A4, A1, A2, BINARITH: 3;

          case

           A5: (( 'not' (( Ex (a,PA,G)) . z)) '&' (( Ex (b,PA,G)) . z)) = TRUE ;

          then (( Ex (b,PA,G)) . z) = TRUE by MARGREL1: 12;

          then

          consider x1 be Element of Y such that

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

           A7: (b . x1) = TRUE by BVFUNC_1:def 17;

          ( 'not' (( Ex (a,PA,G)) . z)) = TRUE by A5, MARGREL1: 12;

          then (a . x1) <> TRUE by A6, BVFUNC_1:def 17, MARGREL1: 11;

          then

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

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

          .= ( TRUE 'or' FALSE ) by A3, A7, A8

          .= TRUE by BINARITH: 10;

          hence thesis by A6, BVFUNC_1:def 17;

        end;

          case

           A9: ((( Ex (a,PA,G)) . z) '&' ( 'not' (( Ex (b,PA,G)) . z))) = TRUE ;

          then (( Ex (a,PA,G)) . z) = TRUE by MARGREL1: 12;

          then

          consider x1 be Element of Y such that

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

           A11: (a . x1) = TRUE by BVFUNC_1:def 17;

          ( 'not' (( Ex (b,PA,G)) . z)) = TRUE by A9, MARGREL1: 12;

          then (b . x1) <> TRUE by A10, BVFUNC_1:def 17, MARGREL1: 11;

          then

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

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

          .= ( FALSE 'or' TRUE ) by A3, A11, A12

          .= TRUE by BINARITH: 10;

          hence thesis by A10, BVFUNC_1:def 17;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_2:17

    for a,b be Function of Y, BOOLEAN , PA be a_partition of Y holds (( Ex (a,PA,G)) 'imp' ( Ex (b,PA,G))) '<' ( Ex ((a 'imp' b),PA,G))

    proof

      let a,b be Function of Y, BOOLEAN ;

      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 ((( Ex (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = TRUE ;

      then

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

      

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

      now

        per cases by A2, A3, BINARITH: 3;

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

          then

           A4: (a . z) <> TRUE by A1, BVFUNC_1:def 17, MARGREL1: 11;

          ((a 'imp' b) . z) = (( 'not' (a . z)) 'or' (b . z)) by BVFUNC_1:def 8

          .= ( TRUE 'or' (b . z)) by A4, MARGREL1: 11, XBOOLEAN:def 3

          .= TRUE by BINARITH: 10;

          hence thesis by A1, BVFUNC_1:def 17;

        end;

          case (( Ex (b,PA,G)) . z) = TRUE ;

          then

          consider x1 be Element of Y such that

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

           A6: (b . x1) = TRUE by BVFUNC_1:def 17;

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

          .= TRUE by A6, BINARITH: 10;

          hence thesis by A5, BVFUNC_1:def 17;

        end;

      end;

      hence thesis;

    end;

    reserve a,u for Function of Y, BOOLEAN ;

    theorem :: BVFUNC_2:18

    for PA be a_partition of Y holds ( 'not' ( All (a,PA,G))) = ( Ex (( 'not' a),PA,G))

    proof

      let PA be a_partition of Y;

      let z be Element of Y;

      per cases ;

        suppose

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

        then

        consider x1 be Element of Y such that

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

         A3: (( 'not' a) . x1) = TRUE ;

        ( 'not' (a . x1)) = TRUE by A3, MARGREL1:def 19;

        hence thesis by A1, A2, MARGREL1: 11;

      end;

        suppose

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

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

        then

         A5: (( 'not' ( B_INF (a,( CompF (PA,G))))) . z) = ( 'not' TRUE ) by MARGREL1:def 19;

        (( B_SUP (( 'not' a),( CompF (PA,G)))) . z) = FALSE by A4, BVFUNC_1:def 17;

        hence thesis by A5, MARGREL1: 11;

      end;

        suppose

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

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

        then

         A7: (( 'not' ( B_INF (a,( CompF (PA,G))))) . z) = ( 'not' FALSE ) by MARGREL1:def 19;

        (( B_SUP (( 'not' a),( CompF (PA,G)))) . z) = TRUE by A6, BVFUNC_1:def 17;

        hence thesis by A7, MARGREL1: 11;

      end;

        suppose

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

        then

        consider x1 be Element of Y such that

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

         A10: (a . x1) <> TRUE ;

        (( 'not' a) . x1) <> TRUE by A8, A9;

        then ( 'not' (a . x1)) <> TRUE by MARGREL1:def 19;

        hence thesis by A10, MARGREL1: 11, XBOOLEAN:def 3;

      end;

    end;

    theorem :: BVFUNC_2:19

    for PA be a_partition of Y holds ( 'not' ( Ex (a,PA,G))) = ( All (( 'not' a),PA,G))

    proof

      let PA be a_partition of Y;

      let z be Element of Y;

      per cases ;

        suppose

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

        then

        consider x1 be Element of Y such that

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

         A3: (a . x1) = TRUE ;

        (( 'not' a) . x1) = ( 'not' TRUE ) by A3, MARGREL1:def 19;

        hence thesis by A1, A2, MARGREL1: 11;

      end;

        suppose

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

        then ( 'not' (( B_SUP (a,( CompF (PA,G)))) . z)) = TRUE by BVFUNC_1:def 17, MARGREL1: 11;

        then (( 'not' ( B_SUP (a,( CompF (PA,G))))) . z) = TRUE by MARGREL1:def 19;

        hence thesis by A4, BVFUNC_1:def 16;

      end;

        suppose

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

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

        then

         A6: (( 'not' ( B_SUP (a,( CompF (PA,G))))) . z) = ( 'not' TRUE ) by MARGREL1:def 19;

        (( B_INF (( 'not' a),( CompF (PA,G)))) . z) = FALSE by A5, BVFUNC_1:def 16;

        hence thesis by A6, MARGREL1: 11;

      end;

        suppose

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

        then

        consider x1 be Element of Y such that

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

         A9: (( 'not' a) . x1) <> TRUE ;

        (( 'not' a) . x1) = FALSE by A9, XBOOLEAN:def 3;

        then ( 'not' (a . x1)) = FALSE by MARGREL1:def 19;

        hence thesis by A7, A8, MARGREL1: 11;

      end;

    end;

    theorem :: BVFUNC_2:20

    for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((u 'imp' a),PA,G)) = (u 'imp' ( All (a,PA,G)))

    proof

      let PA be a_partition of Y;

      assume

       A1: u is_independent_of (PA,G);

      

       A2: (u 'imp' ( All (a,PA,G))) '<' ( All ((u 'imp' a),PA,G))

      proof

        let z be Element of Y;

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

        then

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

        

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

        now

          per cases by A3, A4, BINARITH: 3;

            suppose

             A5: (( All (a,PA,G)) . z) = TRUE ;

            for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((u 'imp' a) . x) = TRUE

            proof

              let x be Element of Y;

              assume

               A6: x in ( EqClass (z,( CompF (PA,G))));

              ((u 'imp' a) . x) = (( 'not' (u . x)) 'or' (a . x)) by BVFUNC_1:def 8

              .= (( 'not' (u . x)) 'or' TRUE ) by A5, A6, BVFUNC_1:def 16

              .= TRUE by BINARITH: 10;

              hence thesis;

            end;

            hence thesis by BVFUNC_1:def 16;

          end;

            suppose

             A7: (( All (a,PA,G)) . z) <> TRUE & ( 'not' (u . z)) = TRUE ;

            

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

            for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((u 'imp' a) . x) = TRUE

            proof

              let x be Element of Y;

              assume x in ( EqClass (z,( CompF (PA,G))));

              then ((u 'imp' a) . x) = (( 'not' (u . x)) 'or' (a . x)) & (u . x) = (u . z) by A1, A8, BVFUNC_1:def 8, BVFUNC_1:def 15;

              hence thesis by A7, BINARITH: 10;

            end;

            hence thesis by BVFUNC_1:def 16;

          end;

        end;

        hence thesis;

      end;

      ( All ((u 'imp' a),PA,G)) '<' (u 'imp' ( All (a,PA,G)))

      proof

        let z be Element of Y;

        assume

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

        

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

        per cases ;

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

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

          hence thesis by A10, BINARITH: 10;

        end;

          suppose 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 ( 'not' (u . x)) = TRUE ;

          then ( 'not' (u . z)) = TRUE by EQREL_1:def 6;

          hence thesis by A10, BINARITH: 10;

        end;

          suppose

           A11: 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 ( 'not' (u . x)) = TRUE );

          then

          consider x1 be Element of Y such that

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

           A13: ( 'not' (u . x1)) <> TRUE ;

          consider x2 be Element of Y such that

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

           A15: (a . x2) <> TRUE by A11;

          (u . x1) = (u . x2) by A1, A12, A14, BVFUNC_1:def 15;

          then

           A16: (u . x2) = TRUE by A13, MARGREL1: 11, XBOOLEAN:def 3;

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

          then ((u 'imp' a) . x2) = (( 'not' TRUE ) 'or' FALSE ) by A16, BVFUNC_1:def 8;

          

          then ((u 'imp' a) . x2) = ( FALSE 'or' FALSE ) by MARGREL1: 11

          .= FALSE ;

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

        end;

      end;

      hence thesis by A2, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC_2:21

    for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((a 'imp' u),PA,G)) = (( Ex (a,PA,G)) 'imp' u)

    proof

      let PA be a_partition of Y;

      assume

       A1: u is_independent_of (PA,G);

      

       A2: (( Ex (a,PA,G)) 'imp' u) '<' ( All ((a 'imp' u),PA,G))

      proof

        let z be Element of Y;

        

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

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

        then

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

        

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

        now

          per cases by A4, A5, BINARITH: 3, XBOOLEAN:def 3;

            case

             A6: (u . z) = TRUE ;

            for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((a 'imp' u) . x) = TRUE

            proof

              let x be Element of Y;

              assume x in ( EqClass (z,( CompF (PA,G))));

              then ((a 'imp' u) . x) = (( 'not' (a . x)) 'or' (u . x)) & (u . x) = (u . z) by A1, A3, BVFUNC_1:def 8, BVFUNC_1:def 15;

              hence thesis by A6, BINARITH: 10;

            end;

            hence thesis by BVFUNC_1:def 16;

          end;

            case

             A7: ( 'not' (( Ex (a,PA,G)) . z)) = TRUE & (u . z) = FALSE ;

            for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((a 'imp' u) . x) = TRUE

            proof

              let x be Element of Y;

              assume x in ( EqClass (z,( CompF (PA,G))));

              then (a . x) <> TRUE by A7, BVFUNC_1:def 17, MARGREL1: 11;

              then ((a 'imp' u) . x) = (( 'not' (a . x)) 'or' (u . x)) & (a . x) = FALSE by BVFUNC_1:def 8, XBOOLEAN:def 3;

              

              then ((a 'imp' u) . x) = ( TRUE 'or' (u . x)) by MARGREL1: 11

              .= TRUE by BINARITH: 10;

              hence thesis;

            end;

            hence thesis by BVFUNC_1:def 16;

          end;

        end;

        hence thesis;

      end;

      ( All ((a 'imp' u),PA,G)) '<' (( Ex (a,PA,G)) 'imp' u)

      proof

        let z be Element of Y;

        assume

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

        

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

        per cases ;

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

          

          then ((( Ex (a,PA,G)) 'imp' u) . z) = (( 'not' (( Ex (a,PA,G)) . z)) 'or' TRUE ) by A9, EQREL_1:def 6

          .= TRUE by BINARITH: 10;

          hence thesis;

        end;

          suppose

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

          then

          consider x1 be Element of Y such that

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

           A12: (u . x1) <> TRUE ;

          consider x2 be Element of Y such that

           A13: x2 in ( EqClass (z,( CompF (PA,G)))) and

           A14: (a . x2) = TRUE by A10;

          

           A15: (u . x1) = (u . x2) by A1, A11, A13, BVFUNC_1:def 15;

          ((a 'imp' u) . x2) = (( 'not' (a . x2)) 'or' (u . x2)) by BVFUNC_1:def 8

          .= (( 'not' TRUE ) 'or' FALSE ) by A12, A14, A15, XBOOLEAN:def 3

          .= ( FALSE 'or' FALSE ) by MARGREL1: 11

          .= FALSE ;

          hence thesis by A8, A13, BVFUNC_1:def 16;

        end;

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

          

          then ((( Ex (a,PA,G)) 'imp' u) . z) = (( 'not' FALSE ) 'or' (u . z)) by A9, BVFUNC_1:def 17

          .= ( TRUE 'or' (u . z)) by MARGREL1: 11

          .= TRUE by BINARITH: 10;

          hence thesis;

        end;

      end;

      hence thesis by A2, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC_2:22

    

     Th22: for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((u 'or' a),PA,G)) = (u 'or' ( All (a,PA,G)))

    proof

      let PA be a_partition of Y;

      assume

       A1: u is_independent_of (PA,G);

      let z be Element of Y;

      

       A2: ((u 'or' ( B_INF (a,( CompF (PA,G))))) . z) = ((u . z) 'or' (( B_INF (a,( CompF (PA,G)))) . z)) by BVFUNC_1:def 4;

      per cases ;

        suppose

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

        

         A4: for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((u 'or' a) . x) = TRUE

        proof

          let x be Element of Y;

          assume

           A5: x in ( EqClass (z,( CompF (PA,G))));

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

          .= ((u . x) 'or' TRUE ) by A3, A5

          .= TRUE by BINARITH: 10;

          hence thesis;

        end;

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

        then ((u 'or' ( B_INF (a,( CompF (PA,G))))) . z) = TRUE by A2, BINARITH: 10;

        hence thesis by A4, BVFUNC_1:def 16;

      end;

        suppose

         A6: 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 (u . x) = TRUE ;

        

         A7: for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((u 'or' a) . x) = TRUE

        proof

          let x be Element of Y;

          assume

           A8: x in ( EqClass (z,( CompF (PA,G))));

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

          .= ( TRUE 'or' (a . x)) by A6, A8

          .= TRUE by BINARITH: 10;

          hence thesis;

        end;

        ((u 'or' ( B_INF (a,( CompF (PA,G))))) . z) = ( TRUE 'or' (( B_INF (a,( CompF (PA,G)))) . z)) by A2, A6, EQREL_1:def 6;

        then ((u 'or' ( B_INF (a,( CompF (PA,G))))) . z) = TRUE by BINARITH: 10;

        hence thesis by A7, BVFUNC_1:def 16;

      end;

        suppose

         A9: 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 (u . x) = TRUE );

        then

        consider x2 be Element of Y such that

         A10: x2 in ( EqClass (z,( CompF (PA,G)))) and

         A11: (u . x2) <> TRUE ;

        consider x1 be Element of Y such that

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

         A13: (a . x1) <> TRUE by A9;

        (u . x1) = (u . x2) by A1, A12, A10, BVFUNC_1:def 15;

        then

         A14: (u . x1) = FALSE by A11, XBOOLEAN:def 3;

        

         A15: (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by A9, BVFUNC_1:def 16;

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

        then

         A16: (u . x1) = (u . z) by A1, A12, BVFUNC_1:def 15;

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

        then ((u 'or' a) . x1) = ( FALSE 'or' FALSE ) by A14, BVFUNC_1:def 4;

        hence thesis by A2, A15, A12, A14, A16, BVFUNC_1:def 16;

      end;

    end;

    theorem :: BVFUNC_2:23

    for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((a 'or' u),PA,G)) = (( All (a,PA,G)) 'or' u) by Th22;

    theorem :: BVFUNC_2:24

    for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((a 'or' u),PA,G)) '<' (( Ex (a,PA,G)) 'or' u)

    proof

      let PA be a_partition of Y;

      assume

       A1: u is_independent_of (PA,G);

      let z be Element of Y;

      assume

       A2: (( All ((a 'or' u),PA,G)) . z) = TRUE ;

      

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

      proof

        let x be Element of Y;

        assume x in ( EqClass (z,( CompF (PA,G))));

        then ((a 'or' u) . x) = TRUE by A2, BVFUNC_1:def 16;

        then

         A4: ((a . x) 'or' (u . x)) = TRUE by BVFUNC_1:def 4;

        (u . x) = TRUE or (u . x) = FALSE by XBOOLEAN:def 3;

        hence thesis by A4, BINARITH: 3;

      end;

      

       A5: ((( Ex (a,PA,G)) 'or' u) . z) = ((( Ex (a,PA,G)) . z) 'or' (u . z)) by BVFUNC_1:def 4;

      per cases ;

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

        

        then ((( Ex (a,PA,G)) 'or' u) . z) = ((( Ex (a,PA,G)) . z) 'or' TRUE ) by A5, EQREL_1:def 6

        .= TRUE by BINARITH: 10;

        hence thesis;

      end;

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

        

        then ((( Ex (a,PA,G)) 'or' u) . z) = ( TRUE 'or' (u . z)) by A5, BVFUNC_1:def 17

        .= TRUE by BINARITH: 10;

        hence thesis;

      end;

        suppose

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

        

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

        

         A8: (a . z) <> TRUE by A6, EQREL_1:def 6;

        consider x1 be Element of Y such that

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

         A10: (u . x1) <> TRUE by A6;

        (u . x1) = (u . z) by A1, A7, A9, BVFUNC_1:def 15;

        hence thesis by A3, A8, A10, EQREL_1:def 6;

      end;

    end;

    theorem :: BVFUNC_2:25

    

     Th25: for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((u '&' a),PA,G)) = (u '&' ( All (a,PA,G)))

    proof

      let PA be a_partition of Y;

      

       A1: ( All ((u '&' a),PA,G)) '<' (u '&' ( All (a,PA,G)))

      proof

        let z be Element of Y;

        assume

         A2: (( All ((u '&' a),PA,G)) . z) = TRUE ;

        

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

        proof

          let x be Element of Y;

          assume x in ( EqClass (z,( CompF (PA,G))));

          then

           A4: ((u '&' a) . x) = TRUE by A2, BVFUNC_1:def 16;

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

          hence thesis by A4, MARGREL1: 12;

        end;

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

        proof

          let x be Element of Y;

          assume x in ( EqClass (z,( CompF (PA,G))));

          then

           A5: ((u '&' a) . x) = TRUE by A2, BVFUNC_1:def 16;

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

          hence thesis by A5, MARGREL1: 12;

        end;

        then

         A6: ((u '&' ( All (a,PA,G))) . z) = ((u . z) '&' (( All (a,PA,G)) . z)) & (( All (a,PA,G)) . z) = TRUE by BVFUNC_1:def 16, MARGREL1:def 20;

        (u . z) = TRUE by A3, EQREL_1:def 6;

        hence thesis by A6;

      end;

      assume

       A7: u is_independent_of (PA,G);

      (u '&' ( All (a,PA,G))) '<' ( All ((u '&' a),PA,G))

      proof

        let z be Element of Y;

        

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

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

        then

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

        then

         A10: (( All (a,PA,G)) . z) = TRUE by MARGREL1: 12;

        

         A11: (u . z) = TRUE by A9, MARGREL1: 12;

        for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((u '&' a) . x) = TRUE

        proof

          let x be Element of Y;

          assume x in ( EqClass (z,( CompF (PA,G))));

          then (a . x) = TRUE & (u . x) = (u . z) by A7, A10, A8, BVFUNC_1:def 15, BVFUNC_1:def 16;

          

          then ((u '&' a) . x) = ( TRUE '&' TRUE ) by A11, MARGREL1:def 20

          .= TRUE ;

          hence thesis;

        end;

        hence thesis by BVFUNC_1:def 16;

      end;

      hence thesis by A1, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC_2:26

    for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((a '&' u),PA,G)) = (( All (a,PA,G)) '&' u) by Th25;

    theorem :: BVFUNC_2:27

    for PA be a_partition of Y holds ( All ((a '&' u),PA,G)) '<' (( Ex (a,PA,G)) '&' u)

    proof

      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

       A2: (( All ((a '&' u),PA,G)) . z) = TRUE ;

      

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

      proof

        let x be Element of Y;

        assume x in ( EqClass (z,( CompF (PA,G))));

        then ((a '&' u) . x) = TRUE by A2, BVFUNC_1:def 16;

        then ((a . x) '&' (u . x)) = TRUE by MARGREL1:def 20;

        hence thesis by MARGREL1: 12;

      end;

      

       A4: ((( Ex (a,PA,G)) '&' u) . z) = ((( Ex (a,PA,G)) . z) '&' (u . z)) by MARGREL1:def 20;

      per cases ;

        suppose

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

        now

          per cases ;

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

            then (( Ex (a,PA,G)) . z) = TRUE by BVFUNC_1:def 17;

            

            hence ((( Ex (a,PA,G)) '&' u) . z) = ( TRUE '&' TRUE ) by A4, A5, EQREL_1:def 6

            .= TRUE ;

          end;

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

            then (a . z) <> TRUE by EQREL_1:def 6;

            hence thesis by A3, A1;

          end;

        end;

        hence thesis;

      end;

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

        hence thesis by A3;

      end;

    end;

    theorem :: BVFUNC_2:28

    

     Th28: for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((u 'xor' a),PA,G)) '<' (u 'xor' ( All (a,PA,G)))

    proof

      let PA be a_partition of Y;

      assume

       A1: u is_independent_of (PA,G);

      let z be Element of Y;

      assume

       A2: (( All ((u 'xor' a),PA,G)) . z) = TRUE ;

      

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

      

       A4: ( 'not' FALSE ) = TRUE & ((u 'xor' ( All (a,PA,G))) . z) = ((( All (a,PA,G)) . z) 'xor' (u . z)) by BVFUNC_1:def 5, MARGREL1: 11;

      per cases ;

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

        then

         A5: (u . z) = TRUE & (a . z) = TRUE by EQREL_1:def 6;

        

         A6: ( FALSE '&' TRUE ) = FALSE by MARGREL1: 12;

        ((u 'xor' a) . z) = ((a . z) 'xor' (u . z)) by BVFUNC_1:def 5

        .= FALSE by A5, A6, MARGREL1: 11;

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

      end;

        suppose

         A7: (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (u . x) = TRUE ) & 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

         A8: x1 in ( EqClass (z,( CompF (PA,G)))) and (a . x1) <> TRUE ;

        

         A9: (u . x1) = TRUE by A7, A8;

        

         A10: (( All (a,PA,G)) . z) = FALSE by A7, BVFUNC_1:def 16;

        (u . z) = (u . x1) by A1, A3, A8, BVFUNC_1:def 15;

        

        then ((u 'xor' ( All (a,PA,G))) . z) = ( TRUE 'or' FALSE ) by A4, A10, A9

        .= TRUE by BINARITH: 3;

        hence thesis;

      end;

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

        then

        consider x1 be Element of Y such that

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

         A12: (u . x1) <> TRUE ;

        now

          per cases ;

            suppose

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

            (u . z) = (u . x1) by A1, A3, A11, BVFUNC_1:def 15;

            then

             A14: (u . z) = FALSE by A12, XBOOLEAN:def 3;

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

            

            then ((u 'xor' ( All (a,PA,G))) . z) = ( FALSE 'or' TRUE ) by A4, A14

            .= TRUE by BINARITH: 3;

            hence thesis;

          end;

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

            then

            consider x2 be Element of Y such that

             A15: x2 in ( EqClass (z,( CompF (PA,G)))) and

             A16: (a . x2) <> TRUE ;

            

             A17: (a . x2) = FALSE by A16, XBOOLEAN:def 3;

            (u . x1) = (u . x2) by A1, A11, A15, BVFUNC_1:def 15;

            then

             A18: (u . x2) = FALSE by A12, XBOOLEAN:def 3;

            ((u 'xor' a) . x2) = ((a . x2) 'xor' (u . x2)) by BVFUNC_1:def 5

            .= FALSE by A18, A17, MARGREL1: 12;

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

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: BVFUNC_2:29

    for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((a 'xor' u),PA,G)) '<' (( All (a,PA,G)) 'xor' u) by Th28;

    theorem :: BVFUNC_2:30

    

     Th30: for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((u 'eqv' a),PA,G)) '<' (u 'eqv' ( All (a,PA,G)))

    proof

      let PA be a_partition of Y;

      

       A1: ( 'not' FALSE ) = TRUE by MARGREL1: 11;

      assume

       A2: u is_independent_of (PA,G);

      let z be Element of Y;

      assume

       A3: (( All ((u 'eqv' a),PA,G)) . z) = TRUE ;

      

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

      per cases ;

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

        then

         A5: (( All (a,PA,G)) . z) = TRUE & (u . z) = TRUE by BVFUNC_1:def 16, EQREL_1:def 6;

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

        .= TRUE by A1, A5, MARGREL1: 13;

        hence thesis;

      end;

        suppose

         A6: (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (u . x) = TRUE ) & 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

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

         A8: (a . x1) <> TRUE ;

        

         A9: (u . x1) = TRUE by A6, A7;

        

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

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

        .= ( 'not' ( FALSE 'or' TRUE )) by A1, A9, A10

        .= FALSE by BINARITH: 3, MARGREL1: 11;

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

      end;

        suppose

         A11: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (u . x) = TRUE ) & 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

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

         A13: (u . x1) <> TRUE ;

        

         A14: (a . x1) = TRUE by A11, A12;

        

         A15: (u . x1) = FALSE by A13, XBOOLEAN:def 3;

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

        .= ( 'not' ( TRUE 'or' FALSE )) by A1, A15, A14

        .= FALSE by BINARITH: 3, MARGREL1: 11;

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

      end;

        suppose

         A16: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (u . x) = TRUE ) & 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

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

         A18: (u . x1) <> TRUE ;

        (u . x1) = (u . z) by A2, A4, A17, BVFUNC_1:def 15;

        then

         A19: (u . z) = FALSE by A18, XBOOLEAN:def 3;

        

         A20: (( All (a,PA,G)) . z) = FALSE by A16, BVFUNC_1:def 16;

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

        .= TRUE by A20, A19, MARGREL1: 11, MARGREL1: 13;

        hence thesis;

      end;

    end;

    theorem :: BVFUNC_2:31

    for PA be a_partition of Y st u is_independent_of (PA,G) holds ( All ((a 'eqv' u),PA,G)) '<' (( All (a,PA,G)) 'eqv' u) by Th30;

    theorem :: BVFUNC_2:32

    

     Th32: for PA be a_partition of Y st u is_independent_of (PA,G) holds ( Ex ((u 'or' a),PA,G)) = (u 'or' ( Ex (a,PA,G)))

    proof

      let PA be a_partition of Y;

      assume

       A1: u is_independent_of (PA,G);

      

       A2: ( Ex ((u 'or' a),PA,G)) '<' (u 'or' ( Ex (a,PA,G)))

      proof

        let z be Element of Y;

        

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

        

         A4: ((u 'or' ( Ex (a,PA,G))) . z) = ((u . z) 'or' (( Ex (a,PA,G)) . z)) by BVFUNC_1:def 4;

        assume (( Ex ((u 'or' a),PA,G)) . z) = TRUE ;

        then

        consider x1 be Element of Y such that

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

         A6: ((u 'or' a) . x1) = TRUE by BVFUNC_1:def 17;

        

         A7: (u . x1) = TRUE or (u . x1) = FALSE by XBOOLEAN:def 3;

        

         A8: ((u . x1) 'or' (a . x1)) = TRUE by A6, BVFUNC_1:def 4;

        now

          per cases by A8, A7, BINARITH: 3;

            case

             A9: (u . x1) = TRUE ;

            (u . z) = (u . x1) by A1, A5, A3, BVFUNC_1:def 15;

            hence thesis by A4, A9, BINARITH: 10;

          end;

            case (a . x1) = TRUE ;

            

            then ((u 'or' ( Ex (a,PA,G))) . z) = ((u . z) 'or' TRUE ) by A5, A4, BVFUNC_1:def 17

            .= TRUE by BINARITH: 10;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      (u 'or' ( Ex (a,PA,G))) '<' ( Ex ((u 'or' a),PA,G))

      proof

        let z be Element of Y;

        

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

        assume ((u 'or' ( Ex (a,PA,G))) . z) = TRUE ;

        then

         A11: ((u . z) 'or' (( Ex (a,PA,G)) . z)) = TRUE by BVFUNC_1:def 4;

        

         A12: (( Ex (a,PA,G)) . z) = TRUE or (( Ex (a,PA,G)) . z) = FALSE by XBOOLEAN:def 3;

        now

          per cases by A11, A12, BINARITH: 3;

            case (u . z) = TRUE ;

            

            then ((u 'or' a) . z) = ( TRUE 'or' (a . z)) by BVFUNC_1:def 4

            .= TRUE by BINARITH: 10;

            hence thesis by A10, BVFUNC_1:def 17;

          end;

            case (( Ex (a,PA,G)) . z) = TRUE ;

            then

            consider x1 be Element of Y such that

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

             A14: (a . x1) = TRUE by BVFUNC_1:def 17;

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

            .= TRUE by A14, BINARITH: 10;

            hence thesis by A13, BVFUNC_1:def 17;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A2, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC_2:33

    for PA be a_partition of Y st u is_independent_of (PA,G) holds ( Ex ((a 'or' u),PA,G)) = (( Ex (a,PA,G)) 'or' u) by Th32;

    theorem :: BVFUNC_2:34

    

     Th34: for PA be a_partition of Y st u is_independent_of (PA,G) holds ( Ex ((u '&' a),PA,G)) = (u '&' ( Ex (a,PA,G)))

    proof

      let PA be a_partition of Y;

      assume

       A1: u is_independent_of (PA,G);

      

       A2: ( Ex ((u '&' a),PA,G)) '<' (u '&' ( Ex (a,PA,G)))

      proof

        let z be Element of Y;

        assume (( Ex ((u '&' a),PA,G)) . z) = TRUE ;

        then

        consider x1 be Element of Y such that

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

         A4: ((u '&' a) . x1) = TRUE by BVFUNC_1:def 17;

        

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

        then (a . x1) = TRUE by MARGREL1: 12;

        then

         A6: (( Ex (a,PA,G)) . z) = TRUE by A3, BVFUNC_1:def 17;

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

        then

         A7: (u . z) = (u . x1) by A1, A3, BVFUNC_1:def 15;

        (u . x1) = TRUE by A5, MARGREL1: 12;

        

        then ((u '&' ( Ex (a,PA,G))) . z) = ( TRUE '&' TRUE ) by A6, A7, MARGREL1:def 20

        .= TRUE ;

        hence thesis;

      end;

      (u '&' ( Ex (a,PA,G))) '<' ( Ex ((u '&' a),PA,G))

      proof

        let z be Element of Y;

        assume ((u '&' ( Ex (a,PA,G))) . z) = TRUE ;

        then

         A8: ((u . z) '&' (( Ex (a,PA,G)) . z)) = TRUE by MARGREL1:def 20;

        then

         A9: (u . z) = TRUE by MARGREL1: 12;

        (( Ex (a,PA,G)) . z) = TRUE by A8, MARGREL1: 12;

        then

        consider x1 be Element of Y such that

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

         A11: (a . x1) = TRUE by BVFUNC_1:def 17;

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

        then (u . x1) = (u . z) by A1, A10, BVFUNC_1:def 15;

        

        then ((u '&' a) . x1) = ( TRUE '&' TRUE ) by A9, A11, MARGREL1:def 20

        .= TRUE ;

        hence thesis by A10, BVFUNC_1:def 17;

      end;

      hence thesis by A2, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC_2:35

    for PA be a_partition of Y st u is_independent_of (PA,G) holds ( Ex ((a '&' u),PA,G)) = (( Ex (a,PA,G)) '&' u) by Th34;

    theorem :: BVFUNC_2:36

    for PA be a_partition of Y holds (u 'imp' ( Ex (a,PA,G))) '<' ( Ex ((u 'imp' a),PA,G))

    proof

      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 ((u 'imp' ( Ex (a,PA,G))) . z) = TRUE ;

      then

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

      

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

      now

        per cases by A2, A3, BINARITH: 3;

          case

           A4: ( 'not' (u . z)) = TRUE ;

          ((u 'imp' a) . z) = (( 'not' (u . z)) 'or' (a . z)) by BVFUNC_1:def 8

          .= TRUE by A4, BINARITH: 10;

          hence thesis by A1, BVFUNC_1:def 17;

        end;

          case (( Ex (a,PA,G)) . z) = TRUE ;

          then

          consider x1 be Element of Y such that

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

           A6: (a . x1) = TRUE by BVFUNC_1:def 17;

          ((u 'imp' a) . x1) = (( 'not' (u . x1)) 'or' (a . x1)) by BVFUNC_1:def 8

          .= TRUE by A6, BINARITH: 10;

          hence thesis by A5, BVFUNC_1:def 17;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_2:37

    for PA be a_partition of Y holds (( Ex (a,PA,G)) 'imp' u) '<' ( Ex ((a 'imp' u),PA,G))

    proof

      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 ((( Ex (a,PA,G)) 'imp' u) . z) = TRUE ;

      then

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

      

       A3: (u . z) = TRUE or (u . z) = FALSE by XBOOLEAN:def 3;

      now

        per cases by A2, A3, BINARITH: 3;

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

          then

           A4: (a . z) <> TRUE by A1, BVFUNC_1:def 17, MARGREL1: 11;

          ((a 'imp' u) . z) = (( 'not' (a . z)) 'or' (u . z)) by BVFUNC_1:def 8

          .= ( TRUE 'or' (u . z)) by A4, MARGREL1: 11, XBOOLEAN:def 3

          .= TRUE by BINARITH: 10;

          hence thesis by A1, BVFUNC_1:def 17;

        end;

          case

           A5: (u . z) = TRUE ;

          ((a 'imp' u) . z) = (( 'not' (a . z)) 'or' (u . z)) by BVFUNC_1:def 8

          .= TRUE by A5, BINARITH: 10;

          hence thesis by A1, BVFUNC_1:def 17;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_2:38

    

     Th38: for PA be a_partition of Y st u is_independent_of (PA,G) holds (u 'xor' ( Ex (a,PA,G))) '<' ( Ex ((u 'xor' a),PA,G))

    proof

      let PA be a_partition of Y;

      

       A1: ( 'not' FALSE ) = TRUE by MARGREL1: 11;

      assume

       A2: u is_independent_of (PA,G);

      let z be Element of Y;

      

       A3: ((u 'xor' ( Ex (a,PA,G))) . z) = ((u . z) 'xor' (( Ex (a,PA,G)) . z)) by BVFUNC_1:def 5

      .= ((( 'not' (u . z)) '&' (( Ex (a,PA,G)) . z)) 'or' ((u . z) '&' ( 'not' (( Ex (a,PA,G)) . z))));

      

       A4: ((u . z) '&' ( 'not' (( Ex (a,PA,G)) . z))) = TRUE or ((u . z) '&' ( 'not' (( Ex (a,PA,G)) . z))) = FALSE by XBOOLEAN:def 3;

      

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

      assume

       A6: ((u 'xor' ( Ex (a,PA,G))) . z) = TRUE ;

      now

        per cases by A6, A3, A4, BINARITH: 3;

          case

           A7: (( 'not' (u . z)) '&' (( Ex (a,PA,G)) . z)) = TRUE ;

          then (( Ex (a,PA,G)) . z) = TRUE by MARGREL1: 12;

          then

          consider x1 be Element of Y such that

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

           A9: (a . x1) = TRUE by BVFUNC_1:def 17;

          

           A10: (u . z) = (u . x1) by A2, A5, A8, BVFUNC_1:def 15;

          

           A11: ( 'not' (u . z)) = TRUE by A7, MARGREL1: 12;

          ((u 'xor' a) . x1) = ((u . x1) 'xor' (a . x1)) by BVFUNC_1:def 5

          .= ( TRUE 'or' FALSE ) by A11, A9, A10, MARGREL1: 11

          .= TRUE by BINARITH: 10;

          hence thesis by A8, BVFUNC_1:def 17;

        end;

          case

           A12: ((u . z) '&' ( 'not' (( Ex (a,PA,G)) . z))) = TRUE ;

          then ( 'not' (( Ex (a,PA,G)) . z)) = TRUE by MARGREL1: 12;

          then (a . z) <> TRUE by A5, BVFUNC_1:def 17, MARGREL1: 11;

          then

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

          

           A14: (u . z) = TRUE by A12, MARGREL1: 12;

          ((u 'xor' a) . z) = ((u . z) 'xor' (a . z)) by BVFUNC_1:def 5

          .= ( FALSE 'or' TRUE ) by A1, A14, A13

          .= TRUE by BINARITH: 10;

          hence thesis by A5, BVFUNC_1:def 17;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_2:39

    for PA be a_partition of Y st u is_independent_of (PA,G) holds (( Ex (a,PA,G)) 'xor' u) '<' ( Ex ((a 'xor' u),PA,G)) by Th38;