bvfunc_1.miz



    begin

    definition

      let k,l be boolean object;

      :: original: <=

      redefine

      :: BVFUNC_1:def1

      pred k <= l means (k => l) = TRUE ;

      compatibility

      proof

        (l = 0 or l = 1) & (k = 0 or k = 1) by XBOOLEAN:def 3;

        hence thesis;

      end;

    end

    begin

    reserve Y for non empty set;

    reserve B for Subset of Y;

    scheme :: BVFUNC_1:sch1

    BVFUniq1 { Y() -> non empty set , F( set) -> set } :

for f1,f2 be Function of Y(), BOOLEAN st (for x be Element of Y() holds (f1 . x) = F(x)) & (for x be Element of Y() holds (f2 . x) = F(x)) holds f1 = f2;

      let f1,f2 be Function of Y(), BOOLEAN ;

      assume that

       A1: for x be Element of Y() holds (f1 . x) = F(x) and

       A2: for x be Element of Y() holds (f2 . x) = F(x);

      let u be Element of Y();

      

      thus (f2 . u) = F(u) by A2

      .= (f1 . u) by A1;

    end;

    definition

      let Y;

      let a be Function of Y, BOOLEAN ;

      :: original: 'not'

      redefine

      func 'not' a -> Function of Y, BOOLEAN ;

      coherence

      proof

        reconsider a as Function of Y, BOOLEAN ;

        ( 'not' a) is Function of Y, BOOLEAN ;

        hence thesis;

      end;

      let b be Function of Y, BOOLEAN ;

      :: original: '&'

      redefine

      func a '&' b -> Function of Y, BOOLEAN ;

      coherence

      proof

        reconsider a, b as Function of Y, BOOLEAN ;

        (a '&' b) is Function of Y, BOOLEAN ;

        hence thesis;

      end;

    end

    definition

      let p,q be boolean-valued Function;

      :: BVFUNC_1:def2

      func p 'or' q -> boolean-valued Function means

      : Def2: ( dom it ) = (( dom p) /\ ( dom q)) & for x be object st x in ( dom it ) holds (it . x) = ((p . x) 'or' (q . x));

      existence

      proof

        deffunc F( object) = ((p . $1) 'or' (q . $1));

        consider s be Function such that

         A1: ( dom s) = (( dom p) /\ ( dom q)) & for x be object st x in (( dom p) /\ ( dom q)) holds (s . x) = F(x) from FUNCT_1:sch 3;

        s is boolean-valued

        proof

          let x be object;

          assume x in ( rng s);

          then

          consider y be object such that

           A2: y in ( dom s) & x = (s . y) by FUNCT_1:def 3;

          x = ((p . y) 'or' (q . y)) by A1, A2;

          then x = FALSE or x = TRUE by XBOOLEAN:def 3;

          hence thesis;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let s1,s2 be boolean-valued Function such that

         A3: ( dom s1) = (( dom p) /\ ( dom q)) and

         A4: for x be object st x in ( dom s1) holds (s1 . x) = ((p . x) 'or' (q . x)) and

         A5: ( dom s2) = (( dom p) /\ ( dom q)) and

         A6: for x be object st x in ( dom s2) holds (s2 . x) = ((p . x) 'or' (q . x));

        for x be object st x in ( dom s1) holds (s1 . x) = (s2 . x)

        proof

          let x be object;

          assume

           A7: x in ( dom s1);

          then (s1 . x) = ((p . x) 'or' (q . x)) by A4;

          hence thesis by A3, A5, A6, A7;

        end;

        hence thesis by A3, A5, FUNCT_1: 2;

      end;

      commutativity ;

      idempotence ;

      :: BVFUNC_1:def3

      func p 'xor' q -> Function means

      : Def3: ( dom it ) = (( dom p) /\ ( dom q)) & for x be set st x in ( dom it ) holds (it . x) = ((p . x) 'xor' (q . x));

      existence

      proof

        deffunc F( object) = ((p . $1) 'xor' (q . $1));

        consider s be Function such that

         A8: ( dom s) = (( dom p) /\ ( dom q)) & for x be object st x in (( dom p) /\ ( dom q)) holds (s . x) = F(x) from FUNCT_1:sch 3;

        take s;

        thus thesis by A8;

      end;

      uniqueness

      proof

        let s1,s2 be Function such that

         A9: ( dom s1) = (( dom p) /\ ( dom q)) and

         A10: for x be set st x in ( dom s1) holds (s1 . x) = ((p . x) 'xor' (q . x)) and

         A11: ( dom s2) = (( dom p) /\ ( dom q)) and

         A12: for x be set st x in ( dom s2) holds (s2 . x) = ((p . x) 'xor' (q . x));

        for x be object st x in ( dom s1) holds (s1 . x) = (s2 . x)

        proof

          let x be object;

          assume

           A13: x in ( dom s1);

          then (s1 . x) = ((p . x) 'xor' (q . x)) by A10;

          hence thesis by A9, A11, A12, A13;

        end;

        hence thesis by A9, A11, FUNCT_1: 2;

      end;

      commutativity ;

    end

    registration

      let p,q be boolean-valued Function;

      cluster (p 'xor' q) -> boolean-valued;

      coherence

      proof

        let x be object;

        assume x in ( rng (p 'xor' q));

        then

        consider y be object such that

         A1: y in ( dom (p 'xor' q)) & x = ((p 'xor' q) . y) by FUNCT_1:def 3;

        x = ((p . y) 'xor' (q . y)) by A1, Def3;

        then x = FALSE or x = TRUE by XBOOLEAN:def 3;

        hence thesis;

      end;

    end

    definition

      let A be non empty set;

      let p,q be Function of A, BOOLEAN ;

      :: original: 'or'

      redefine

      :: BVFUNC_1:def4

      func p 'or' q -> Function of A, BOOLEAN means

      : Def4: for x be Element of A holds (it . x) = ((p . x) 'or' (q . x));

      coherence

      proof

        ( dom p) = A & ( dom q) = A by PARTFUN1:def 2;

        

        then

         A1: ( dom (p 'or' q)) = (A /\ A) by Def2

        .= A;

        ( rng (p 'or' q)) c= BOOLEAN by MARGREL1:def 16;

        hence thesis by A1, FUNCT_2: 2;

      end;

      compatibility

      proof

        let IT be Function of A, BOOLEAN ;

        

         A2: ( dom IT) = A by FUNCT_2:def 1;

        hereby

          assume

           A3: IT = (p 'or' q);

          let x be Element of A;

          ( dom p) = A & ( dom q) = A by FUNCT_2:def 1;

          

          then ( dom (p 'or' q)) = (A /\ A) by Def2

          .= A;

          hence (IT . x) = ((p . x) 'or' (q . x)) by A3, Def2;

        end;

        

         A4: ( dom q) = A by FUNCT_2:def 1;

        

         A5: ( dom IT) = (A /\ A) by FUNCT_2:def 1

        .= (( dom p) /\ ( dom q)) by A4, FUNCT_2:def 1;

        assume for x be Element of A holds (IT . x) = ((p . x) 'or' (q . x));

        then for x be object st x in ( dom IT) holds (IT . x) = ((p . x) 'or' (q . x)) by A2;

        hence thesis by A5, Def2;

      end;

      :: original: 'xor'

      redefine

      :: BVFUNC_1:def5

      func p 'xor' q -> Function of A, BOOLEAN means for x be Element of A holds (it . x) = ((p . x) 'xor' (q . x));

      coherence

      proof

        ( dom p) = A & ( dom q) = A by PARTFUN1:def 2;

        

        then

         A6: ( dom (p 'xor' q)) = (A /\ A) by Def3

        .= A;

        ( rng (p 'xor' q)) c= BOOLEAN by MARGREL1:def 16;

        hence thesis by A6, FUNCT_2: 2;

      end;

      compatibility

      proof

        let IT be Function of A, BOOLEAN ;

        

         A7: ( dom IT) = A by FUNCT_2:def 1;

        hereby

          assume

           A8: IT = (p 'xor' q);

          let x be Element of A;

          ( dom p) = A & ( dom q) = A by FUNCT_2:def 1;

          

          then ( dom (p 'xor' q)) = (A /\ A) by Def3

          .= A;

          hence (IT . x) = ((p . x) 'xor' (q . x)) by A8, Def3;

        end;

        

         A9: ( dom q) = A by FUNCT_2:def 1;

        

         A10: ( dom IT) = (A /\ A) by FUNCT_2:def 1

        .= (( dom p) /\ ( dom q)) by A9, FUNCT_2:def 1;

        assume for x be Element of A holds (IT . x) = ((p . x) 'xor' (q . x));

        then for x be set st x in ( dom IT) holds (IT . x) = ((p . x) 'xor' (q . x)) by A7;

        hence thesis by A10, Def3;

      end;

    end

    definition

      let p,q be boolean-valued Function;

      :: BVFUNC_1:def6

      func p 'imp' q -> Function means

      : Def6: ( dom it ) = (( dom p) /\ ( dom q)) & for x be set st x in ( dom it ) holds (it . x) = ((p . x) => (q . x));

      existence

      proof

        deffunc F( object) = ((p . $1) => (q . $1));

        consider s be Function such that

         A1: ( dom s) = (( dom p) /\ ( dom q)) & for x be object st x in (( dom p) /\ ( dom q)) holds (s . x) = F(x) from FUNCT_1:sch 3;

        take s;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let s1,s2 be Function such that

         A2: ( dom s1) = (( dom p) /\ ( dom q)) and

         A3: for x be set st x in ( dom s1) holds (s1 . x) = ((p . x) => (q . x)) and

         A4: ( dom s2) = (( dom p) /\ ( dom q)) and

         A5: for x be set st x in ( dom s2) holds (s2 . x) = ((p . x) => (q . x));

        for x be object st x in ( dom s1) holds (s1 . x) = (s2 . x)

        proof

          let x be object;

          assume

           A6: x in ( dom s1);

          then (s1 . x) = ((p . x) => (q . x)) by A3;

          hence thesis by A2, A4, A5, A6;

        end;

        hence thesis by A2, A4, FUNCT_1: 2;

      end;

      :: BVFUNC_1:def7

      func p 'eqv' q -> Function means

      : Def7: ( dom it ) = (( dom p) /\ ( dom q)) & for x be set st x in ( dom it ) holds (it . x) = ((p . x) <=> (q . x));

      existence

      proof

        deffunc F( object) = ((p . $1) <=> (q . $1));

        consider s be Function such that

         A7: ( dom s) = (( dom p) /\ ( dom q)) & for x be object st x in (( dom p) /\ ( dom q)) holds (s . x) = F(x) from FUNCT_1:sch 3;

        take s;

        thus thesis by A7;

      end;

      uniqueness

      proof

        let s1,s2 be Function such that

         A8: ( dom s1) = (( dom p) /\ ( dom q)) and

         A9: for x be set st x in ( dom s1) holds (s1 . x) = ((p . x) <=> (q . x)) and

         A10: ( dom s2) = (( dom p) /\ ( dom q)) and

         A11: for x be set st x in ( dom s2) holds (s2 . x) = ((p . x) <=> (q . x));

        for x be object st x in ( dom s1) holds (s1 . x) = (s2 . x)

        proof

          let x be object;

          assume

           A12: x in ( dom s1);

          then (s1 . x) = ((p . x) <=> (q . x)) by A9;

          hence thesis by A8, A10, A11, A12;

        end;

        hence thesis by A8, A10, FUNCT_1: 2;

      end;

      commutativity ;

    end

    registration

      let p,q be boolean-valued Function;

      cluster (p 'imp' q) -> boolean-valued;

      coherence

      proof

        let x be object;

        assume x in ( rng (p 'imp' q));

        then

        consider y be object such that

         A1: y in ( dom (p 'imp' q)) & x = ((p 'imp' q) . y) by FUNCT_1:def 3;

        x = ((p . y) => (q . y)) by A1, Def6

        .= (( 'not' (p . y)) 'or' (q . y));

        then x = FALSE or x = TRUE by XBOOLEAN:def 3;

        hence thesis;

      end;

      cluster (p 'eqv' q) -> boolean-valued;

      coherence

      proof

        let x be object;

        assume x in ( rng (p 'eqv' q));

        then

        consider y be object such that

         A2: y in ( dom (p 'eqv' q)) & x = ((p 'eqv' q) . y) by FUNCT_1:def 3;

        x = ( 'not' ((p . y) 'xor' (q . y))) by A2, Def7;

        then x = FALSE or x = TRUE by XBOOLEAN:def 3;

        hence thesis;

      end;

    end

    definition

      let A be non empty set;

      let p,q be Function of A, BOOLEAN ;

      :: original: 'imp'

      redefine

      :: BVFUNC_1:def8

      func p 'imp' q -> Function of A, BOOLEAN means

      : Def8: for x be Element of A holds (it . x) = (( 'not' (p . x)) 'or' (q . x));

      coherence

      proof

        ( dom p) = A & ( dom q) = A by PARTFUN1:def 2;

        

        then

         A1: ( dom (p 'imp' q)) = (A /\ A) by Def6

        .= A;

        ( rng (p 'imp' q)) c= BOOLEAN by MARGREL1:def 16;

        hence thesis by A1, FUNCT_2: 2;

      end;

      compatibility

      proof

        let IT be Function of A, BOOLEAN ;

        

         A2: ( dom q) = A by FUNCT_2:def 1;

        hereby

          assume

           A3: IT = (p 'imp' q);

          let x be Element of A;

          ( dom p) = A & ( dom q) = A by FUNCT_2:def 1;

          

          then ( dom (p 'imp' q)) = (A /\ A) by Def6

          .= A;

          

          hence (IT . x) = ((p . x) => (q . x)) by A3, Def6

          .= (( 'not' (p . x)) 'or' (q . x));

        end;

        assume

         A4: for x be Element of A holds (IT . x) = (( 'not' (p . x)) 'or' (q . x));

        

         A5: for x be set st x in ( dom IT) holds (IT . x) = ((p . x) => (q . x))

        proof

          let x be set;

          assume x in ( dom IT);

          then

          reconsider x as Element of A by FUNCT_2:def 1;

          (IT . x) = (( 'not' (p . x)) 'or' (q . x)) by A4;

          hence thesis;

        end;

        ( dom IT) = (A /\ A) by FUNCT_2:def 1

        .= (( dom p) /\ ( dom q)) by A2, FUNCT_2:def 1;

        hence thesis by A5, Def6;

      end;

      :: original: 'eqv'

      redefine

      :: BVFUNC_1:def9

      func p 'eqv' q -> Function of A, BOOLEAN means

      : Def9: for x be Element of A holds (it . x) = ( 'not' ((p . x) 'xor' (q . x)));

      coherence

      proof

        ( dom p) = A & ( dom q) = A by PARTFUN1:def 2;

        

        then

         A6: ( dom (p 'eqv' q)) = (A /\ A) by Def7

        .= A;

        ( rng (p 'eqv' q)) c= BOOLEAN by MARGREL1:def 16;

        hence thesis by A6, FUNCT_2: 2;

      end;

      compatibility

      proof

        let IT be Function of A, BOOLEAN ;

        

         A7: ( dom q) = A by FUNCT_2:def 1;

        hereby

          assume

           A8: IT = (p 'eqv' q);

          let x be Element of A;

          ( dom p) = A & ( dom q) = A by FUNCT_2:def 1;

          

          then ( dom (p 'eqv' q)) = (A /\ A) by Def7

          .= A;

          hence (IT . x) = ( 'not' ((p . x) 'xor' (q . x))) by A8, Def7;

        end;

        assume

         A9: for x be Element of A holds (IT . x) = ( 'not' ((p . x) 'xor' (q . x)));

        

         A10: for x be set st x in ( dom IT) holds (IT . x) = ((p . x) <=> (q . x))

        proof

          let x be set;

          assume x in ( dom IT);

          then

          reconsider x as Element of A by FUNCT_2:def 1;

          (IT . x) = ( 'not' ((p . x) 'xor' (q . x))) by A9;

          hence thesis;

        end;

        ( dom IT) = (A /\ A) by FUNCT_2:def 1

        .= (( dom p) /\ ( dom q)) by A7, FUNCT_2:def 1;

        hence thesis by A10, Def7;

      end;

    end

    definition

      let Y;

      :: BVFUNC_1:def10

      func O_el (Y) -> Function of Y, BOOLEAN means

      : Def10: for x be Element of Y holds (it . x) = FALSE ;

      existence

      proof

        reconsider f = (Y --> FALSE ) as Function of Y, BOOLEAN ;

        reconsider f as Function of Y, BOOLEAN ;

        take f;

        let x be Element of Y;

        thus thesis;

      end;

      uniqueness

      proof

        deffunc F( set) = FALSE ;

        thus for f1,f2 be Function of Y, BOOLEAN st (for x be Element of Y holds (f1 . x) = F(x)) & (for x be Element of Y holds (f2 . x) = F(x)) holds f1 = f2 from BVFUniq1;

      end;

    end

    definition

      let Y;

      :: BVFUNC_1:def11

      func I_el (Y) -> Function of Y, BOOLEAN means

      : Def11: for x be Element of Y holds (it . x) = TRUE ;

      existence

      proof

        reconsider f = (Y --> TRUE ) as Function of Y, BOOLEAN ;

        reconsider f as Function of Y, BOOLEAN ;

        take f;

        let x be Element of Y;

        thus thesis;

      end;

      uniqueness

      proof

        deffunc F( set) = TRUE ;

        thus for f1,f2 be Function of Y, BOOLEAN st (for x be Element of Y holds (f1 . x) = F(x)) & (for x be Element of Y holds (f2 . x) = F(x)) holds f1 = f2 from BVFUniq1;

      end;

    end

    ::$Canceled

    theorem :: BVFUNC_1:2

    

     Th1: ( 'not' ( I_el Y)) = ( O_el Y) & ( 'not' ( O_el Y)) = ( I_el Y)

    proof

      

       A1: for x be Element of Y holds (( 'not' ( O_el Y)) . x) = TRUE

      proof

        let x be Element of Y;

        (( 'not' ( O_el Y)) . x) = ( 'not' (( O_el Y) . x)) & (( O_el Y) . x) = FALSE by Def10, MARGREL1:def 19;

        hence thesis;

      end;

      for x be Element of Y holds (( 'not' ( I_el Y)) . x) = FALSE

      proof

        let x be Element of Y;

        (( 'not' ( I_el Y)) . x) = ( 'not' (( I_el Y) . x)) & (( I_el Y) . x) = TRUE by Def11, MARGREL1:def 19;

        hence thesis;

      end;

      hence thesis by A1, Def10, Def11;

    end;

    theorem :: BVFUNC_1:3

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

    theorem :: BVFUNC_1:4

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

    proof

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

      let x be Element of Y;

      

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

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

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

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

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

    end;

    theorem :: BVFUNC_1:5

    

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

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

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

      .= ((a . x) '&' FALSE ) by Def10

      .= (( O_el Y) . x) by Def10;

    end;

    theorem :: BVFUNC_1:6

    

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

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

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

      .= ((a . x) '&' TRUE ) by Def11

      .= (a . x);

    end;

    theorem :: BVFUNC_1:7

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

    theorem :: BVFUNC_1:8

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

    proof

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

      let x be Element of Y;

      

      thus (((a 'or' b) 'or' c) . x) = (((a 'or' b) . x) 'or' (c . x)) by Def4

      .= (((a . x) 'or' (b . x)) 'or' (c . x)) by Def4

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

      .= ((a . x) 'or' ((b 'or' c) . x)) by Def4

      .= ((a 'or' (b 'or' c)) . x) by Def4;

    end;

    theorem :: BVFUNC_1:9

    

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

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

      thus ((a 'or' ( O_el Y)) . x) = ((a . x) 'or' (( O_el Y) . x)) by Def4

      .= ((a . x) 'or' FALSE ) by Def10

      .= (a . x);

    end;

    theorem :: BVFUNC_1:10

    

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

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

      thus ((a 'or' ( I_el Y)) . x) = ((a . x) 'or' (( I_el Y) . x)) by Def4

      .= ((a . x) 'or' TRUE ) by Def11

      .= (( I_el Y) . x) by Def11;

    end;

    theorem :: BVFUNC_1:11

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

    proof

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

      let x be Element of Y;

      

      thus (((a '&' b) 'or' c) . x) = (((a '&' b) . x) 'or' (c . x)) by Def4

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

      .= (((a . x) 'or' (c . x)) '&' ((b . x) 'or' (c . x))) by XBOOLEAN: 9

      .= (((a . x) 'or' (c . x)) '&' ((b 'or' c) . x)) by Def4

      .= (((a 'or' c) . x) '&' ((b 'or' c) . x)) by Def4

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

    end;

    theorem :: BVFUNC_1:12

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

    proof

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

      let x be Element of Y;

      

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

      .= (((a . x) 'or' (b . x)) '&' (c . x)) by Def4

      .= (((a . x) '&' (c . x)) 'or' ((b . x) '&' (c . x))) by XBOOLEAN: 8

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

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

      .= (((a '&' c) 'or' (b '&' c)) . x) by Def4;

    end;

    theorem :: BVFUNC_1:13

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

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

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

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

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

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

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

    end;

    theorem :: BVFUNC_1:14

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

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

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

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

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

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

      .= ((( 'not' a) 'or' ( 'not' b)) . x) by Def4;

    end;

    definition

      let Y;

      let a,b be Function of Y, BOOLEAN ;

      :: BVFUNC_1:def12

      pred a '<' b means for x be Element of Y st (a . x) = TRUE holds (b . x) = TRUE ;

      reflexivity ;

    end

    theorem :: BVFUNC_1:15

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

    proof

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

      

       A1: for a,b,c be Function of Y, BOOLEAN holds a '<' b & b '<' a implies a = b

      proof

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

        assume

         A2: a '<' b & b '<' a;

        let x be Element of Y;

        (a . x) = FALSE & (b . x) = FALSE or (a . x) = FALSE & (b . x) = TRUE or (a . x) = TRUE & (b . x) = FALSE or (a . x) = TRUE & (b . x) = TRUE by XBOOLEAN:def 3;

        hence thesis by A2;

      end;

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

      proof

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

        assume that

         A3: a '<' b and

         A4: b '<' c;

        for x be Element of Y st (a . x) = TRUE holds (c . x) = TRUE

        proof

          let x be Element of Y;

          (b . x) = TRUE implies (c . x) = TRUE by A4;

          hence thesis by A3;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: BVFUNC_1:16

    

     Th15: for a,b be Function of Y, BOOLEAN holds (a 'imp' b) = ( I_el Y) iff a '<' b

    proof

      let a,b be Function of Y, BOOLEAN ;

      

       A1: for a,b be Function of Y, BOOLEAN holds a '<' b implies (a 'imp' b) = ( I_el Y)

      proof

        let a,b be Function of Y, BOOLEAN ;

        assume

         A2: a '<' b;

        

         A3: for x be Element of Y holds (( 'not' (a . x)) 'or' (b . x)) = TRUE

        proof

          let x be Element of Y;

          (a . x) = FALSE & (b . x) = FALSE or (a . x) = FALSE & (b . x) = TRUE or (a . x) = TRUE & (b . x) = TRUE by A2, XBOOLEAN:def 3;

          hence thesis;

        end;

        let x be Element of Y;

        ((a 'imp' b) . x) = (( 'not' (a . x)) 'or' (b . x)) & (( I_el Y) . x) = TRUE by Def8, Def11;

        hence thesis by A3;

      end;

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

      proof

        let a,b be Function of Y, BOOLEAN ;

        assume

         A4: (a 'imp' b) = ( I_el Y);

        

         A5: for x be Element of Y holds (( 'not' (a . x)) 'or' (b . x)) = TRUE

        proof

          let x be Element of Y;

          ((a 'imp' b) . x) = (( 'not' (a . x)) 'or' (b . x)) by Def8;

          hence thesis by A4, Def11;

        end;

        for x be Element of Y holds (a . x) = FALSE & (b . x) = FALSE or (a . x) = FALSE & (b . x) = TRUE or (a . x) = TRUE & (b . x) = TRUE

        proof

          let x be Element of Y;

          

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

          (( 'not' (a . x)) 'or' (b . x)) = TRUE by A5;

          hence thesis by A6;

        end;

        then for x be Element of Y st (a . x) = TRUE holds (b . x) = TRUE ;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: BVFUNC_1:17

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

    proof

      let a,b be Function of Y, BOOLEAN ;

      

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

      proof

        let a,b be Function of Y, BOOLEAN ;

        assume

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

        

         A3: for x be Element of Y holds ((( 'not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ( 'not' (b . x)))) = FALSE

        proof

          let x be Element of Y;

          ((a 'eqv' b) . x) = ( 'not' ((a . x) 'xor' (b . x))) by Def9;

          then ( 'not' ((a . x) 'xor' (b . x))) = TRUE by A2, Def11;

          hence thesis;

        end;

        

         A4: for x be Element of Y holds (( 'not' (a . x)) '&' (b . x)) = FALSE & ((a . x) '&' ( 'not' (b . x))) = FALSE

        proof

          let x be Element of Y;

          

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

          ((( 'not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ( 'not' (b . x)))) = FALSE by A3;

          hence thesis by A5;

        end;

        let x be Element of Y;

        (( 'not' (a . x)) '&' (b . x)) = FALSE by A4;

        then

         A6: ( 'not' (a . x)) = TRUE & (b . x) = FALSE or ( 'not' (a . x)) = FALSE & (b . x) = FALSE or ( 'not' (a . x)) = FALSE & (b . x) = TRUE by MARGREL1: 12, XBOOLEAN:def 3;

        ((a . x) '&' ( 'not' (b . x))) = FALSE by A4;

        hence thesis by A6;

      end;

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

      proof

        let a,b be Function of Y, BOOLEAN ;

        assume

         A7: a = b;

        

         A8: for x be Element of Y holds (( 'not' (a . x)) '&' (b . x)) = FALSE & ((a . x) '&' ( 'not' (b . x))) = FALSE

        proof

          let x be Element of Y;

          (b . x) = TRUE iff ( 'not' (b . x)) = FALSE ;

          then (a . x) = FALSE & ( 'not' (b . x)) = TRUE or (a . x) = TRUE & ( 'not' (b . x)) = FALSE by A7, XBOOLEAN:def 3;

          hence thesis;

        end;

        let x be Element of Y;

        ((a . x) '&' ( 'not' (b . x))) = FALSE by A8;

        then ( 'not' ((a . x) 'xor' (b . x))) = TRUE by A8;

        then ((a 'eqv' b) . x) = TRUE by Def9;

        hence thesis by Def11;

      end;

      hence thesis by A1;

    end;

    theorem :: BVFUNC_1:18

    for a be Function of Y, BOOLEAN holds ( O_el Y) '<' a & a '<' ( I_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      

       A1: (( O_el Y) 'imp' a) = ( I_el Y)

      proof

        let x be Element of Y;

        ((( O_el Y) 'imp' a) . x) = (( 'not' (( O_el Y) . x)) 'or' (a . x)) by Def8;

        then ((( O_el Y) 'imp' a) . x) = ( TRUE 'or' (a . x)) by Def10;

        hence thesis by Def11;

      end;

      (a 'imp' ( I_el Y)) = ( I_el Y)

      proof

        let x be Element of Y;

        ((a 'imp' ( I_el Y)) . x) = (( 'not' (a . x)) 'or' (( I_el Y) . x)) by Def8;

        then ((a 'imp' ( I_el Y)) . x) = (( 'not' (a . x)) 'or' TRUE ) by Def11;

        hence thesis by Def11;

      end;

      hence thesis by A1, Th15;

    end;

    begin

    definition

      let Y;

      let a be Function of Y, BOOLEAN ;

      :: BVFUNC_1:def13

      func B_INF (a) -> Function of Y, BOOLEAN equals

      : Def13: ( I_el Y) if for x be Element of Y holds (a . x) = TRUE

      otherwise ( O_el Y);

      correctness ;

      :: BVFUNC_1:def14

      func B_SUP (a) -> Function of Y, BOOLEAN equals

      : Def14: ( O_el Y) if for x be Element of Y holds (a . x) = FALSE

      otherwise ( I_el Y);

      correctness ;

    end

    theorem :: BVFUNC_1:19

    

     Th18: for a be Function of Y, BOOLEAN holds ( 'not' ( B_INF a)) = ( B_SUP ( 'not' a)) & ( 'not' ( B_SUP a)) = ( B_INF ( 'not' a))

    proof

      let a be Function of Y, BOOLEAN ;

      

       A1: (for x be Element of Y holds (( 'not' a) . x) = TRUE ) implies for x be Element of Y holds (a . x) = FALSE

      proof

        assume

         A2: for x be Element of Y holds (( 'not' a) . x) = TRUE ;

        let x be Element of Y;

        (( 'not' a) . x) = TRUE by A2;

        then ( 'not' (a . x)) = TRUE by MARGREL1:def 19;

        hence thesis;

      end;

      

       A3: (for x be Element of Y holds (( 'not' a) . x) = FALSE ) implies for x be Element of Y holds (a . x) = TRUE

      proof

        assume

         A4: for x be Element of Y holds (( 'not' a) . x) = FALSE ;

        let x be Element of Y;

        (( 'not' a) . x) = FALSE by A4;

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

        hence thesis;

      end;

       A5:

      now

        assume

         A6: (for x be Element of Y holds (a . x) = TRUE ) or for x be Element of Y holds (a . x) = FALSE ;

        now

          per cases by A6;

            case

             A7: (for x be Element of Y holds (a . x) = TRUE ) & not (for x be Element of Y holds (a . x) = FALSE );

            

             A8: for x be Element of Y holds (( 'not' a) . x) = FALSE

            proof

              let x be Element of Y;

              ( 'not' TRUE ) = FALSE ;

              then ( 'not' (a . x)) = FALSE by A7;

              hence thesis by MARGREL1:def 19;

            end;

            ( B_INF a) = ( I_el Y) by A7, Def13;

            then

             A9: ( 'not' ( B_INF a)) = ( O_el Y) by Th1;

            ( B_INF ( 'not' a)) = ( O_el Y) & ( 'not' ( B_SUP a)) = ( 'not' ( I_el Y)) by A1, A7, Def13, Def14;

            hence thesis by A9, A8, Def14, Th1;

          end;

            case

             A10: (for x be Element of Y holds (a . x) = FALSE ) & not (for x be Element of Y holds (a . x) = TRUE );

            

             A11: for x be Element of Y holds (( 'not' a) . x) = TRUE

            proof

              let x be Element of Y;

              ( 'not' FALSE ) = TRUE ;

              then ( 'not' (a . x)) = TRUE by A10;

              hence thesis by MARGREL1:def 19;

            end;

            ( 'not' ( B_SUP a)) = ( 'not' ( O_el Y)) by A10, Def14;

            then

             A12: ( 'not' ( B_SUP a)) = ( I_el Y) by Th1;

            ( B_SUP ( 'not' a)) = ( I_el Y) & ( 'not' ( B_INF a)) = ( 'not' ( O_el Y)) by A3, A10, Def13, Def14;

            hence thesis by A12, A11, Def13, Th1;

          end;

            case

             A13: (for x be Element of Y holds (a . x) = TRUE ) & for x be Element of Y holds (a . x) = FALSE ;

            let x be Element of Y;

            (a . x) = TRUE by A13;

            hence thesis by A13;

          end;

        end;

        hence thesis;

      end;

      now

        assume that

         A14: not (for x be Element of Y holds (a . x) = TRUE ) and

         A15: not (for x be Element of Y holds (a . x) = FALSE );

        ( 'not' ( B_INF a)) = ( 'not' ( O_el Y)) by A14, Def13;

        then

         A16: ( 'not' ( B_INF a)) = ( I_el Y) by Th1;

        ( 'not' ( B_SUP a)) = ( 'not' ( I_el Y)) & ( B_INF ( 'not' a)) = ( O_el Y) by A1, A15, Def13, Def14;

        hence thesis by A3, A14, A16, Def14, Th1;

      end;

      hence thesis by A5;

    end;

    theorem :: BVFUNC_1:20

    ( B_INF ( O_el Y)) = ( O_el Y) & ( B_INF ( I_el Y)) = ( I_el Y) & ( B_SUP ( O_el Y)) = ( O_el Y) & ( B_SUP ( I_el Y)) = ( I_el Y)

    proof

      

       A1: not (for x be Element of Y holds (( O_el Y) . x) = TRUE )

      proof

        now

          assume for x be Element of Y holds (( O_el Y) . x) = TRUE ;

          let x be Element of Y;

          (( O_el Y) . x) = FALSE by Def10;

          hence thesis;

        end;

        hence thesis;

      end;

      

       A2: not (for x be Element of Y holds (( I_el Y) . x) = FALSE )

      proof

        now

          assume

           A3: for x be Element of Y holds (( I_el Y) . x) = FALSE ;

          let x be Element of Y;

          (( I_el Y) . x) = FALSE by A3;

          hence thesis by Def11;

        end;

        hence thesis;

      end;

      (for x be Element of Y holds (( O_el Y) . x) = FALSE ) & for x be Element of Y holds (( I_el Y) . x) = TRUE by Def10, Def11;

      hence thesis by A1, A2, Def13, Def14;

    end;

    registration

      let Y;

      cluster ( O_el Y) -> constant;

      coherence

      proof

        for n1,n2 be object st n1 in ( dom ( O_el Y)) & n2 in ( dom ( O_el Y)) holds (( O_el Y) . n1) = (( O_el Y) . n2)

        proof

          let n1,n2 be object;

          assume n1 in ( dom ( O_el Y)) & n2 in ( dom ( O_el Y));

          then

          reconsider n1, n2 as Element of Y by PARTFUN1:def 2;

          (( O_el Y) . n2) = FALSE & (( O_el Y) . n1) = (( O_el Y) . n1) by Def10;

          hence thesis by Def10;

        end;

        hence thesis by FUNCT_1:def 10;

      end;

    end

    registration

      let Y;

      cluster ( I_el Y) -> constant;

      coherence

      proof

        thus ( I_el Y) is constant

        proof

          for n1,n2 be object st n1 in ( dom ( I_el Y)) & n2 in ( dom ( I_el Y)) holds (( I_el Y) . n1) = (( I_el Y) . n2)

          proof

            let n1,n2 be object;

            assume n1 in ( dom ( I_el Y)) & n2 in ( dom ( I_el Y));

            then

            reconsider n1, n2 as Element of Y by PARTFUN1:def 2;

            (( I_el Y) . n2) = TRUE & (( I_el Y) . n1) = (( I_el Y) . n1) by Def11;

            hence thesis by Def11;

          end;

          hence thesis by FUNCT_1:def 10;

        end;

      end;

    end

    theorem :: BVFUNC_1:21

    

     Th20: for a be constant Function of Y, BOOLEAN holds a = ( O_el Y) or a = ( I_el Y)

    proof

      let a be constant Function of Y, BOOLEAN ;

      

       A1: (for n1,n2 be set st n1 in Y & n2 in Y holds (a . n1) = (a . n2)) implies (for x be Element of Y holds (a . x) = TRUE ) or for x be Element of Y holds (a . x) = FALSE

      proof

        assume

         A2: for n1,n2 be set st n1 in Y & n2 in Y holds (a . n1) = (a . n2);

        now

          assume that

           A3: not (for x be Element of Y holds (a . x) = TRUE ) and

           A4: not (for x be Element of Y holds (a . x) = FALSE );

          consider x1 be Element of Y such that

           A5: (a . x1) <> TRUE by A3;

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

          hence contradiction by A2, A4;

        end;

        hence thesis;

      end;

      ( dom a) = Y by PARTFUN1:def 2;

      hence thesis by A1, Def10, Def11, FUNCT_1:def 10;

    end;

    theorem :: BVFUNC_1:22

    

     Th21: for d be constant Function of Y, BOOLEAN holds ( B_INF d) = d & ( B_SUP d) = d

    proof

      let d be constant Function of Y, BOOLEAN ;

       A1:

      now

        assume

         A2: (for x be Element of Y holds (d . x) = TRUE ) or for x be Element of Y holds (d . x) = FALSE ;

        now

          per cases by A2;

            case

             A3: (for x be Element of Y holds (d . x) = TRUE ) & not (for x be Element of Y holds (d . x) = FALSE );

            then d = ( I_el Y) by Def11;

            hence thesis by A3, Def13, Def14;

          end;

            case

             A4: (for x be Element of Y holds (d . x) = FALSE ) & not (for x be Element of Y holds (d . x) = TRUE );

            then d = ( O_el Y) by Def10;

            hence thesis by A4, Def13, Def14;

          end;

            case

             A5: (for x be Element of Y holds (d . x) = TRUE ) & for x be Element of Y holds (d . x) = FALSE ;

            let x be Element of Y;

            (d . x) = TRUE by A5;

            hence thesis by A5;

          end;

        end;

        hence thesis;

      end;

      now

        assume that

         A6: not (for x be Element of Y holds (d . x) = TRUE ) and

         A7: not (for x be Element of Y holds (d . x) = FALSE );

        now

          per cases by Th20;

            case d = ( O_el Y);

            hence thesis by A7, Def10;

          end;

            case d = ( I_el Y);

            hence thesis by A6, Def11;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: BVFUNC_1:23

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

    proof

      let a,b be Function of Y, BOOLEAN ;

       A1:

      now

        assume

         A2: for x be Element of Y holds ((a '&' b) . x) = TRUE ;

        

         A3: for x be Element of Y holds (a . x) = TRUE

        proof

          let x be Element of Y;

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

          then ((a . x) '&' (b . x)) = TRUE by A2;

          hence thesis by XBOOLEAN: 101;

        end;

         not (for x be Element of Y holds (a . x) = FALSE )

        proof

          now

            assume for x be Element of Y holds (a . x) = FALSE ;

            let x be Element of Y;

            (a . x) = TRUE by A3;

            hence thesis;

          end;

          hence thesis;

        end;

        then

         A4: ( B_SUP a) = ( I_el Y) by Def14;

        

         A5: for x be Element of Y holds (b . x) = TRUE

        proof

          let x be Element of Y;

          ((a '&' b) . x) = TRUE by A2;

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

          hence thesis by XBOOLEAN: 101;

        end;

         not (for x be Element of Y holds (b . x) = FALSE )

        proof

          now

            assume for x be Element of Y holds (b . x) = FALSE ;

            let x be Element of Y;

            (b . x) = TRUE by A5;

            hence thesis;

          end;

          hence thesis;

        end;

        then

         A6: (( B_SUP a) 'or' ( B_SUP b)) = (( I_el Y) 'or' ( I_el Y)) by A4, Def14;

        

         A7: not (for x be Element of Y holds ((a 'or' b) . x) = FALSE )

        proof

          now

            assume for x be Element of Y holds ((a 'or' b) . x) = FALSE ;

            let x be Element of Y;

            ((a 'or' b) . x) = ((a . x) 'or' (b . x)) & (a . x) = TRUE by A3, Def4;

            hence thesis;

          end;

          hence thesis;

        end;

        (( B_INF a) '&' ( B_INF b)) = (( B_INF a) '&' ( I_el Y)) by A5, Def13

        .= (( I_el Y) '&' ( I_el Y)) by A3, Def13;

        hence thesis by A2, A7, A6, Def13, Def14;

      end;

       A8:

      now

        assume

         A9: for x be Element of Y holds ((a 'or' b) . x) = FALSE ;

        

         A10: for x be Element of Y holds (a . x) = FALSE

        proof

          let x be Element of Y;

          ((a 'or' b) . x) = FALSE by A9;

          then

           A11: ((a . x) 'or' (b . x)) = FALSE by Def4;

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

          hence thesis by A11;

        end;

        

         A12: not (for x be Element of Y holds ((a '&' b) . x) = TRUE )

        proof

          now

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

            let x be Element of Y;

            ((a '&' b) . x) = ((a . x) '&' (b . x)) & (a . x) = FALSE by A10, MARGREL1:def 20;

            hence thesis;

          end;

          hence thesis;

        end;

        

         A13: for x be Element of Y holds (b . x) = FALSE

        proof

          let x be Element of Y;

          ((a 'or' b) . x) = FALSE by A9;

          then

           A14: ((a . x) 'or' (b . x)) = FALSE by Def4;

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

          hence thesis by A14;

        end;

        then ( B_SUP b) = ( O_el Y) by Def14;

        then

         A15: (( B_SUP a) 'or' ( B_SUP b)) = (( O_el Y) 'or' ( O_el Y)) by A10, Def14;

         not (for x be Element of Y holds (a . x) = TRUE )

        proof

          now

            assume for x be Element of Y holds (a . x) = TRUE ;

            let x be Element of Y;

            (a . x) = FALSE by A10;

            hence thesis;

          end;

          hence thesis;

        end;

        then

         A16: ( B_INF a) = ( O_el Y) by Def13;

         not (for x be Element of Y holds (b . x) = TRUE )

        proof

          now

            assume for x be Element of Y holds (b . x) = TRUE ;

            let x be Element of Y;

            (b . x) = FALSE by A13;

            hence thesis;

          end;

          hence thesis;

        end;

        then (( B_INF a) '&' ( B_INF b)) = (( O_el Y) '&' ( O_el Y)) by A16, Def13;

        hence thesis by A9, A15, A12, Def13, Def14;

      end;

      now

        assume that

         A17: not (for x be Element of Y holds ((a '&' b) . x) = TRUE ) and

         A18: not (for x be Element of Y holds ((a 'or' b) . x) = FALSE );

        (for x be Element of Y holds (a . x) = FALSE ) & (for x be Element of Y holds (b . x) = FALSE ) implies for x be Element of Y holds ((a 'or' b) . x) = FALSE

        proof

          assume that

           A19: for x be Element of Y holds (a . x) = FALSE and

           A20: for x be Element of Y holds (b . x) = FALSE ;

          let x be Element of Y;

          (a . x) = FALSE by A19;

          then ((a . x) 'or' (b . x)) = FALSE by A20;

          hence thesis by Def4;

        end;

        then ( B_SUP a) = ( I_el Y) or ( B_SUP b) = ( I_el Y) by A18, Def14;

        then

         A21: (( B_SUP a) 'or' ( B_SUP b)) = ( I_el Y) by Th9;

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

        proof

          assume that

           A22: for x be Element of Y holds (a . x) = TRUE and

           A23: for x be Element of Y holds (b . x) = TRUE ;

          let x be Element of Y;

          (a . x) = TRUE by A22;

          then ((a . x) '&' (b . x)) = TRUE by A23;

          hence thesis by MARGREL1:def 20;

        end;

        then ( B_INF a) = ( O_el Y) or ( B_INF b) = ( O_el Y) by A17, Def13;

        then (( B_INF a) '&' ( B_INF b)) = ( O_el Y) by Th4;

        hence thesis by A17, A18, A21, Def13, Def14;

      end;

      hence thesis by A1, A8;

    end;

    theorem :: BVFUNC_1:24

    for a be Function of Y, BOOLEAN , d be constant Function of Y, BOOLEAN holds ( B_INF (d 'imp' a)) = (d 'imp' ( B_INF a)) & ( B_INF (a 'imp' d)) = (( B_SUP a) 'imp' d)

    proof

      let a be Function of Y, BOOLEAN ;

      let d be constant Function of Y, BOOLEAN ;

      

       A1: (( I_el Y) 'imp' ( I_el Y)) = ( I_el Y)

      proof

        let x be Element of Y;

        (( I_el Y) . x) = TRUE by Def11;

        then ((( I_el Y) 'imp' ( I_el Y)) . x) = (( 'not' TRUE ) 'or' TRUE ) by Def8;

        hence thesis by Def11;

      end;

      

       A2: (( B_SUP a) 'imp' d) = (( B_SUP a) 'imp' ( B_INF d)) by Th21;

      

       A3: ( B_INF d) = d by Th21;

      

       A4: (( O_el Y) 'imp' ( I_el Y)) = ( I_el Y)

      proof

        let x be Element of Y;

        ((( O_el Y) 'imp' ( I_el Y)) . x) = (( 'not' (( O_el Y) . x)) 'or' (( I_el Y) . x)) & (( I_el Y) . x) = TRUE by Def8, Def11;

        hence thesis;

      end;

      

       A5: (( I_el Y) 'imp' ( O_el Y)) = ( O_el Y)

      proof

        let x be Element of Y;

        (( O_el Y) . x) = FALSE by Def10;

        then

         A6: (( 'not' (( I_el Y) . x)) 'or' (( O_el Y) . x)) = (( 'not' TRUE ) 'or' FALSE ) by Def11;

        ((( I_el Y) 'imp' ( O_el Y)) . x) = (( 'not' (( I_el Y) . x)) 'or' (( O_el Y) . x)) by Def8;

        hence thesis by A6, Def10;

      end;

      

       A7: (( O_el Y) 'imp' ( O_el Y)) = ( I_el Y)

      proof

        let x be Element of Y;

        (( O_el Y) . x) = FALSE by Def10;

        then ((( O_el Y) 'imp' ( O_el Y)) . x) = ( TRUE 'or' FALSE ) by Def8;

        hence thesis by Def11;

      end;

      

       A8: (d 'imp' ( B_INF a)) = (( B_INF d) 'imp' ( B_INF a)) by Th21;

      

       A9: (( B_SUP a) 'imp' d) = (( B_SUP a) 'imp' ( B_SUP d)) by Th21;

       A10:

      now

        assume

         A11: (for x be Element of Y holds (d . x) = TRUE ) or for x be Element of Y holds (d . x) = FALSE ;

        now

          per cases by A11;

            case

             A12: (for x be Element of Y holds (d . x) = TRUE ) & not (for x be Element of Y holds (d . x) = FALSE );

             A13:

            now

              assume

               A14: (for x be Element of Y holds (a . x) = TRUE ) or for x be Element of Y holds (a . x) = FALSE ;

              now

                per cases by A14;

                  case

                   A15: (for x be Element of Y holds (a . x) = TRUE ) & not (for x be Element of Y holds (a . x) = FALSE );

                  

                   A16: for x be Element of Y holds ((a 'imp' d) . x) = TRUE

                  proof

                    let x be Element of Y;

                    (d . x) = TRUE & (a . x) = TRUE by A12, A15;

                    then ((a 'imp' d) . x) = (( 'not' TRUE ) 'or' TRUE ) by Def8;

                    hence thesis;

                  end;

                  

                   A17: for x be Element of Y holds ((d 'imp' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    (d . x) = TRUE & (a . x) = TRUE by A12, A15;

                    then ((d 'imp' a) . x) = (( 'not' TRUE ) 'or' TRUE ) by Def8;

                    hence thesis;

                  end;

                  ( B_INF a) = ( I_el Y) by A15, Def13;

                  then

                   A18: (d 'imp' ( B_INF a)) = ( I_el Y) by A8, A1, A12, Def13;

                  

                   A19: ( B_SUP a) = ( I_el Y) by A15, Def14;

                  ( B_SUP d) = ( I_el Y) by A12, Def14;

                  hence thesis by A9, A1, A17, A16, A19, A18, Def13;

                end;

                  case

                   A20: (for x be Element of Y holds (a . x) = FALSE ) & not (for x be Element of Y holds (a . x) = TRUE );

                  

                   A21: for x be Element of Y holds ((d 'imp' a) . x) = FALSE

                  proof

                    let x be Element of Y;

                    ((d 'imp' a) . x) = (( 'not' (d . x)) 'or' (a . x)) & (d . x) = TRUE by A12, Def8;

                    hence thesis by A20;

                  end;

                   A22:

                  now

                    assume

                     A23: for x be Element of Y holds ((d 'imp' a) . x) = TRUE ;

                    let x be Element of Y;

                    ((d 'imp' a) . x) = TRUE by A23;

                    hence contradiction by A21;

                  end;

                  

                   A24: for x be Element of Y holds ((a 'imp' d) . x) = TRUE

                  proof

                    let x be Element of Y;

                    (d . x) = TRUE & (a . x) = FALSE by A12, A20;

                    then ((a 'imp' d) . x) = (( 'not' FALSE ) 'or' TRUE ) by Def8;

                    hence thesis;

                  end;

                  

                   A25: ( B_SUP a) = ( O_el Y) by A20, Def14;

                  ( B_SUP d) = ( I_el Y) by A12, Def14;

                  then

                   A26: (( B_SUP a) 'imp' d) = ( I_el Y) by A4, A25, Th21;

                  

                   A27: ( B_INF a) = ( O_el Y) by A20, Def13;

                  ( B_INF d) = ( I_el Y) by A12, Def13;

                  hence thesis by A8, A5, A22, A24, A27, A26, Def13;

                end;

                  case

                   A28: (for x be Element of Y holds (a . x) = FALSE ) & for x be Element of Y holds (a . x) = TRUE ;

                  

                   A29: for x be Element of Y holds ((d 'imp' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    ((d 'imp' a) . x) = (( 'not' (d . x)) 'or' (a . x)) & (a . x) = TRUE by A28, Def8;

                    hence thesis;

                  end;

                  

                   A30: ( B_INF d) = ( I_el Y) by A12, Def13;

                  

                   A31: for x be Element of Y holds ((a 'imp' d) . x) = TRUE

                  proof

                    let x be Element of Y;

                    ((a 'imp' d) . x) = (( 'not' (a . x)) 'or' (d . x)) & (d . x) = TRUE by A12, Def8;

                    hence thesis;

                  end;

                  ( B_INF a) = ( I_el Y) & ( B_SUP a) = ( O_el Y) by A28, Def13, Def14;

                  hence thesis by A8, A2, A1, A4, A29, A31, A30, Def13;

                end;

              end;

              hence thesis;

            end;

            now

              

               A32: for x be Element of Y holds ((a 'imp' d) . x) = TRUE

              proof

                let x be Element of Y;

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

                then (( 'not' (a . x)) 'or' (d . x)) = ((( 'not' a) 'or' d) . x) by Def4;

                then

                 A33: (( 'not' (a . x)) 'or' (d . x)) = ((( 'not' a) 'or' ( I_el Y)) . x) by A3, A12, Def13;

                ((a 'imp' d) . x) = (( 'not' (a . x)) 'or' (d . x)) by Def8;

                hence thesis by Th9, Def11, A33;

              end;

              

               A34: ( B_INF d) = ( I_el Y) by A12, Def13;

              assume that

               A35: not (for x be Element of Y holds (a . x) = TRUE ) and

               A36: not (for x be Element of Y holds (a . x) = FALSE );

              

               A37: ( B_INF a) = ( O_el Y) by A35, Def13;

              ( B_SUP a) = ( I_el Y) by A36, Def14;

              then

               A38: (( B_SUP a) 'imp' d) = ( I_el Y) by A1, A34, Th21;

              (d 'imp' a) = a

              proof

                let x be Element of Y;

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

                then (( 'not' (d . x)) 'or' (a . x)) = ((( 'not' d) 'or' a) . x) by Def4;

                then (( 'not' (d . x)) 'or' (a . x)) = ((( 'not' ( I_el Y)) 'or' a) . x) by A3, A12, Def13;

                then

                 A39: (( 'not' (d . x)) 'or' (a . x)) = ((( O_el Y) 'or' a) . x) by Th1;

                ((d 'imp' a) . x) = (( 'not' (d . x)) 'or' (a . x)) by Def8;

                hence thesis by A39, Th8;

              end;

              hence thesis by A8, A5, A12, Def13, A37, A32, A38;

            end;

            hence thesis by A13;

          end;

            case

             A40: (for x be Element of Y holds (d . x) = FALSE ) & not (for x be Element of Y holds (d . x) = TRUE );

             A41:

            now

              assume

               A42: (for x be Element of Y holds (a . x) = TRUE ) or for x be Element of Y holds (a . x) = FALSE ;

              now

                per cases by A42;

                  case

                   A43: (for x be Element of Y holds (a . x) = TRUE ) & not (for x be Element of Y holds (a . x) = FALSE );

                  

                   A44: for x be Element of Y holds ((a 'imp' d) . x) = FALSE

                  proof

                    let x be Element of Y;

                    (d . x) = FALSE & (a . x) = TRUE by A40, A43;

                    then ((a 'imp' d) . x) = (( 'not' TRUE ) 'or' FALSE ) by Def8;

                    hence thesis;

                  end;

                   A45:

                  now

                    assume

                     A46: for x be Element of Y holds ((a 'imp' d) . x) = TRUE ;

                    let x be Element of Y;

                    ((a 'imp' d) . x) = TRUE by A46;

                    hence contradiction by A44;

                  end;

                  

                   A47: for x be Element of Y holds ((d 'imp' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    (d . x) = FALSE & (a . x) = TRUE by A40, A43;

                    then ((d 'imp' a) . x) = (( 'not' FALSE ) 'or' TRUE ) by Def8;

                    hence thesis;

                  end;

                  

                   A48: ( B_SUP a) = ( I_el Y) by A43, Def14;

                  ( B_SUP d) = ( O_el Y) by A40, Def14;

                  then

                   A49: (( B_SUP a) 'imp' d) = ( O_el Y) by A5, A48, Th21;

                  

                   A50: ( B_INF a) = ( I_el Y) by A43, Def13;

                  ( B_INF d) = ( O_el Y) by A40, Def13;

                  hence thesis by A8, A4, A47, A45, A50, A49, Def13;

                end;

                  case

                   A51: (for x be Element of Y holds (a . x) = FALSE ) & not (for x be Element of Y holds (a . x) = TRUE );

                  

                   A52: for x be Element of Y holds ((d 'imp' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    (d . x) = FALSE & (a . x) = FALSE by A40, A51;

                    then ((d 'imp' a) . x) = (( 'not' FALSE ) 'or' FALSE ) by Def8;

                    hence thesis;

                  end;

                  

                   A53: ( B_INF d) = ( O_el Y) by A40, Def13;

                  

                   A54: for x be Element of Y holds ((a 'imp' d) . x) = TRUE

                  proof

                    let x be Element of Y;

                    ((a 'imp' d) . x) = (( 'not' (a . x)) 'or' (d . x)) & (a . x) = FALSE by A51, Def8;

                    hence thesis;

                  end;

                  ( B_INF a) = ( O_el Y) & ( B_SUP a) = ( O_el Y) by A51, Def13, Def14;

                  hence thesis by A8, A2, A7, A52, A54, A53, Def13;

                end;

                  case

                   A55: (for x be Element of Y holds (a . x) = FALSE ) & for x be Element of Y holds (a . x) = TRUE ;

                  

                   A56: for x be Element of Y holds ((a 'imp' d) . x) = TRUE

                  proof

                    let x be Element of Y;

                    ((a 'imp' d) . x) = (( 'not' (a . x)) 'or' (d . x)) & (a . x) = FALSE by A55, Def8;

                    hence thesis;

                  end;

                  

                   A57: for x be Element of Y holds ((d 'imp' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    ((d 'imp' a) . x) = (( 'not' (d . x)) 'or' (a . x)) & (a . x) = TRUE by A55, Def8;

                    hence thesis;

                  end;

                  

                   A58: ( B_INF d) = ( O_el Y) by A40, Def13;

                  ( B_SUP a) = ( O_el Y) by A55, Def14;

                  then

                   A59: (( B_SUP a) 'imp' d) = ( I_el Y) by A7, A58, Th21;

                  ( B_INF a) = ( I_el Y) by A55, Def13;

                  hence thesis by A8, A4, A57, A56, A58, A59, Def13;

                end;

              end;

              hence thesis;

            end;

            now

              

               A60: ( B_INF d) = ( O_el Y) by A40, Def13;

              

               A61: for x be Element of Y holds ((d 'imp' a) . x) = TRUE

              proof

                let x be Element of Y;

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

                then (( 'not' (d . x)) 'or' (a . x)) = ((( 'not' ( O_el Y)) 'or' a) . x) by A3, A60, Def4;

                then (( 'not' (d . x)) 'or' (a . x)) = ((( I_el Y) 'or' a) . x) by Th1;

                then (( 'not' (d . x)) 'or' (a . x)) = TRUE by Def11, Th9;

                hence thesis by Def8;

              end;

              (a 'imp' d) = ( 'not' a)

              proof

                let x be Element of Y;

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

                then (( 'not' (a . x)) 'or' (d . x)) = ((( 'not' a) 'or' d) . x) by Def4;

                then (( 'not' (a . x)) 'or' (d . x)) = (( 'not' a) . x) by A3, A60, Th8;

                hence thesis by Def8;

              end;

              then

               A62: ( B_INF (a 'imp' d)) = ( 'not' ( B_SUP a)) by Th18;

              assume ( not (for x be Element of Y holds (a . x) = TRUE )) & not (for x be Element of Y holds (a . x) = FALSE );

              then

               A63: ( B_INF a) = ( O_el Y) & ( B_SUP a) = ( I_el Y) by Def13, Def14;

              ( B_INF d) = ( O_el Y) by A40, Def13;

              hence thesis by A8, A2, A5, A7, A61, A62, A63, Def13, Th1;

            end;

            hence thesis by A41;

          end;

            case

             A64: (for x be Element of Y holds (d . x) = TRUE ) & for x be Element of Y holds (d . x) = FALSE ;

            let x be Element of Y;

            (d . x) = FALSE by A64;

            hence thesis by A64;

          end;

        end;

        hence thesis;

      end;

      now

        assume that

         A65: not (for x be Element of Y holds (d . x) = TRUE ) and

         A66: not (for x be Element of Y holds (d . x) = FALSE );

        now

          per cases by Th20;

            case d = ( O_el Y);

            hence thesis by A66, Def10;

          end;

            case d = ( I_el Y);

            hence thesis by A65, Def11;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A10;

    end;

    theorem :: BVFUNC_1:25

    for a be Function of Y, BOOLEAN , d be constant Function of Y, BOOLEAN holds ( B_INF (d 'or' a)) = (d 'or' ( B_INF a)) & ( B_SUP (d '&' a)) = (d '&' ( B_SUP a)) & ( B_SUP (a '&' d)) = (( B_SUP a) '&' d)

    proof

      let a be Function of Y, BOOLEAN ;

      let d be constant Function of Y, BOOLEAN ;

      

       A1: (d 'or' ( B_INF a)) = (( B_INF d) 'or' ( B_INF a)) by Th21;

      

       A2: (d '&' ( B_SUP a)) = (( B_SUP d) '&' ( B_SUP a)) by Th21;

      

       A3: ( B_INF d) = d by Th21;

       A4:

      now

        assume

         A5: (for x be Element of Y holds (d . x) = TRUE ) or for x be Element of Y holds (d . x) = FALSE ;

        now

          per cases by A5;

            case

             A6: (for x be Element of Y holds (d . x) = TRUE ) & not (for x be Element of Y holds (d . x) = FALSE );

             A7:

            now

              assume

               A8: (for x be Element of Y holds (a . x) = TRUE ) or for x be Element of Y holds (a . x) = FALSE ;

              now

                per cases by A8;

                  case

                   A9: (for x be Element of Y holds (a . x) = TRUE ) & not (for x be Element of Y holds (a . x) = FALSE );

                  

                   A10: for x be Element of Y holds ((d '&' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    (d . x) = TRUE & (a . x) = TRUE by A6, A9;

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

                    hence thesis;

                  end;

                   A11:

                  now

                    assume

                     A12: for x be Element of Y holds ((d '&' a) . x) = FALSE ;

                    let x be Element of Y;

                    ((d '&' a) . x) = TRUE by A10;

                    hence contradiction by A12;

                  end;

                  

                   A13: for x be Element of Y holds ((d 'or' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    ((d 'or' a) . x) = ((d . x) 'or' (a . x)) & (a . x) = TRUE by A9, Def4;

                    hence thesis;

                  end;

                  

                   A14: ( B_INF a) = ( I_el Y) & ( B_SUP a) = ( I_el Y) by A9, Def13, Def14;

                  ( B_INF d) = ( I_el Y) & ( B_SUP d) = ( I_el Y) by A6, Def13, Def14;

                  hence thesis by A1, A2, A13, A11, A14, Def13, Def14;

                end;

                  case

                   A15: (for x be Element of Y holds (a . x) = FALSE ) & not (for x be Element of Y holds (a . x) = TRUE );

                  

                   A16: for x be Element of Y holds ((d '&' a) . x) = FALSE

                  proof

                    let x be Element of Y;

                    ((d '&' a) . x) = ((d . x) '&' (a . x)) & (a . x) = FALSE by A15, MARGREL1:def 20;

                    hence thesis;

                  end;

                  

                   A17: for x be Element of Y holds ((d 'or' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    ((d 'or' a) . x) = ((d . x) 'or' (a . x)) & (d . x) = TRUE by A6, Def4;

                    hence thesis;

                  end;

                  ( B_SUP a) = ( O_el Y) by A15, Def14;

                  then

                   A18: (d '&' ( B_SUP a)) = ( O_el Y) by Th4;

                  

                   A19: ( B_INF a) = ( O_el Y) by A15, Def13;

                  ( B_INF d) = ( I_el Y) by A6, Def13;

                  then (d 'or' ( B_INF a)) = ( I_el Y) by A1, A19, Th8;

                  hence thesis by A17, A16, A18, Def13, Def14;

                end;

                  case

                   A20: (for x be Element of Y holds (a . x) = FALSE ) & for x be Element of Y holds (a . x) = TRUE ;

                  

                   A21: for x be Element of Y holds ((d '&' a) . x) = FALSE

                  proof

                    let x be Element of Y;

                    (d . x) = TRUE & (a . x) = FALSE by A6, A20;

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

                    hence thesis;

                  end;

                  

                   A22: for x be Element of Y holds ((d 'or' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    (d . x) = TRUE & (a . x) = FALSE by A6, A20;

                    then ((d 'or' a) . x) = ( TRUE 'or' FALSE ) by Def4;

                    hence thesis;

                  end;

                  ( B_SUP a) = ( O_el Y) by A20, Def14;

                  then

                   A23: (d '&' ( B_SUP a)) = ( O_el Y) by Th4;

                  ( B_INF d) = ( I_el Y) by A6, Def13;

                  then (d 'or' ( B_INF a)) = ( I_el Y) by A1, Th9;

                  hence thesis by A22, A21, A23, Def13, Def14;

                end;

              end;

              hence thesis;

            end;

            now

              assume that

               A24: not (for x be Element of Y holds (a . x) = TRUE ) and not (for x be Element of Y holds (a . x) = FALSE );

              

               A25: ( B_INF a) = ( O_el Y) by A24, Def13;

              ( B_INF d) = ( I_el Y) by A6, Def13;

              then

               A26: (d 'or' ( B_INF a)) = ( I_el Y) by A1, A25, Th8;

              

               A27: d = ( I_el Y) by A3, A6, Def13;

              

               A28: for x be Element of Y holds ((d 'or' a) . x) = TRUE by A27, Th9, Def11;

              

               A29: (d '&' a) = a

              proof

                let x be Element of Y;

                ((d '&' a) . x) = ((( I_el Y) . x) '&' (a . x)) by A27, MARGREL1:def 20;

                then ((d '&' a) . x) = ( TRUE '&' (a . x)) by Def11;

                hence thesis;

              end;

              ( B_SUP d) = ( I_el Y) by A6, Def14;

              hence thesis by A2, A28, A29, A26, Def13, Th5;

            end;

            hence thesis by A7;

          end;

            case

             A30: (for x be Element of Y holds (d . x) = FALSE ) & not (for x be Element of Y holds (d . x) = TRUE );

             A31:

            now

              assume

               A32: (for x be Element of Y holds (a . x) = TRUE ) or for x be Element of Y holds (a . x) = FALSE ;

              now

                per cases by A32;

                  case

                   A33: (for x be Element of Y holds (a . x) = TRUE ) & not (for x be Element of Y holds (a . x) = FALSE );

                  

                   A34: for x be Element of Y holds ((d 'or' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    ((d 'or' a) . x) = ((d . x) 'or' (a . x)) & (d . x) = FALSE by A30, Def4;

                    hence thesis by A33;

                  end;

                  ( B_SUP d) = ( O_el Y) by A30, Def14;

                  then

                   A35: (d '&' ( B_SUP a)) = ( O_el Y) by A2, Th4;

                  

                   A36: for x be Element of Y holds ((d '&' a) . x) = FALSE

                  proof

                    let x be Element of Y;

                    ((d '&' a) . x) = ((d . x) '&' (a . x)) & (d . x) = FALSE by A30, MARGREL1:def 20;

                    hence thesis;

                  end;

                  

                   A37: ( B_INF a) = ( I_el Y) by A33, Def13;

                  ( B_INF d) = ( O_el Y) by A30, Def13;

                  then (d 'or' ( B_INF a)) = ( I_el Y) by A1, A37, Th8;

                  hence thesis by A34, A36, A35, Def13, Def14;

                end;

                  case

                   A38: (for x be Element of Y holds (a . x) = FALSE ) & not (for x be Element of Y holds (a . x) = TRUE );

                  

                   A39: for x be Element of Y holds ((d 'or' a) . x) = FALSE

                  proof

                    let x be Element of Y;

                    (d . x) = FALSE & (a . x) = FALSE by A30, A38;

                    then ((d 'or' a) . x) = ( FALSE 'or' FALSE ) by Def4;

                    hence thesis;

                  end;

                   A40:

                  now

                    assume

                     A41: for x be Element of Y holds ((d 'or' a) . x) = TRUE ;

                    let x be Element of Y;

                    ((d 'or' a) . x) = FALSE by A39;

                    hence contradiction by A41;

                  end;

                  ( B_SUP d) = ( O_el Y) by A30, Def14;

                  then

                   A42: (d '&' ( B_SUP a)) = ( O_el Y) by A2, Th4;

                  

                   A43: for x be Element of Y holds ((d '&' a) . x) = FALSE

                  proof

                    let x be Element of Y;

                    (d . x) = FALSE & (a . x) = FALSE by A30, A38;

                    then ((d '&' a) . x) = ( FALSE '&' FALSE ) by MARGREL1:def 20;

                    hence thesis;

                  end;

                  

                   A44: ( B_INF a) = ( O_el Y) by A38, Def13;

                  ( B_INF d) = ( O_el Y) by A30, Def13;

                  hence thesis by A1, A40, A43, A44, A42, Def13, Def14;

                end;

                  case

                   A45: (for x be Element of Y holds (a . x) = FALSE ) & for x be Element of Y holds (a . x) = TRUE ;

                  

                   A46: for x be Element of Y holds ((d 'or' a) . x) = TRUE

                  proof

                    let x be Element of Y;

                    (d . x) = FALSE & (a . x) = TRUE by A30, A45;

                    then ((d 'or' a) . x) = ( FALSE 'or' TRUE ) by Def4;

                    hence thesis;

                  end;

                  ( B_SUP d) = ( O_el Y) by A30, Def14;

                  then

                   A47: (d '&' ( B_SUP a)) = ( O_el Y) by A2, Th4;

                  

                   A48: for x be Element of Y holds ((d '&' a) . x) = FALSE

                  proof

                    let x be Element of Y;

                    (d . x) = FALSE & (a . x) = TRUE by A30, A45;

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

                    hence thesis;

                  end;

                  

                   A49: ( B_INF a) = ( I_el Y) by A45, Def13;

                  ( B_INF d) = ( O_el Y) by A30, Def13;

                  then (d 'or' ( B_INF a)) = ( I_el Y) by A1, A49, Th8;

                  hence thesis by A46, A48, A47, Def13, Def14;

                end;

              end;

              hence thesis;

            end;

            now

              for x be Element of Y holds ((d '&' a) . x) = FALSE

              proof

                let x be Element of Y;

                ((d '&' a) . x) = ((( O_el Y) '&' a) . x) by A3, A30, Def13;

                hence thesis by Def10, Th4;

              end;

              then

               A50: ( B_SUP (d '&' a)) = ( O_el Y) by Def14;

              assume that

               A51: not (for x be Element of Y holds (a . x) = TRUE ) and not (for x be Element of Y holds (a . x) = FALSE );

              ( B_INF d) = ( O_el Y) by A30, Def13;

              then

               A52: (d 'or' ( B_INF a)) = (( O_el Y) 'or' ( O_el Y)) by A1, A51, Def13;

              

               A53: (d 'or' a) = a

              proof

                let x be Element of Y;

                ((d 'or' a) . x) = ((d . x) 'or' (a . x)) by Def4;

                then ((d 'or' a) . x) = ( FALSE 'or' (a . x)) by A30;

                hence thesis;

              end;

              ( B_SUP d) = ( O_el Y) by A30, Def14;

              hence thesis by A2, A51, A53, A50, A52, Def13, Th4;

            end;

            hence thesis by A31;

          end;

            case

             A54: (for x be Element of Y holds (d . x) = TRUE ) & for x be Element of Y holds (d . x) = FALSE ;

            let x be Element of Y;

            (d . x) = FALSE by A54;

            hence thesis by A54;

          end;

        end;

        hence thesis;

      end;

      now

        assume that

         A55: not (for x be Element of Y holds (d . x) = TRUE ) and

         A56: not (for x be Element of Y holds (d . x) = FALSE );

        now

          per cases by Th20;

            case d = ( O_el Y);

            hence thesis by A56, Def10;

          end;

            case d = ( I_el Y);

            hence thesis by A55, Def11;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: BVFUNC_1:26

    for a be Function of Y, BOOLEAN , x be Element of Y holds (( B_INF a) . x) <= (a . x)

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        assume not (for x be Element of Y holds (a . x) = TRUE );

        then ( B_INF a) = ( O_el Y) by Def13;

        then (( B_INF a) . x) = FALSE by Def10;

        then ((( B_INF a) . x) => (a . x)) = TRUE ;

        hence thesis;

      end;

      now

        assume for x be Element of Y holds (a . x) = TRUE ;

        then (a . x) = TRUE ;

        then ((( B_INF a) . x) => (a . x)) = TRUE ;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: BVFUNC_1:27

    for a be Function of Y, BOOLEAN , x be Element of Y holds (a . x) <= (( B_SUP a) . x)

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        assume not (for x be Element of Y holds (a . x) = FALSE );

        then ( B_SUP a) = ( I_el Y) by Def14;

        then (( B_SUP a) . x) = TRUE by Def11;

        then ((a . x) => (( B_SUP a) . x)) = TRUE ;

        hence thesis;

      end;

      now

        assume for x be Element of Y holds (a . x) = FALSE ;

        then (a . x) = FALSE ;

        then ((a . x) => (( B_SUP a) . x)) = TRUE ;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    begin

    definition

      let Y;

      let a be Function of Y, BOOLEAN , PA be a_partition of Y;

      :: BVFUNC_1:def15

      pred a is_dependent_of PA means for F be set st F in PA holds for x1,x2 be set st x1 in F & x2 in F holds (a . x1) = (a . x2);

    end

    theorem :: BVFUNC_1:28

    for a be Function of Y, BOOLEAN holds a is_dependent_of ( %I Y)

    proof

      let a be Function of Y, BOOLEAN ;

      for F be set st F in ( %I Y) holds for x1,x2 be set st x1 in F & x2 in F holds (a . x1) = (a . x2)

      proof

        let F be set;

        assume F in ( %I Y);

        then F in { B : ex z be set st B = {z} & z in Y } by PARTIT1: 31;

        then ex B st F = B & ex z be set st B = {z} & z in Y;

        then

        consider z be set such that

         A1: F = {z} and z in Y;

        let x1,x2 be set;

        assume that

         A2: x1 in F and

         A3: x2 in F;

        x1 = z by A1, A2, TARSKI:def 1;

        hence thesis by A1, A3, TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_1:29

    for a be constant Function of Y, BOOLEAN holds a is_dependent_of ( %O Y)

    proof

      let a be constant Function of Y, BOOLEAN ;

      for F be set st F in ( %O Y) holds for x1,x2 be set st x1 in F & x2 in F holds (a . x1) = (a . x2)

      proof

        let F be set;

        for x1,x2 be Element of Y holds (a . x1) = (a . x2)

        proof

          let x1,x2 be Element of Y;

          per cases by Th20;

            suppose

             A1: a = ( O_el Y);

            then (a . x1) = FALSE by Def10;

            hence thesis by A1, Def10;

          end;

            suppose

             A2: a = ( I_el Y);

            then (a . x1) = TRUE by Def11;

            hence thesis by A2, Def11;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let Y;

      let PA be a_partition of Y;

      :: original: Element

      redefine

      mode Element of PA -> Subset of Y ;

      coherence

      proof

        let x be Element of PA;

        thus thesis;

      end;

    end

    definition

      let Y;

      let x be Element of Y;

      let PA be a_partition of Y;

      :: original: EqClass

      redefine

      func EqClass (x,PA) -> Element of PA ;

      coherence by EQREL_1:def 6;

    end

    definition

      let Y;

      let a be Function of Y, BOOLEAN , PA be a_partition of Y;

      :: BVFUNC_1:def16

      func B_INF (a,PA) -> Function of Y, BOOLEAN means

      : Def16: for y be Element of Y holds ((for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ) implies (it . y) = TRUE ) & ( not (for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ) implies (it . y) = FALSE );

      existence

      proof

        defpred P[ Element of Y, set] means ((for x be Element of Y st x in ( EqClass ($1,PA)) holds (a . x) = TRUE ) implies $2 = TRUE ) & ( not (for x be Element of Y st x in ( EqClass ($1,PA)) holds (a . x) = TRUE ) implies $2 = FALSE );

        

         A1: for e be Element of Y holds ex u be Element of BOOLEAN st P[e, u]

        proof

          let e be Element of Y;

          per cases ;

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

            hence thesis;

          end;

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

            hence thesis;

          end;

        end;

        consider f be Function of Y, BOOLEAN such that

         A2: for e be Element of Y holds P[e, (f . e)] from FUNCT_2:sch 3( A1);

        reconsider f as Function of Y, BOOLEAN ;

        reconsider f as Function of Y, BOOLEAN ;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let A1,A2 be Function of Y, BOOLEAN such that

         A3: for y be Element of Y holds ((for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ) implies (A1 . y) = TRUE ) & ( not (for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ) implies (A1 . y) = FALSE ) and

         A4: for y be Element of Y holds ((for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ) implies (A2 . y) = TRUE ) & ( not (for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ) implies (A2 . y) = FALSE );

        let y be Element of Y;

         A5:

        now

          assume

           A6: not (for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE );

          then (A2 . y) = FALSE by A4;

          hence thesis by A3, A6;

        end;

        now

          assume

           A7: for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ;

          then (A2 . y) = TRUE by A4;

          hence thesis by A3, A7;

        end;

        hence thesis by A5;

      end;

    end

    definition

      let Y;

      let a be Function of Y, BOOLEAN , PA be a_partition of Y;

      :: BVFUNC_1:def17

      func B_SUP (a,PA) -> Function of Y, BOOLEAN means

      : Def17: for y be Element of Y holds ((ex x be Element of Y st x in ( EqClass (y,PA)) & (a . x) = TRUE ) implies (it . y) = TRUE ) & ( not (ex x be Element of Y st x in ( EqClass (y,PA)) & (a . x) = TRUE ) implies (it . y) = FALSE );

      existence

      proof

        defpred P[ Element of Y, set] means ((ex x be Element of Y st x in ( EqClass ($1,PA)) & (a . x) = TRUE ) implies $2 = TRUE ) & ( not (ex x be Element of Y st x in ( EqClass ($1,PA)) & (a . x) = TRUE ) implies $2 = FALSE );

        

         A1: for e be Element of Y holds ex u be Element of BOOLEAN st P[e, u]

        proof

          let e be Element of Y;

          per cases ;

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

            hence thesis;

          end;

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

            hence thesis;

          end;

        end;

        consider f be Function of Y, BOOLEAN such that

         A2: for e be Element of Y holds P[e, (f . e)] from FUNCT_2:sch 3( A1);

        reconsider f as Function of Y, BOOLEAN ;

        reconsider f as Function of Y, BOOLEAN ;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let A1,A2 be Function of Y, BOOLEAN such that

         A3: for y be Element of Y holds ((ex x be Element of Y st x in ( EqClass (y,PA)) & (a . x) = TRUE ) implies (A1 . y) = TRUE ) & ( not (ex x be Element of Y st x in ( EqClass (y,PA)) & (a . x) = TRUE ) implies (A1 . y) = FALSE ) and

         A4: for y be Element of Y holds ((ex x be Element of Y st x in ( EqClass (y,PA)) & (a . x) = TRUE ) implies (A2 . y) = TRUE ) & ( not (ex x be Element of Y st x in ( EqClass (y,PA)) & (a . x) = TRUE ) implies (A2 . y) = FALSE );

        let y be Element of Y;

         A5:

        now

          assume

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

          then (A2 . y) = FALSE by A4;

          hence thesis by A3, A6;

        end;

        now

          assume

           A7: ex x be Element of Y st x in ( EqClass (y,PA)) & (a . x) = TRUE ;

          then (A2 . y) = TRUE by A4;

          hence thesis by A3, A7;

        end;

        hence thesis by A5;

      end;

    end

    theorem :: BVFUNC_1:30

    for a be Function of Y, BOOLEAN , PA be a_partition of Y holds ( B_INF (a,PA)) is_dependent_of PA

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

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

      proof

        let F be set;

        assume

         A1: F in PA;

        let x1,x2 be set;

        assume that

         A2: x1 in F and

         A3: x2 in F;

        reconsider x1 as Element of Y by A1, A2;

        

         A4: ( EqClass (x1,PA)) = F or ( EqClass (x1,PA)) misses F by A1, EQREL_1:def 4;

        reconsider x2 as Element of Y by A1, A3;

        

         A5: x1 in ( EqClass (x1,PA)) & ( EqClass (x2,PA)) = F by A1, A3, EQREL_1:def 6;

        per cases ;

          suppose

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

          then (( B_INF (a,PA)) . x1) = TRUE by Def16;

          hence thesis by A2, A4, A5, A6, Def16, XBOOLE_0: 3;

        end;

          suppose

           A7: not (for x be Element of Y st x in ( EqClass (x1,PA)) holds (a . x) = TRUE );

          then (( B_INF (a,PA)) . x1) = FALSE by Def16;

          hence thesis by A2, A4, A5, A7, Def16, XBOOLE_0: 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_1:31

    for a be Function of Y, BOOLEAN , PA be a_partition of Y holds ( B_SUP (a,PA)) is_dependent_of PA

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

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

      proof

        let F be set;

        assume

         A1: F in PA;

        let x1,x2 be set;

        assume

         A2: x1 in F & x2 in F;

        then

        reconsider x1, x2 as Element of Y by A1;

        

         A3: x1 in ( EqClass (x1,PA)) by EQREL_1:def 6;

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

        then

         A4: ( EqClass (x2,PA)) = ( EqClass (x1,PA)) 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,PA)) & (a . x) = TRUE ;

          then (( B_SUP (a,PA)) . x1) = TRUE by Def17;

          hence thesis by A4, A5, Def17;

        end;

          suppose

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

          then (( B_SUP (a,PA)) . x1) = FALSE by Def17;

          hence thesis by A4, A6, Def17;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_1:32

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

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      (( B_INF (a,PA)) 'imp' a) = ( I_el Y)

      proof

        let y be Element of Y;

        per cases ;

          suppose

           A1: for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ;

          

           A2: (a . y) = TRUE by A1, EQREL_1:def 6;

          ( 'not' (( B_INF (a,PA)) . y)) = (( 'not' ( B_INF (a,PA))) . y) by MARGREL1:def 19;

          

          then (( 'not' (( B_INF (a,PA)) . y)) 'or' (a . y)) = ((( 'not' ( B_INF (a,PA))) . y) 'or' (( I_el Y) . y)) by A2, Def11

          .= ((( 'not' ( B_INF (a,PA))) 'or' ( I_el Y)) . y) by Def4

          .= (( I_el Y) . y) by Th9;

          hence thesis by Def8;

        end;

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

          then (( B_INF (a,PA)) . y) = FALSE by Def16;

          

          then (( 'not' (( B_INF (a,PA)) . y)) 'or' (a . y)) = ((( I_el Y) . y) 'or' (a . y)) by Def11

          .= ((( I_el Y) 'or' a) . y) by Def4

          .= (( I_el Y) . y) by Th9;

          hence thesis by Def8;

        end;

      end;

      hence thesis by Th15;

    end;

    theorem :: BVFUNC_1:33

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

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      (a 'imp' ( B_SUP (a,PA))) = ( I_el Y)

      proof

        let y be Element of Y;

        per cases ;

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

          then (( B_SUP (a,PA)) . y) = TRUE by Def17;

          then (( B_SUP (a,PA)) . y) = (( I_el Y) . y) by Def11;

          

          then (( 'not' (a . y)) 'or' (( B_SUP (a,PA)) . y)) = ((( 'not' a) . y) 'or' (( I_el Y) . y)) by MARGREL1:def 19

          .= ((( 'not' a) 'or' ( I_el Y)) . y) by Def4

          .= (( I_el Y) . y) by Th9;

          hence thesis by Def8;

        end;

          suppose

           A1: not (ex x be Element of Y st x in ( EqClass (y,PA)) & (a . x) = TRUE );

          (a . y) <> TRUE by A1, EQREL_1:def 6;

          then (a . y) = FALSE by XBOOLEAN:def 3;

          

          then (( 'not' (a . y)) 'or' (( B_SUP (a,PA)) . y)) = ((( I_el Y) . y) 'or' (( B_SUP (a,PA)) . y)) by Def11

          .= ((( I_el Y) 'or' ( B_SUP (a,PA))) . y) by Def4

          .= (( I_el Y) . y) by Th9;

          hence thesis by Def8;

        end;

      end;

      hence thesis by Th15;

    end;

    theorem :: BVFUNC_1:34

    for a be Function of Y, BOOLEAN , PA be a_partition of Y holds ( 'not' ( B_INF (a,PA))) = ( B_SUP (( 'not' a),PA))

    proof

      let a be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      let y be Element of Y;

       A1:

      now

        assume that

         A2: for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE and

         A3: ex x be Element of Y st x in ( EqClass (y,PA)) & (( 'not' a) . x) = TRUE ;

        consider x1 be Element of Y such that

         A4: x1 in ( EqClass (y,PA)) and

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

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

        hence contradiction by A2, A4;

      end;

       A6:

      now

        assume that

         A7: not (for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ) and

         A8: not (ex x be Element of Y st x in ( EqClass (y,PA)) & (( 'not' a) . x) = TRUE );

        consider x1 be Element of Y such that

         A9: x1 in ( EqClass (y,PA)) and

         A10: (a . x1) <> TRUE by A7;

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

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

        hence contradiction by A8, A9;

      end;

       A11:

      now

        assume that

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

         A13: ex x be Element of Y st x in ( EqClass (y,PA)) & (( 'not' a) . x) = TRUE ;

        (( B_INF (a,PA)) . y) = FALSE by A12, Def16;

        then (( 'not' ( B_INF (a,PA))) . y) = ( 'not' FALSE ) by MARGREL1:def 19;

        hence thesis by A13, Def17;

      end;

      now

        assume that

         A14: for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE and

         A15: not (ex x be Element of Y st x in ( EqClass (y,PA)) & (( 'not' a) . x) = TRUE );

        (( B_INF (a,PA)) . y) = TRUE by A14, Def16;

        then (( 'not' ( B_INF (a,PA))) . y) = ( 'not' TRUE ) by MARGREL1:def 19;

        hence thesis by A15, Def17;

      end;

      hence thesis by A1, A11, A6;

    end;

    theorem :: BVFUNC_1:35

    for a be Function of Y, BOOLEAN holds ( B_INF (a,( %O Y))) = ( B_INF a)

    proof

      let a be Function of Y, BOOLEAN ;

      let y be Element of Y;

       A1:

      now

        ( EqClass (y,( %O Y))) in ( %O Y);

        then ( EqClass (y,( %O Y))) in {Y} by PARTIT1:def 8;

        then

         A2: ( EqClass (y,( %O Y))) = Y by TARSKI:def 1;

        assume ( not (for x be Element of Y holds (a . x) = TRUE )) & for x be Element of Y st x in ( EqClass (y,( %O Y))) holds (a . x) = TRUE ;

        hence contradiction by A2;

      end;

       A3:

      now

        assume that

         A4: not (for x be Element of Y holds (a . x) = TRUE ) and

         A5: not (for x be Element of Y st x in ( EqClass (y,( %O Y))) holds (a . x) = TRUE );

        ( B_INF a) = ( O_el Y) by A4, Def13;

        then (( B_INF a) . y) = FALSE by Def10;

        hence thesis by A5, Def16;

      end;

      now

        assume that

         A6: for x be Element of Y holds (a . x) = TRUE and

         A7: for x be Element of Y st x in ( EqClass (y,( %O Y))) holds (a . x) = TRUE ;

        ( B_INF a) = ( I_el Y) by A6, Def13;

        then (( B_INF a) . y) = TRUE by Def11;

        hence thesis by A7, Def16;

      end;

      hence thesis by A1, A3;

    end;

    theorem :: BVFUNC_1:36

    for a be Function of Y, BOOLEAN holds ( B_SUP (a,( %O Y))) = ( B_SUP a)

    proof

      let a be Function of Y, BOOLEAN ;

      let y be Element of Y;

      ( EqClass (y,( %O Y))) in ( %O Y);

      then ( EqClass (y,( %O Y))) in {Y} by PARTIT1:def 8;

      then

       A1: ( EqClass (y,( %O Y))) = Y by TARSKI:def 1;

       A2:

      now

        assume that

         A3: not (ex x be Element of Y st x in ( EqClass (y,( %O Y))) & (a . x) = TRUE ) and

         A4: for x be Element of Y holds (a . x) = FALSE ;

        ( B_SUP a) = ( O_el Y) by A4, Def14;

        then (( B_SUP a) . y) = FALSE by Def10;

        hence thesis by A3, Def17;

      end;

      now

        assume that

         A5: ex x be Element of Y st x in ( EqClass (y,( %O Y))) & (a . x) = TRUE and not (for x be Element of Y holds (a . x) = FALSE );

        ( B_SUP a) = ( I_el Y) by A5, Def14;

        then (( B_SUP a) . y) = TRUE by Def11;

        hence thesis by A5, Def17;

      end;

      hence thesis by A2, A1, XBOOLEAN:def 3;

    end;

    theorem :: BVFUNC_1:37

    for a be Function of Y, BOOLEAN holds ( B_INF (a,( %I Y))) = a

    proof

      let a be Function of Y, BOOLEAN ;

      let y be Element of Y;

       A1:

      now

        ( EqClass (y,( %I Y))) in ( %I Y);

        then ( EqClass (y,( %I Y))) in { B : ex z be set st B = {z} & z in Y } by PARTIT1: 31;

        then ex B st ( EqClass (y,( %I Y))) = B & ex z be set st B = {z} & z in Y;

        then

        consider z be set such that

         A2: ( EqClass (y,( %I Y))) = {z} and z in Y;

        

         A3: y in {z} by A2, EQREL_1:def 6;

        assume that

         A4: not (for x be Element of Y st x in ( EqClass (y,( %I Y))) holds (a . x) = TRUE ) and

         A5: (a . y) = TRUE ;

        consider x1 be Element of Y such that

         A6: x1 in ( EqClass (y,( %I Y))) and

         A7: (a . x1) <> TRUE by A4;

        x1 = z by A6, A2, TARSKI:def 1;

        hence contradiction by A5, A7, A3, TARSKI:def 1;

      end;

       A8:

      now

        assume

         A9: for x be Element of Y st x in ( EqClass (y,( %I Y))) holds (a . x) = TRUE ;

        then (a . y) = TRUE by EQREL_1:def 6;

        hence thesis by A9, Def16;

      end;

      now

        assume that

         A10: not (for x be Element of Y st x in ( EqClass (y,( %I Y))) holds (a . x) = TRUE ) and

         A11: (a . y) <> TRUE ;

        (a . y) = FALSE by A11, XBOOLEAN:def 3;

        hence thesis by A10, Def16;

      end;

      hence thesis by A8, A1;

    end;

    theorem :: BVFUNC_1:38

    for a be Function of Y, BOOLEAN holds ( B_SUP (a,( %I Y))) = a

    proof

      let a be Function of Y, BOOLEAN ;

      let y be Element of Y;

       A1:

      now

        ( EqClass (y,( %I Y))) in ( %I Y);

        then ( EqClass (y,( %I Y))) in { B : ex z be set st B = {z} & z in Y } by PARTIT1: 31;

        then ex B st ( EqClass (y,( %I Y))) = B & ex z be set st B = {z} & z in Y;

        then

        consider z be set such that

         A2: ( EqClass (y,( %I Y))) = {z} and z in Y;

        

         A3: y in {z} by A2, EQREL_1:def 6;

        assume that

         A4: ex x be Element of Y st x in ( EqClass (y,( %I Y))) & (a . x) = TRUE and

         A5: (a . y) <> TRUE ;

        consider x1 be Element of Y such that

         A6: x1 in ( EqClass (y,( %I Y))) and

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

        x1 = z by A6, A2, TARSKI:def 1;

        hence contradiction by A5, A7, A3, TARSKI:def 1;

      end;

       A8:

      now

        assume that

         A9: not (ex x be Element of Y st x in ( EqClass (y,( %I Y))) & (a . x) = TRUE ) and

         A10: (a . y) <> TRUE ;

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

        hence thesis by A9, Def17;

      end;

      y in ( EqClass (y,( %I Y))) by EQREL_1:def 6;

      hence thesis by A1, A8, Def17;

    end;

    theorem :: BVFUNC_1:39

    for a,b be Function of Y, BOOLEAN , PA be a_partition of Y holds ( B_INF ((a '&' b),PA)) = (( B_INF (a,PA)) '&' ( B_INF (b,PA)))

    proof

      let a,b be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      let y be Element of Y;

       A1:

      now

        assume that for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE and

         A2: not (for x be Element of Y st x in ( EqClass (y,PA)) holds (b . x) = TRUE );

        (( B_INF (b,PA)) . y) = FALSE by A2, Def16;

        then ((( B_INF (a,PA)) . y) '&' (( B_INF (b,PA)) . y)) = FALSE ;

        then

         A3: ((( B_INF (a,PA)) '&' ( B_INF (b,PA))) . y) = FALSE by MARGREL1:def 20;

        consider x1 be Element of Y such that

         A4: x1 in ( EqClass (y,PA)) and

         A5: (b . x1) <> TRUE by A2;

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

        then ((a . x1) '&' (b . x1)) = FALSE ;

        then ((a '&' b) . x1) <> TRUE by MARGREL1:def 20;

        hence thesis by A4, A3, Def16;

      end;

       A6:

      now

        assume that

         A7: not (for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ) and

         A8: not (for x be Element of Y st x in ( EqClass (y,PA)) holds (b . x) = TRUE );

        (( B_INF (b,PA)) . y) = FALSE by A8, Def16;

        then ((( B_INF (a,PA)) . y) '&' (( B_INF (b,PA)) . y)) = FALSE ;

        then

         A9: ((( B_INF (a,PA)) '&' ( B_INF (b,PA))) . y) = FALSE by MARGREL1:def 20;

        consider xa be Element of Y such that

         A10: xa in ( EqClass (y,PA)) and

         A11: (a . xa) <> TRUE by A7;

        (a . xa) = FALSE by A11, XBOOLEAN:def 3;

        then ((a . xa) '&' (b . xa)) = FALSE ;

        then ((a '&' b) . xa) <> TRUE by MARGREL1:def 20;

        hence thesis by A10, A9, Def16;

      end;

       A12:

      now

        assume that

         A13: for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE and

         A14: for x be Element of Y st x in ( EqClass (y,PA)) holds (b . x) = TRUE ;

        

         A15: for x be Element of Y st x in ( EqClass (y,PA)) holds ((a '&' b) . x) = TRUE

        proof

          let x be Element of Y;

          assume

           A16: x in ( EqClass (y,PA));

          then (b . x) = TRUE by A14;

          then ((a . x) '&' (b . x)) = ( TRUE '&' TRUE ) by A13, A16;

          hence thesis by MARGREL1:def 20;

        end;

        (( B_INF (b,PA)) . y) = TRUE by A14, Def16;

        then ((( B_INF (a,PA)) . y) '&' (( B_INF (b,PA)) . y)) = ( TRUE '&' TRUE ) by A13, Def16;

        then ((( B_INF (a,PA)) '&' ( B_INF (b,PA))) . y) = TRUE by MARGREL1:def 20;

        hence thesis by A15, Def16;

      end;

      now

        assume that

         A17: not (for x be Element of Y st x in ( EqClass (y,PA)) holds (a . x) = TRUE ) and

         A18: for x be Element of Y st x in ( EqClass (y,PA)) holds (b . x) = TRUE ;

        (( B_INF (b,PA)) . y) = TRUE by A18, Def16;

        then ((( B_INF (a,PA)) . y) '&' (( B_INF (b,PA)) . y)) = ( FALSE '&' TRUE ) by A17, Def16;

        then

         A19: ((( B_INF (a,PA)) '&' ( B_INF (b,PA))) . y) = FALSE by MARGREL1:def 20;

        consider x1 be Element of Y such that

         A20: x1 in ( EqClass (y,PA)) and

         A21: (a . x1) <> TRUE by A17;

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

        then ((a . x1) '&' (b . x1)) = FALSE ;

        then ((a '&' b) . x1) <> TRUE by MARGREL1:def 20;

        hence thesis by A20, A19, Def16;

      end;

      hence thesis by A12, A1, A6;

    end;

    theorem :: BVFUNC_1:40

    for a,b be Function of Y, BOOLEAN , PA be a_partition of Y holds ( B_SUP ((a 'or' b),PA)) = (( B_SUP (a,PA)) 'or' ( B_SUP (b,PA)))

    proof

      let a,b be Function of Y, BOOLEAN ;

      let PA be a_partition of Y;

      let y be Element of Y;

       A1:

      now

        assume

         A2: ex x be Element of Y st x in ( EqClass (y,PA)) & ((a 'or' b) . x) = TRUE ;

        then

        consider x1 be Element of Y such that

         A3: x1 in ( EqClass (y,PA)) and

         A4: ((a 'or' b) . x1) = TRUE ;

        

         A5: (a . x1) = FALSE & (b . x1) = FALSE or (a . x1) = FALSE & (b . x1) = TRUE or (a . x1) = TRUE & (b . x1) = FALSE or (a . x1) = TRUE & (b . x1) = TRUE by XBOOLEAN:def 3;

        

         A6: ((a . x1) 'or' (b . x1)) = TRUE by A4, Def4;

        now

          per cases by A6, A5;

            case (a . x1) = FALSE & (b . x1) = TRUE ;

            then (( B_SUP (b,PA)) . y) = TRUE by A3, Def17;

            then ((( B_SUP (a,PA)) . y) 'or' (( B_SUP (b,PA)) . y)) = TRUE ;

            then ((( B_SUP (a,PA)) 'or' ( B_SUP (b,PA))) . y) = TRUE by Def4;

            hence thesis by A2, Def17;

          end;

            case (a . x1) = TRUE & (b . x1) = FALSE ;

            then (( B_SUP (a,PA)) . y) = TRUE by A3, Def17;

            then ((( B_SUP (a,PA)) . y) 'or' (( B_SUP (b,PA)) . y)) = TRUE ;

            then ((( B_SUP (a,PA)) 'or' ( B_SUP (b,PA))) . y) = TRUE by Def4;

            hence thesis by A2, Def17;

          end;

            case (a . x1) = TRUE & (b . x1) = TRUE ;

            then (( B_SUP (b,PA)) . y) = TRUE by A3, Def17;

            then ((( B_SUP (a,PA)) . y) 'or' (( B_SUP (b,PA)) . y)) = TRUE ;

            then ((( B_SUP (a,PA)) 'or' ( B_SUP (b,PA))) . y) = TRUE by Def4;

            hence thesis by A2, Def17;

          end;

        end;

        hence thesis;

      end;

      now

        assume

         A7: not (ex x be Element of Y st x in ( EqClass (y,PA)) & ((a 'or' b) . x) = TRUE );

        now

          assume ex x be Element of Y st x in ( EqClass (y,PA)) & (b . x) = TRUE ;

          then

          consider x1 be Element of Y such that

           A8: x1 in ( EqClass (y,PA)) and

           A9: (b . x1) = TRUE ;

          ((a . x1) 'or' (b . x1)) = TRUE by A9;

          then ((a 'or' b) . x1) = TRUE by Def4;

          hence contradiction by A7, A8;

        end;

        then

         A10: (( B_SUP (b,PA)) . y) = FALSE by Def17;

        now

          assume ex x be Element of Y st x in ( EqClass (y,PA)) & (a . x) = TRUE ;

          then

          consider x1 be Element of Y such that

           A11: x1 in ( EqClass (y,PA)) and

           A12: (a . x1) = TRUE ;

          ((a . x1) 'or' (b . x1)) = TRUE by A12;

          then ((a 'or' b) . x1) = TRUE by Def4;

          hence contradiction by A7, A11;

        end;

        then ((( B_SUP (a,PA)) . y) 'or' (( B_SUP (b,PA)) . y)) = ( FALSE 'or' FALSE ) by A10, Def17;

        then ((( B_SUP (a,PA)) 'or' ( B_SUP (b,PA))) . y) = FALSE by Def4;

        hence thesis by A7, Def17;

      end;

      hence thesis by A1;

    end;

    definition

      let Y;

      let f be Function of Y, BOOLEAN ;

      :: BVFUNC_1:def18

      func GPart (f) -> a_partition of Y equals ( {{ x where x be Element of Y : (f . x) = TRUE }, { x9 where x9 be Element of Y : (f . x9) = FALSE }} \ { {} });

      correctness

      proof

        defpred P[ set] means (f . $1) = TRUE ;

        reconsider C = { x where x be Element of Y : P[x] } as Subset of Y from DOMAIN_1:sch 7;

        defpred P[ set] means (f . $1) = FALSE ;

        reconsider D = { x9 where x9 be Element of Y : P[x9] } as Subset of Y from DOMAIN_1:sch 7;

        

         A1: ( union ( {C, D} \ { {} })) = Y

        proof

          thus ( union ( {C, D} \ { {} })) c= Y

          proof

            let a be object;

            assume a in ( union ( {C, D} \ { {} }));

            then ex b be set st a in b & b in ( {C, D} \ { {} }) by TARSKI:def 4;

            then a in C or a in D by TARSKI:def 2;

            hence thesis;

          end;

          let a be object;

          

           A2: C in {C, D} by TARSKI:def 2;

          assume a in Y;

          then

          reconsider a as Element of Y;

          

           A3: (f . a) = TRUE or (f . a) = FALSE by TARSKI:def 2;

          

           A4: D in {C, D} by TARSKI:def 2;

          per cases by A3;

            suppose

             A5: a in C;

            then not C in { {} } by TARSKI:def 1;

            then C in ( {C, D} \ { {} }) by A2, XBOOLE_0:def 5;

            hence thesis by A5, TARSKI:def 4;

          end;

            suppose

             A6: a in D;

            then not D in { {} } by TARSKI:def 1;

            then D in ( {C, D} \ { {} }) by A4, XBOOLE_0:def 5;

            hence thesis by A6, TARSKI:def 4;

          end;

        end;

        

         A7: for A be Subset of Y st A in ( {C, D} \ { {} }) holds A <> {} & for B be Subset of Y st B in ( {C, D} \ { {} }) holds A = B or A misses B

        proof

          let A be Subset of Y;

           A8:

          now

            given b be object such that

             A9: b in C & b in D;

            now

              assume b in C;

              then

               A10: ex x be Element of Y st b = x & (f . x) = TRUE ;

              now

                assume b in D;

                then ex x9 be Element of Y st b = x9 & (f . x9) = FALSE ;

                hence contradiction by A10;

              end;

              hence not b in D;

            end;

            hence contradiction by A9;

          end;

          assume

           A11: A in ( {C, D} \ { {} });

          then not A in { {} } by XBOOLE_0:def 5;

          hence A <> {} by TARSKI:def 1;

          let B be Subset of Y;

          assume

           A12: B in ( {C, D} \ { {} });

          per cases by A11, A12, TARSKI:def 2;

            suppose A = C & B = C;

            hence thesis;

          end;

            suppose A = D & B = D;

            hence thesis;

          end;

            suppose A = C & B = D;

            hence thesis by A8, XBOOLE_0: 3;

          end;

            suppose A = D & B = C;

            hence thesis by A8, XBOOLE_0: 3;

          end;

        end;

        ( {C, D} \ { {} }) c= ( bool Y)

        proof

          let a be object;

          assume a in ( {C, D} \ { {} });

          then a = C or a = D by TARSKI:def 2;

          hence thesis;

        end;

        hence thesis by A1, A7, EQREL_1:def 4;

      end;

    end

    theorem :: BVFUNC_1:41

    for a be Function of Y, BOOLEAN holds a is_dependent_of ( GPart a)

    proof

      let a be Function of Y, BOOLEAN ;

      defpred P[ set] means (a . $1) = TRUE ;

      reconsider C = { x where x be Element of Y : P[x] } as Subset of Y from DOMAIN_1:sch 7;

      defpred P[ set] means (a . $1) = FALSE ;

      reconsider D = { x9 where x9 be Element of Y : P[x9] } as Subset of Y from DOMAIN_1:sch 7;

      for F be set st F in ( GPart a) holds for x1,x2 be set st x1 in F & x2 in F holds (a . x1) = (a . x2)

      proof

        let F be set;

        assume

         A1: F in ( GPart a);

        thus for x1,x2 be set st x1 in F & x2 in F holds (a . x1) = (a . 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;

          now

            per cases by A1, TARSKI:def 2;

              case F = C;

              then (ex x be Element of Y st x = x1 & (a . x) = TRUE ) & ex x5 be Element of Y st x5 = x2 & (a . x5) = TRUE by A2;

              hence thesis;

            end;

              case F = D;

              then (ex x be Element of Y st x = x1 & (a . x) = FALSE ) & ex x5 be Element of Y st x5 = x2 & (a . x5) = FALSE by A2;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_1:42

    for a be Function of Y, BOOLEAN , PA be a_partition of Y st a is_dependent_of PA holds PA is_finer_than ( GPart a)

    proof

      let a be Function of Y, BOOLEAN , PA be a_partition of Y;

      defpred P[ set] means (a . $1) = TRUE ;

      reconsider C = { x where x be Element of Y : P[x] } as Subset of Y from DOMAIN_1:sch 7;

      defpred P[ set] means (a . $1) = FALSE ;

      reconsider D = { x9 where x9 be Element of Y : P[x9] } as Subset of Y from DOMAIN_1:sch 7;

      assume

       A1: a is_dependent_of PA;

      for g be set st g in PA holds ex h be set st h in ( GPart a) & g c= h

      proof

        let g be set;

        set u = the Element of g;

        assume

         A2: g in PA;

        then

         A3: g <> {} by EQREL_1:def 4;

        then u in g;

        then

        reconsider u as Element of Y by A2;

        

         A4: for x1 be set st x1 in g holds (a . x1) = TRUE or (a . x1) = FALSE

        proof

          let x1 be set;

          assume x1 in g;

          then

          reconsider x1 as Element of Y by A2;

          (a . x1) in BOOLEAN ;

          hence thesis by TARSKI:def 2;

        end;

        now

          per cases by A3, A4;

            case

             A5: (a . u) = TRUE ;

            

             A6: g c= C

            proof

              let t be object;

              assume

               A7: t in g;

              then

              reconsider t as Element of Y by A2;

              now

                per cases by A4, A7;

                  case (a . t) = TRUE ;

                  hence thesis;

                end;

                  case (a . t) = FALSE ;

                  hence contradiction by A1, A2, A5, A7;

                end;

              end;

              hence thesis;

            end;

            u in C by A5;

            then

             A8: not C in { {} } by TARSKI:def 1;

            C in {C, D} by TARSKI:def 2;

            then C in ( {C, D} \ { {} }) by A8, XBOOLE_0:def 5;

            hence thesis by A6;

          end;

            case

             A9: (a . u) = FALSE ;

            

             A10: g c= D

            proof

              let t be object;

              assume

               A11: t in g;

              then

              reconsider t as Element of Y by A2;

              now

                per cases by A4, A11;

                  case (a . t) = TRUE ;

                  hence contradiction by A1, A2, A9, A11;

                end;

                  case (a . t) = FALSE ;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

            u in D by A9;

            then

             A12: not D in { {} } by TARSKI:def 1;

            D in {C, D} by TARSKI:def 2;

            then D in ( {C, D} \ { {} }) by A12, XBOOLE_0:def 5;

            hence thesis by A10;

          end;

        end;

        hence thesis;

      end;

      hence thesis by SETFAM_1:def 2;

    end;

    begin

    definition

      let x,y be Element of BOOLEAN ;

      :: original: 'nand'

      redefine

      func x 'nand' y -> Element of BOOLEAN ;

      correctness

      proof

        (x 'nand' y) = FALSE or (x 'nand' y) = TRUE by XBOOLEAN:def 3;

        hence thesis;

      end;

    end

    definition

      let x,y be Element of BOOLEAN ;

      :: original: 'nor'

      redefine

      func x 'nor' y -> Element of BOOLEAN ;

      correctness

      proof

        (x 'nor' y) = FALSE or (x 'nor' y) = TRUE by XBOOLEAN:def 3;

        hence thesis;

      end;

    end

    definition

      let x,y be boolean object;

      :: original: <=>

      redefine

      :: BVFUNC_1:def19

      func x <=> y equals ( 'not' (x 'xor' y));

      correctness ;

    end

    definition

      let x,y be Element of BOOLEAN ;

      :: original: <=>

      redefine

      func x <=> y -> Element of BOOLEAN ;

      correctness

      proof

        (x <=> y) = FALSE or (x <=> y) = TRUE by XBOOLEAN:def 3;

        hence thesis;

      end;

    end

    reserve x,y,z for boolean object;

    theorem :: BVFUNC_1:43

    ( TRUE 'nand' x) = ( 'not' x);

    theorem :: BVFUNC_1:44

    ( FALSE 'nand' x) = TRUE ;

    theorem :: BVFUNC_1:45

    (x 'nand' x) = ( 'not' x) & ( 'not' (x 'nand' x)) = x;

    theorem :: BVFUNC_1:46

    ( 'not' (x 'nand' y)) = (x '&' y);

    theorem :: BVFUNC_1:47

    (x 'nand' ( 'not' x)) = TRUE & ( 'not' (x 'nand' ( 'not' x))) = FALSE by XBOOLEAN: 135, XBOOLEAN: 138;

    theorem :: BVFUNC_1:48

    (x 'nand' (y '&' z)) = ( 'not' ((x '&' y) '&' z));

    theorem :: BVFUNC_1:49

    (x 'nand' (y '&' z)) = ((x '&' y) 'nand' z);

    theorem :: BVFUNC_1:50

    ( TRUE 'nor' x) = FALSE ;

    theorem :: BVFUNC_1:51

    ( FALSE 'nor' x) = ( 'not' x);

    theorem :: BVFUNC_1:52

    (x 'nor' x) = ( 'not' x) & ( 'not' (x 'nor' x)) = x;

    theorem :: BVFUNC_1:53

    ( 'not' (x 'nor' y)) = (x 'or' y);

    theorem :: BVFUNC_1:54

    (x 'nor' ( 'not' x)) = FALSE & ( 'not' (x 'nor' ( 'not' x))) = TRUE by XBOOLEAN: 134, XBOOLEAN: 138;

    theorem :: BVFUNC_1:55

    (x 'nor' (y 'or' z)) = ( 'not' ((x 'or' y) 'or' z));

    theorem :: BVFUNC_1:56

    ( TRUE <=> x) = x;

    theorem :: BVFUNC_1:57

    ( FALSE <=> x) = ( 'not' x);

    theorem :: BVFUNC_1:58

    (x <=> x) = TRUE & ( 'not' (x <=> x)) = FALSE by XBOOLEAN: 125, XBOOLEAN: 143;

    theorem :: BVFUNC_1:59

    ( 'not' (x <=> y)) = (x 'xor' y);

    theorem :: BVFUNC_1:60

    (x <=> ( 'not' x)) = FALSE & ( 'not' (x <=> ( 'not' x))) = TRUE by XBOOLEAN: 129, XBOOLEAN: 142;

    theorem :: BVFUNC_1:61

    x <= (y => z) iff (x '&' y) <= z;

    theorem :: BVFUNC_1:62

    (x <=> y) = ((x => y) '&' (y => x));

    theorem :: BVFUNC_1:63

    (x => y) = (( 'not' y) => ( 'not' x));

    theorem :: BVFUNC_1:64

    (x <=> y) = (( 'not' x) <=> ( 'not' y));

    theorem :: BVFUNC_1:65

    x = TRUE & (x => y) = TRUE implies y = TRUE ;

    theorem :: BVFUNC_1:66

    y = TRUE implies (x => y) = TRUE ;

    theorem :: BVFUNC_1:67

    ( 'not' x) = TRUE implies (x => y) = TRUE ;

    theorem :: BVFUNC_1:68

    (z => (y => x)) = TRUE implies (y => (z => x)) = TRUE ;

    theorem :: BVFUNC_1:69

    (z => (y => x)) = TRUE & y = TRUE implies (z => x) = TRUE ;

    theorem :: BVFUNC_1:70

    (z => (y => x)) = TRUE & y = TRUE & z = TRUE implies x = TRUE ;