bvfunc25.miz



    begin

    reserve Y for non empty set,

a,b,c,d for Function of Y, BOOLEAN ;

    theorem :: BVFUNC25:1

    

     Th1: ( 'not' (a 'imp' b)) = (a '&' ( 'not' b))

    proof

      

      thus ( 'not' (a 'imp' b)) = ( 'not' (( 'not' a) 'or' b)) by BVFUNC_4: 8

      .= (( 'not' ( 'not' a)) '&' ( 'not' b)) by BVFUNC_1: 13

      .= (a '&' ( 'not' b));

    end;

    theorem :: BVFUNC25:2

    

     Th2: (a 'imp' b) = (( 'not' b) 'imp' ( 'not' a))

    proof

      ((a 'imp' b) 'imp' (( 'not' b) 'imp' ( 'not' a))) = ( I_el Y) by BVFUNC_5: 32;

      then

       A1: (a 'imp' b) '<' (( 'not' b) 'imp' ( 'not' a)) by BVFUNC_1: 16;

      ((( 'not' b) 'imp' ( 'not' a)) 'imp' (a 'imp' b)) = ( I_el Y) by BVFUNC_5: 31;

      then (( 'not' b) 'imp' ( 'not' a)) '<' (a 'imp' b) by BVFUNC_1: 16;

      hence thesis by A1, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC25:3

    (a 'eqv' b) = (( 'not' a) 'eqv' ( 'not' b))

    proof

      

      thus (( 'not' a) 'eqv' ( 'not' b)) = ((( 'not' a) 'imp' ( 'not' b)) '&' (( 'not' b) 'imp' ( 'not' a))) by BVFUNC_4: 7

      .= ((b 'imp' a) '&' (( 'not' b) 'imp' ( 'not' a))) by Th2

      .= ((b 'imp' a) '&' (a 'imp' b)) by Th2

      .= (a 'eqv' b) by BVFUNC_4: 7;

    end;

    theorem :: BVFUNC25:4

    

     Th4: (a 'imp' b) = (a 'imp' (a '&' b))

    proof

      (a 'imp' (a '&' b)) = (( 'not' a) 'or' (a '&' b)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' a) '&' (( 'not' a) 'or' b)) by BVFUNC_1: 11

      .= (( I_el Y) '&' (( 'not' a) 'or' b)) by BVFUNC_4: 6

      .= (( 'not' a) 'or' b) by BVFUNC_1: 6;

      hence thesis by BVFUNC_4: 8;

    end;

    theorem :: BVFUNC25:5

    (a 'eqv' b) = ((a 'or' b) 'imp' (a '&' b))

    proof

      

      thus ((a 'or' b) 'imp' (a '&' b)) = ((a 'imp' (a '&' b)) '&' (b 'imp' (a '&' b))) by BVFUNC_6: 51

      .= ((a 'imp' b) '&' (b 'imp' (a '&' b))) by Th4

      .= ((a 'imp' b) '&' (b 'imp' a)) by Th4

      .= (a 'eqv' b) by BVFUNC_4: 7;

    end;

    theorem :: BVFUNC25:6

    (a 'eqv' ( 'not' a)) = ( O_el Y)

    proof

      

      thus (a 'eqv' ( 'not' a)) = ((a 'imp' ( 'not' a)) '&' (( 'not' a) 'imp' a)) by BVFUNC_4: 7

      .= ((( 'not' a) 'or' ( 'not' a)) '&' (( 'not' a) 'imp' a)) by BVFUNC_4: 8

      .= (( 'not' a) '&' (( 'not' ( 'not' a)) 'or' a)) by BVFUNC_4: 8

      .= ( O_el Y) by BVFUNC_4: 5;

    end;

    theorem :: BVFUNC25:7

    (a 'imp' (b 'imp' c)) = (b 'imp' (a 'imp' c))

    proof

      

      thus (a 'imp' (b 'imp' c)) = (( 'not' a) 'or' (b 'imp' c)) by BVFUNC_4: 8

      .= (( 'not' a) 'or' (( 'not' b) 'or' c)) by BVFUNC_4: 8

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

      .= (( 'not' b) 'or' (a 'imp' c)) by BVFUNC_4: 8

      .= (b 'imp' (a 'imp' c)) by BVFUNC_4: 8;

    end;

    theorem :: BVFUNC25:8

    (a 'imp' (b 'imp' c)) = ((a 'imp' b) 'imp' (a 'imp' c))

    proof

      

      thus ((a 'imp' b) 'imp' (a 'imp' c)) = ((a 'imp' b) 'imp' (( 'not' a) 'or' c)) by BVFUNC_4: 8

      .= (( 'not' (a 'imp' b)) 'or' (( 'not' a) 'or' c)) by BVFUNC_4: 8

      .= (( 'not' (( 'not' a) 'or' b)) 'or' (( 'not' a) 'or' c)) by BVFUNC_4: 8

      .= ((( 'not' ( 'not' a)) '&' ( 'not' b)) 'or' (( 'not' a) 'or' c)) by BVFUNC_1: 13

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

      .= (((a 'or' ( 'not' a)) '&' (( 'not' b) 'or' ( 'not' a))) 'or' c) by BVFUNC_1: 11

      .= ((( I_el Y) '&' (( 'not' b) 'or' ( 'not' a))) 'or' c) by BVFUNC_4: 6

      .= ((( 'not' a) 'or' ( 'not' b)) 'or' c) by BVFUNC_1: 6

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

      .= (( 'not' a) 'or' (b 'imp' c)) by BVFUNC_4: 8

      .= (a 'imp' (b 'imp' c)) by BVFUNC_4: 8;

    end;

    theorem :: BVFUNC25:9

    (a 'eqv' b) = (a 'xor' ( 'not' b))

    proof

      ( 'not' (a 'xor' b)) = ( 'not' ( 'not' (a 'eqv' b))) by BVFUNC_6: 85;

      hence thesis by BVFUNC_6: 90;

    end;

    theorem :: BVFUNC25:10

    

     Th11: (a '&' (b 'xor' c)) = ((a '&' b) 'xor' (a '&' c))

    proof

      

       A1: ((a '&' b) 'xor' (a '&' c)) = ((( 'not' (a '&' b)) '&' (a '&' c)) 'or' ((a '&' b) '&' ( 'not' (a '&' c)))) by BVFUNC_4: 9

      .= (((( 'not' a) 'or' ( 'not' b)) '&' (a '&' c)) 'or' ((a '&' b) '&' ( 'not' (a '&' c)))) by BVFUNC_1: 14

      .= (((a '&' c) '&' (( 'not' a) 'or' ( 'not' b))) 'or' ((a '&' b) '&' (( 'not' a) 'or' ( 'not' c)))) by BVFUNC_1: 14

      .= ((((a '&' c) '&' ( 'not' a)) 'or' ((a '&' c) '&' ( 'not' b))) 'or' ((a '&' b) '&' (( 'not' a) 'or' ( 'not' c)))) by BVFUNC_1: 12

      .= ((((a '&' c) '&' ( 'not' a)) 'or' ((a '&' c) '&' ( 'not' b))) 'or' (((a '&' b) '&' ( 'not' a)) 'or' ((a '&' b) '&' ( 'not' c)))) by BVFUNC_1: 12

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

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

      .= ((((a '&' c) '&' ( 'not' a)) 'or' ((a '&' b) '&' ( 'not' a))) 'or' (((a '&' c) '&' ( 'not' b)) 'or' ((a '&' b) '&' ( 'not' c)))) by BVFUNC_1: 8;

      

       A2: (((c '&' a) '&' ( 'not' a)) 'or' ((b '&' a) '&' ( 'not' a))) = ((c '&' (a '&' ( 'not' a))) 'or' ((b '&' a) '&' ( 'not' a))) by BVFUNC_1: 4

      .= ((c '&' (a '&' ( 'not' a))) 'or' (b '&' (a '&' ( 'not' a)))) by BVFUNC_1: 4

      .= ((c '&' ( O_el Y)) 'or' (b '&' (a '&' ( 'not' a)))) by BVFUNC_4: 5

      .= ((c '&' ( O_el Y)) 'or' (b '&' ( O_el Y))) by BVFUNC_4: 5

      .= (( O_el Y) 'or' (b '&' ( O_el Y))) by BVFUNC_1: 5

      .= (( O_el Y) 'or' ( O_el Y)) by BVFUNC_1: 5

      .= ( O_el Y);

      (a '&' (b 'xor' c)) = (a '&' ((( 'not' b) '&' c) 'or' (b '&' ( 'not' c)))) by BVFUNC_4: 9

      .= ((a '&' (( 'not' b) '&' c)) 'or' (a '&' (b '&' ( 'not' c)))) by BVFUNC_1: 12

      .= (((a '&' c) '&' ( 'not' b)) 'or' (a '&' (b '&' ( 'not' c)))) by BVFUNC_1: 4

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

      hence thesis by A1, A2, BVFUNC_1: 9;

    end;

    theorem :: BVFUNC25:11

    

     Th12: (a 'eqv' b) = ( 'not' (a 'xor' b))

    proof

      ( 'not' (a 'xor' b)) = ( 'not' ( 'not' (a 'eqv' b))) by BVFUNC_6: 85;

      hence thesis;

    end;

    theorem :: BVFUNC25:12

    

     Th13: (a 'xor' a) = ( O_el Y)

    proof

      

      thus (a 'xor' a) = ((( 'not' a) '&' a) 'or' (a '&' ( 'not' a))) by BVFUNC_4: 9

      .= ( O_el Y) by BVFUNC_4: 5;

    end;

    theorem :: BVFUNC25:13

    

     Th14: (a 'xor' ( 'not' a)) = ( I_el Y)

    proof

      

      thus (a 'xor' ( 'not' a)) = ((( 'not' a) '&' ( 'not' a)) 'or' (a '&' ( 'not' ( 'not' a)))) by BVFUNC_4: 9

      .= ( I_el Y) by BVFUNC_4: 6;

    end;

    theorem :: BVFUNC25:14

    

     Red1: ((a 'imp' b) 'imp' (b 'imp' a)) = (b 'imp' a)

    proof

      ((a 'imp' b) 'imp' (b 'imp' a)) = ((( 'not' a) 'or' b) 'imp' (b 'imp' a)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' b) 'imp' (( 'not' b) 'or' a)) by BVFUNC_4: 8

      .= (( 'not' (( 'not' a) 'or' b)) 'or' (( 'not' b) 'or' a)) by BVFUNC_4: 8

      .= ((( 'not' ( 'not' a)) '&' ( 'not' b)) 'or' (( 'not' b) 'or' a)) by BVFUNC_1: 13

      .= (((a '&' ( 'not' b)) 'or' ( 'not' b)) 'or' a) by BVFUNC_1: 8

      .= (((a 'or' ( 'not' b)) '&' (( 'not' b) 'or' ( 'not' b))) 'or' a) by BVFUNC_1: 11

      .= (((a 'or' ( 'not' b)) 'or' a) '&' (( 'not' b) 'or' a)) by BVFUNC_1: 11

      .= ((( 'not' b) 'or' (a 'or' a)) '&' (( 'not' b) 'or' a)) by BVFUNC_1: 8

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

      hence thesis by BVFUNC_4: 8;

    end;

    registration

      let Y, a, b;

      reduce ((a 'imp' b) 'imp' (b 'imp' a)) to (b 'imp' a);

      reducibility by Red1;

    end

    theorem :: BVFUNC25:15

    

     Th15: ((a 'or' b) '&' (( 'not' a) 'or' ( 'not' b))) = ((( 'not' a) '&' b) 'or' (a '&' ( 'not' b)))

    proof

      (a 'xor' b) = ((( 'not' a) '&' b) 'or' (a '&' ( 'not' b))) by BVFUNC_4: 9;

      hence thesis by BVFUNC_6: 86;

    end;

    theorem :: BVFUNC25:16

    

     Th16: ((a '&' b) 'or' (( 'not' a) '&' ( 'not' b))) = ((( 'not' a) 'or' b) '&' (a 'or' ( 'not' b)))

    proof

      

      thus ((a '&' b) 'or' (( 'not' a) '&' ( 'not' b))) = ((( 'not' a) 'or' b) '&' (( 'not' ( 'not' a)) 'or' ( 'not' b))) by Th15

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

    end;

    theorem :: BVFUNC25:17

    (a 'xor' (b 'xor' c)) = ((a 'xor' b) 'xor' c)

    proof

      

       A1: ((a 'xor' b) 'xor' c) = (((( 'not' a) '&' b) 'or' (a '&' ( 'not' b))) 'xor' c) by BVFUNC_4: 9

      .= ((( 'not' ((( 'not' a) '&' b) 'or' (a '&' ( 'not' b)))) '&' c) 'or' (((( 'not' a) '&' b) 'or' (a '&' ( 'not' b))) '&' ( 'not' c))) by BVFUNC_4: 9

      .= (((( 'not' (( 'not' a) '&' b)) '&' ( 'not' (a '&' ( 'not' b)))) '&' c) 'or' (((( 'not' a) '&' b) 'or' (a '&' ( 'not' b))) '&' ( 'not' c))) by BVFUNC_1: 13

      .= ((((( 'not' ( 'not' a)) 'or' ( 'not' b)) '&' ( 'not' (a '&' ( 'not' b)))) '&' c) 'or' (((( 'not' a) '&' b) 'or' (a '&' ( 'not' b))) '&' ( 'not' c))) by BVFUNC_1: 14

      .= ((((a 'or' ( 'not' b)) '&' (( 'not' a) 'or' ( 'not' ( 'not' b)))) '&' c) 'or' (((( 'not' a) '&' b) 'or' (a '&' ( 'not' b))) '&' ( 'not' c))) by BVFUNC_1: 14

      .= ((((a 'or' ( 'not' b)) '&' (( 'not' a) 'or' b)) '&' c) 'or' (((( 'not' a) '&' b) '&' ( 'not' c)) 'or' ((a '&' ( 'not' b)) '&' ( 'not' c)))) by BVFUNC_1: 12

      .= ((((a '&' b) 'or' (( 'not' a) '&' ( 'not' b))) '&' c) 'or' (((( 'not' a) '&' b) '&' ( 'not' c)) 'or' ((a '&' ( 'not' b)) '&' ( 'not' c)))) by Th16

      .= ((((a '&' b) '&' c) 'or' ((( 'not' a) '&' ( 'not' b)) '&' c)) 'or' (((( 'not' a) '&' b) '&' ( 'not' c)) 'or' ((a '&' ( 'not' b)) '&' ( 'not' c)))) by BVFUNC_1: 12

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

      .= (((((a '&' b) '&' c) 'or' ((a '&' ( 'not' b)) '&' ( 'not' c))) 'or' ((( 'not' a) '&' b) '&' ( 'not' c))) 'or' ((( 'not' a) '&' ( 'not' b)) '&' c)) by BVFUNC_1: 8;

      (a 'xor' (b 'xor' c)) = ((( 'not' a) '&' (b 'xor' c)) 'or' (a '&' ( 'not' (b 'xor' c)))) by BVFUNC_4: 9

      .= ((( 'not' a) '&' ((( 'not' b) '&' c) 'or' (b '&' ( 'not' c)))) 'or' (a '&' ( 'not' (b 'xor' c)))) by BVFUNC_4: 9

      .= ((( 'not' a) '&' ((( 'not' b) '&' c) 'or' (b '&' ( 'not' c)))) 'or' (a '&' ( 'not' ((( 'not' b) '&' c) 'or' (b '&' ( 'not' c)))))) by BVFUNC_4: 9

      .= (((( 'not' a) '&' (( 'not' b) '&' c)) 'or' (( 'not' a) '&' (b '&' ( 'not' c)))) 'or' (a '&' ( 'not' ((( 'not' b) '&' c) 'or' (b '&' ( 'not' c)))))) by BVFUNC_1: 12

      .= (((( 'not' a) '&' (( 'not' b) '&' c)) 'or' (( 'not' a) '&' (b '&' ( 'not' c)))) 'or' (a '&' (( 'not' (( 'not' b) '&' c)) '&' ( 'not' (b '&' ( 'not' c)))))) by BVFUNC_1: 13

      .= (((( 'not' a) '&' (( 'not' b) '&' c)) 'or' (( 'not' a) '&' (b '&' ( 'not' c)))) 'or' (a '&' ((( 'not' ( 'not' b)) 'or' ( 'not' c)) '&' ( 'not' (b '&' ( 'not' c)))))) by BVFUNC_1: 14

      .= (((( 'not' a) '&' (( 'not' b) '&' c)) 'or' (( 'not' a) '&' (b '&' ( 'not' c)))) 'or' (a '&' ((b 'or' ( 'not' c)) '&' (( 'not' b) 'or' ( 'not' ( 'not' c)))))) by BVFUNC_1: 14

      .= (((( 'not' a) '&' (( 'not' b) '&' c)) 'or' (( 'not' a) '&' (b '&' ( 'not' c)))) 'or' (a '&' ((b '&' c) 'or' (( 'not' b) '&' ( 'not' c))))) by Th16

      .= (((( 'not' a) '&' (( 'not' b) '&' c)) 'or' (( 'not' a) '&' (b '&' ( 'not' c)))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (( 'not' b) '&' ( 'not' c))))) by BVFUNC_1: 12

      .= ((((( 'not' a) '&' ( 'not' b)) '&' c) 'or' (( 'not' a) '&' (b '&' ( 'not' c)))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (( 'not' b) '&' ( 'not' c))))) by BVFUNC_1: 4

      .= ((((( 'not' a) '&' ( 'not' b)) '&' c) 'or' ((( 'not' a) '&' b) '&' ( 'not' c))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (( 'not' b) '&' ( 'not' c))))) by BVFUNC_1: 4

      .= ((((( 'not' a) '&' ( 'not' b)) '&' c) 'or' ((( 'not' a) '&' b) '&' ( 'not' c))) 'or' (((a '&' b) '&' c) 'or' (a '&' (( 'not' b) '&' ( 'not' c))))) by BVFUNC_1: 4

      .= ((((a '&' b) '&' c) 'or' ((a '&' ( 'not' b)) '&' ( 'not' c))) 'or' (((( 'not' a) '&' b) '&' ( 'not' c)) 'or' ((( 'not' a) '&' ( 'not' b)) '&' c))) by BVFUNC_1: 4

      .= (((((a '&' b) '&' c) 'or' ((a '&' ( 'not' b)) '&' ( 'not' c))) 'or' ((( 'not' a) '&' b) '&' ( 'not' c))) 'or' ((( 'not' a) '&' ( 'not' b)) '&' c)) by BVFUNC_1: 8;

      hence thesis by A1;

    end;

    theorem :: BVFUNC25:18

    (a 'eqv' (b 'eqv' c)) = ((a 'eqv' b) 'eqv' c)

    proof

      

       A1: ((a 'eqv' b) 'eqv' c) = (((a 'eqv' b) 'imp' c) '&' (c 'imp' (a 'eqv' b))) by BVFUNC_4: 7

      .= ((((a 'imp' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' (a 'eqv' b))) by BVFUNC_4: 7

      .= ((((a 'imp' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a)))) by BVFUNC_4: 7

      .= ((((( 'not' a) 'or' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a)))) by BVFUNC_4: 8

      .= ((((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a)))) by BVFUNC_4: 8

      .= ((( 'not' ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a))) 'or' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a)))) by BVFUNC_4: 8

      .= ((( 'not' ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a))) 'or' c) '&' (( 'not' c) 'or' ((a 'imp' b) '&' (b 'imp' a)))) by BVFUNC_4: 8

      .= ((( 'not' ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a))) 'or' c) '&' (( 'not' c) 'or' ((( 'not' a) 'or' b) '&' (b 'imp' a)))) by BVFUNC_4: 8

      .= ((( 'not' ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a))) 'or' c) '&' (( 'not' c) 'or' ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a)))) by BVFUNC_4: 8

      .= (((( 'not' (( 'not' a) 'or' b)) 'or' ( 'not' (( 'not' b) 'or' a))) 'or' c) '&' (( 'not' c) 'or' ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a)))) by BVFUNC_1: 14

      .= ((((( 'not' ( 'not' a)) '&' ( 'not' b)) 'or' ( 'not' (( 'not' b) 'or' a))) 'or' c) '&' (( 'not' c) 'or' ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a)))) by BVFUNC_1: 13

      .= ((((a '&' ( 'not' b)) 'or' (( 'not' ( 'not' b)) '&' ( 'not' a))) 'or' c) '&' (( 'not' c) 'or' ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a)))) by BVFUNC_1: 13

      .= ((((a 'or' b) '&' (( 'not' a) 'or' ( 'not' b))) 'or' c) '&' (( 'not' c) 'or' ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a)))) by Th15

      .= ((((a 'or' b) 'or' c) '&' ((( 'not' a) 'or' ( 'not' b)) 'or' c)) '&' (( 'not' c) 'or' ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' a)))) by BVFUNC_1: 11

      .= ((((a 'or' b) 'or' c) '&' ((( 'not' a) 'or' ( 'not' b)) 'or' c)) '&' (((a 'or' ( 'not' b)) 'or' ( 'not' c)) '&' ((( 'not' a) 'or' b) 'or' ( 'not' c)))) by BVFUNC_1: 11

      .= ((((a 'or' b) 'or' c) '&' (((a 'or' ( 'not' b)) 'or' ( 'not' c)) '&' ((( 'not' a) 'or' b) 'or' ( 'not' c)))) '&' ((( 'not' a) 'or' ( 'not' b)) 'or' c)) by BVFUNC_1: 4

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

      (a 'eqv' (b 'eqv' c)) = ((a 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' a)) by BVFUNC_4: 7

      .= ((a 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' ((b 'eqv' c) 'imp' a)) by BVFUNC_4: 7

      .= ((a 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a)) by BVFUNC_4: 7

      .= ((( 'not' a) 'or' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' ((( 'not' b) 'or' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' ((( 'not' b) 'or' c) '&' (( 'not' c) 'or' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' ((( 'not' b) 'or' c) '&' (( 'not' c) 'or' b))) '&' (((( 'not' b) 'or' c) '&' (c 'imp' b)) 'imp' a)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' ((( 'not' b) 'or' c) '&' (( 'not' c) 'or' b))) '&' (((( 'not' b) 'or' c) '&' (( 'not' c) 'or' b)) 'imp' a)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' ((( 'not' b) 'or' c) '&' (( 'not' c) 'or' b))) '&' (( 'not' ((( 'not' b) 'or' c) '&' (( 'not' c) 'or' b))) 'or' a)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' ((( 'not' b) 'or' c) '&' (( 'not' c) 'or' b))) '&' ((( 'not' (( 'not' b) 'or' c)) 'or' ( 'not' (( 'not' c) 'or' b))) 'or' a)) by BVFUNC_1: 14

      .= ((( 'not' a) 'or' ((( 'not' b) 'or' c) '&' (( 'not' c) 'or' b))) '&' (((( 'not' ( 'not' b)) '&' ( 'not' c)) 'or' ( 'not' (( 'not' c) 'or' b))) 'or' a)) by BVFUNC_1: 13

      .= ((( 'not' a) 'or' ((( 'not' b) 'or' c) '&' (( 'not' c) 'or' b))) '&' (((b '&' ( 'not' c)) 'or' (( 'not' ( 'not' c)) '&' ( 'not' b))) 'or' a)) by BVFUNC_1: 13

      .= ((( 'not' a) 'or' ((( 'not' b) 'or' c) '&' (( 'not' c) 'or' b))) '&' (((b 'or' c) '&' (( 'not' b) 'or' ( 'not' c))) 'or' a)) by Th15

      .= (((( 'not' a) 'or' (( 'not' b) 'or' c)) '&' (( 'not' a) 'or' (( 'not' c) 'or' b))) '&' (((b 'or' c) '&' (( 'not' b) 'or' ( 'not' c))) 'or' a)) by BVFUNC_1: 11

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

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

      .= ((((( 'not' a) 'or' ( 'not' b)) 'or' c) '&' ((( 'not' a) 'or' b) 'or' ( 'not' c))) '&' ((a 'or' (b 'or' c)) '&' (a 'or' (( 'not' b) 'or' ( 'not' c))))) by BVFUNC_1: 11

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

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

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

      hence thesis by A1;

    end;

    theorem :: BVFUNC25:19

    (( 'not' ( 'not' a)) 'imp' a) = ( I_el Y) by BVFUNC_5: 7;

    theorem :: BVFUNC25:20

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

    proof

      (((a 'imp' b) '&' a) 'imp' b) = ((a '&' b) 'imp' b) by BVFUNC_6: 56;

      hence thesis by BVFUNC_6: 40;

    end;

    theorem :: BVFUNC25:21

    

     Th21: (a 'imp' (( 'not' a) 'imp' a)) = ( I_el Y)

    proof

      (a 'imp' (( 'not' a) 'imp' a)) = (( 'not' a) 'or' (( 'not' a) 'imp' a)) by BVFUNC_4: 8

      .= (( 'not' a) 'or' (( 'not' ( 'not' a)) 'or' a)) by BVFUNC_4: 8

      .= (( 'not' a) 'or' a);

      hence thesis by BVFUNC_4: 6;

    end;

    theorem :: BVFUNC25:22

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

    proof

      ((( 'not' a) 'imp' a) 'eqv' a) = (((( 'not' a) 'imp' a) 'imp' a) '&' (a 'imp' (( 'not' a) 'imp' a))) by BVFUNC_4: 7

      .= (( I_el Y) '&' (a 'imp' (( 'not' a) 'imp' a))) by BVFUNC_5: 11

      .= (a 'imp' (( 'not' a) 'imp' a)) by BVFUNC_1: 6;

      hence thesis by Th21;

    end;

    theorem :: BVFUNC25:23

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

    proof

      (a 'or' (a 'imp' b)) = (a 'or' (( 'not' a) 'or' b)) by BVFUNC_4: 8

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

      .= (( I_el Y) 'or' b) by BVFUNC_4: 6;

      hence thesis by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:24

    ((a 'imp' b) 'or' (c 'imp' a)) = ( I_el Y)

    proof

      ((a 'imp' b) 'or' (c 'imp' a)) = ((( 'not' a) 'or' b) 'or' (c 'imp' a)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' b) 'or' (( 'not' c) 'or' a)) by BVFUNC_4: 8

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

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

      .= (( 'not' c) 'or' (( I_el Y) 'or' b)) by BVFUNC_4: 6

      .= (( 'not' c) 'or' ( I_el Y)) by BVFUNC_1: 10;

      hence thesis by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:25

    ((a 'imp' b) 'or' (( 'not' a) 'imp' b)) = ( I_el Y)

    proof

      ((a 'imp' b) 'or' (( 'not' a) 'imp' b)) = ((( 'not' a) 'or' b) 'or' (( 'not' a) 'imp' b)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' b) 'or' (( 'not' ( 'not' a)) 'or' b)) by BVFUNC_4: 8

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

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

      .= (b 'or' (( I_el Y) 'or' b)) by BVFUNC_4: 6

      .= (b 'or' ( I_el Y)) by BVFUNC_1: 10;

      hence thesis by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:26

    ((a 'imp' b) 'or' (a 'imp' ( 'not' b))) = ( I_el Y)

    proof

      ((a 'imp' b) 'or' (a 'imp' ( 'not' b))) = ((( 'not' a) 'or' b) 'or' (a 'imp' ( 'not' b))) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' b) 'or' (( 'not' a) 'or' ( 'not' b))) by BVFUNC_4: 8

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

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

      .= (( 'not' a) 'or' (( I_el Y) 'or' ( 'not' a))) by BVFUNC_4: 6

      .= (( 'not' a) 'or' ( I_el Y)) by BVFUNC_1: 10;

      hence thesis by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:27

    (( 'not' a) 'imp' (( 'not' b) 'eqv' (b 'imp' a))) = ( I_el Y)

    proof

      (( 'not' a) 'imp' (( 'not' b) 'eqv' (b 'imp' a))) = (( 'not' ( 'not' a)) 'or' (( 'not' b) 'eqv' (b 'imp' a))) by BVFUNC_4: 8

      .= (a 'or' ((( 'not' b) 'imp' (b 'imp' a)) '&' ((b 'imp' a) 'imp' ( 'not' b)))) by BVFUNC_4: 7

      .= (a 'or' ((( 'not' ( 'not' b)) 'or' (b 'imp' a)) '&' ((b 'imp' a) 'imp' ( 'not' b)))) by BVFUNC_4: 8

      .= (a 'or' ((b 'or' (( 'not' b) 'or' a)) '&' ((b 'imp' a) 'imp' ( 'not' b)))) by BVFUNC_4: 8

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

      .= (a 'or' ((( I_el Y) 'or' a) '&' ((b 'imp' a) 'imp' ( 'not' b)))) by BVFUNC_4: 6

      .= (a 'or' (( I_el Y) '&' ((b 'imp' a) 'imp' ( 'not' b)))) by BVFUNC_1: 10

      .= (a 'or' ((b 'imp' a) 'imp' ( 'not' b))) by BVFUNC_1: 6

      .= (a 'or' ((( 'not' b) 'or' a) 'imp' ( 'not' b))) by BVFUNC_4: 8

      .= (a 'or' (( 'not' (( 'not' b) 'or' a)) 'or' ( 'not' b))) by BVFUNC_4: 8

      .= (a 'or' ((( 'not' ( 'not' b)) '&' ( 'not' a)) 'or' ( 'not' b))) by BVFUNC_1: 13

      .= (a 'or' ((b 'or' ( 'not' b)) '&' (( 'not' a) 'or' ( 'not' b)))) by BVFUNC_1: 11

      .= (a 'or' (( I_el Y) '&' (( 'not' a) 'or' ( 'not' b)))) by BVFUNC_4: 6

      .= (a 'or' (( 'not' a) 'or' ( 'not' b))) by BVFUNC_1: 6

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

      .= (( I_el Y) 'or' ( 'not' b)) by BVFUNC_4: 6;

      hence thesis by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:28

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

    proof

      ((a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b)) = (( 'not' (a 'imp' b)) 'or' (((a 'imp' c) 'imp' b) 'imp' b)) by BVFUNC_4: 8

      .= (( 'not' (( 'not' a) 'or' b)) 'or' (((a 'imp' c) 'imp' b) 'imp' b)) by BVFUNC_4: 8

      .= ((( 'not' ( 'not' a)) '&' ( 'not' b)) 'or' (((a 'imp' c) 'imp' b) 'imp' b)) by BVFUNC_1: 13

      .= ((a '&' ( 'not' b)) 'or' (( 'not' ((a 'imp' c) 'imp' b)) 'or' b)) by BVFUNC_4: 8

      .= ((a '&' ( 'not' b)) 'or' (( 'not' ((( 'not' a) 'or' c) 'imp' b)) 'or' b)) by BVFUNC_4: 8

      .= ((a '&' ( 'not' b)) 'or' (( 'not' (( 'not' (( 'not' a) 'or' c)) 'or' b)) 'or' b)) by BVFUNC_4: 8

      .= ((a '&' ( 'not' b)) 'or' (( 'not' ((( 'not' ( 'not' a)) '&' ( 'not' c)) 'or' b)) 'or' b)) by BVFUNC_1: 13

      .= ((a '&' ( 'not' b)) 'or' ((( 'not' (a '&' ( 'not' c))) '&' ( 'not' b)) 'or' b)) by BVFUNC_1: 13

      .= ((a '&' ( 'not' b)) 'or' (((( 'not' a) 'or' ( 'not' ( 'not' c))) '&' ( 'not' b)) 'or' b)) by BVFUNC_1: 14

      .= ((a '&' ( 'not' b)) 'or' (((( 'not' a) 'or' c) 'or' b) '&' (( 'not' b) 'or' b))) by BVFUNC_1: 11

      .= ((a '&' ( 'not' b)) 'or' (((( 'not' a) 'or' c) 'or' b) '&' ( I_el Y))) by BVFUNC_4: 6

      .= ((a '&' ( 'not' b)) 'or' ((( 'not' a) 'or' c) 'or' b)) by BVFUNC_1: 6

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

      .= (((a 'or' b) '&' (( 'not' b) 'or' b)) 'or' (( 'not' a) 'or' c)) by BVFUNC_1: 11

      .= (((a 'or' b) '&' ( I_el Y)) 'or' (( 'not' a) 'or' c)) by BVFUNC_4: 6

      .= ((a 'or' b) 'or' (( 'not' a) 'or' c)) by BVFUNC_1: 6

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

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

      .= (b 'or' (( I_el Y) 'or' c)) by BVFUNC_4: 6

      .= (b 'or' ( I_el Y)) by BVFUNC_1: 10;

      hence thesis by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:29

    (a 'imp' b) = (a 'eqv' (a '&' b))

    proof

      (a 'eqv' (a '&' b)) = ((a 'imp' (a '&' b)) '&' ((a '&' b) 'imp' a)) by BVFUNC_4: 7

      .= ((( 'not' a) 'or' (a '&' b)) '&' ((a '&' b) 'imp' a)) by BVFUNC_4: 8

      .= ((( 'not' a) 'or' (a '&' b)) '&' (( 'not' (a '&' b)) 'or' a)) by BVFUNC_4: 8

      .= (((( 'not' a) 'or' a) '&' (( 'not' a) 'or' b)) '&' (( 'not' (a '&' b)) 'or' a)) by BVFUNC_1: 11

      .= ((( I_el Y) '&' (( 'not' a) 'or' b)) '&' (( 'not' (a '&' b)) 'or' a)) by BVFUNC_4: 6

      .= ((( 'not' a) 'or' b) '&' (( 'not' (a '&' b)) 'or' a)) by BVFUNC_1: 6

      .= ((( 'not' a) 'or' b) '&' ((( 'not' a) 'or' ( 'not' b)) 'or' a)) by BVFUNC_1: 14

      .= ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' (( 'not' a) 'or' a))) by BVFUNC_1: 8

      .= ((( 'not' a) 'or' b) '&' (( 'not' b) 'or' ( I_el Y))) by BVFUNC_4: 6

      .= ((( 'not' a) 'or' b) '&' ( I_el Y)) by BVFUNC_1: 10

      .= (( 'not' a) 'or' b) by BVFUNC_1: 6;

      hence thesis by BVFUNC_4: 8;

    end;

    theorem :: BVFUNC25:30

    (a 'imp' b) = ( I_el Y) & (b 'imp' a) = ( I_el Y) iff a = b

    proof

      (a 'eqv' b) = ( I_el Y) iff (a 'imp' b) = ( I_el Y) & (b 'imp' a) = ( I_el Y) by BVFUNC_4: 10;

      hence thesis by BVFUNC_1: 17;

    end;

    theorem :: BVFUNC25:31

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

    proof

      ((( 'not' a) 'imp' a) 'imp' a) = ( I_el Y) by BVFUNC_5: 11;

      then

       A1: (( 'not' a) 'imp' a) '<' a by BVFUNC_1: 16;

      (a 'imp' (( 'not' a) 'imp' a)) = ( I_el Y) by Th21;

      then a '<' (( 'not' a) 'imp' a) by BVFUNC_1: 16;

      hence thesis by A1, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC25:32

    

     Th32: (a 'imp' ((a 'imp' b) 'imp' a)) = ( I_el Y)

    proof

      

      thus (a 'imp' ((a 'imp' b) 'imp' a)) = (( 'not' a) 'or' ((a 'imp' b) 'imp' a)) by BVFUNC_4: 8

      .= (( 'not' a) 'or' (( 'not' (a 'imp' b)) 'or' a)) by BVFUNC_4: 8

      .= (( 'not' a) 'or' (( 'not' (( 'not' a) 'or' b)) 'or' a)) by BVFUNC_4: 8

      .= (( 'not' a) 'or' ((( 'not' ( 'not' a)) '&' ( 'not' b)) 'or' a)) by BVFUNC_1: 13

      .= ((( 'not' a) 'or' a) 'or' (a '&' ( 'not' b))) by BVFUNC_1: 8

      .= (( I_el Y) 'or' (a '&' ( 'not' b))) by BVFUNC_4: 6

      .= ( I_el Y) by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:33

    a = ((a 'imp' b) 'imp' a)

    proof

      (((a 'imp' b) 'imp' a) 'imp' a) = ( I_el Y) by BVFUNC_6: 100;

      then

       A1: ((a 'imp' b) 'imp' a) '<' a by BVFUNC_1: 16;

      (a 'imp' ((a 'imp' b) 'imp' a)) = ( I_el Y) by Th32;

      then a '<' ((a 'imp' b) 'imp' a) by BVFUNC_1: 16;

      hence thesis by A1, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC25:34

    a = ((b 'imp' a) '&' (( 'not' b) 'imp' a))

    proof

      a = ((a 'or' b) '&' (a 'or' ( 'not' b))) by BVFUNC_6: 80

      .= ((a 'or' ( 'not' ( 'not' b))) '&' (b 'imp' a)) by BVFUNC_4: 8

      .= ((( 'not' b) 'imp' a) '&' (b 'imp' a)) by BVFUNC_4: 8;

      hence thesis;

    end;

    theorem :: BVFUNC25:35

    (a '&' b) = ( 'not' (a 'imp' ( 'not' b)))

    proof

      (( 'not' (a 'imp' ( 'not' b))) 'imp' (a '&' b)) = ( I_el Y) by BVFUNC_6: 35;

      then

       A1: ( 'not' (a 'imp' ( 'not' b))) '<' (a '&' b) by BVFUNC_1: 16;

      ((a '&' b) 'imp' ( 'not' (a 'imp' ( 'not' b)))) = ( I_el Y) by BVFUNC_6: 34;

      then (a '&' b) '<' ( 'not' (a 'imp' ( 'not' b))) by BVFUNC_1: 16;

      hence thesis by A1, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC25:36

    (a 'or' b) = (( 'not' a) 'imp' b)

    proof

      

      thus (( 'not' a) 'imp' b) = (( 'not' ( 'not' a)) 'or' b) by BVFUNC_4: 8

      .= (a 'or' b);

    end;

    theorem :: BVFUNC25:37

    (a 'or' b) = ((a 'imp' b) 'imp' b)

    proof

      

      thus ((a 'imp' b) 'imp' b) = (( 'not' (a 'imp' b)) 'or' b) by BVFUNC_4: 8

      .= (( 'not' (( 'not' a) 'or' b)) 'or' b) by BVFUNC_4: 8

      .= ((( 'not' ( 'not' a)) '&' ( 'not' b)) 'or' b) by BVFUNC_1: 13

      .= ((a 'or' b) '&' (( 'not' b) 'or' b)) by BVFUNC_1: 11

      .= ((a 'or' b) '&' ( I_el Y)) by BVFUNC_4: 6

      .= (a 'or' b) by BVFUNC_1: 6;

    end;

    theorem :: BVFUNC25:38

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

    proof

      

      thus ((a 'imp' b) 'imp' (a 'imp' a)) = ((a 'imp' b) 'imp' ( I_el Y)) by BVFUNC_5: 7

      .= ( I_el Y) by BVFUNC_6: 62;

    end;

    theorem :: BVFUNC25:39

    ((a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c)))) = ( I_el Y)

    proof

      

      thus ((a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c)))) = (( 'not' (a 'imp' (b 'imp' c))) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c)))) by BVFUNC_4: 8

      .= (( 'not' (( 'not' a) 'or' (b 'imp' c))) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c)))) by BVFUNC_4: 8

      .= (( 'not' (( 'not' a) 'or' (( 'not' b) 'or' c))) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c)))) by BVFUNC_4: 8

      .= (( 'not' (( 'not' a) 'or' (( 'not' b) 'or' c))) 'or' (( 'not' (d 'imp' b)) 'or' (a 'imp' (d 'imp' c)))) by BVFUNC_4: 8

      .= (( 'not' (( 'not' a) 'or' (( 'not' b) 'or' c))) 'or' (( 'not' (( 'not' d) 'or' b)) 'or' (a 'imp' (d 'imp' c)))) by BVFUNC_4: 8

      .= (( 'not' (( 'not' a) 'or' (( 'not' b) 'or' c))) 'or' (( 'not' (( 'not' d) 'or' b)) 'or' (( 'not' a) 'or' (d 'imp' c)))) by BVFUNC_4: 8

      .= (( 'not' (( 'not' a) 'or' (( 'not' b) 'or' c))) 'or' (( 'not' (( 'not' d) 'or' b)) 'or' (( 'not' a) 'or' (( 'not' d) 'or' c)))) by BVFUNC_4: 8

      .= ((( 'not' ( 'not' a)) '&' ( 'not' (( 'not' b) 'or' c))) 'or' (( 'not' (( 'not' d) 'or' b)) 'or' (( 'not' a) 'or' (( 'not' d) 'or' c)))) by BVFUNC_1: 13

      .= ((( 'not' ( 'not' a)) '&' (( 'not' ( 'not' b)) '&' ( 'not' c))) 'or' (( 'not' (( 'not' d) 'or' b)) 'or' (( 'not' a) 'or' (( 'not' d) 'or' c)))) by BVFUNC_1: 13

      .= ((a '&' (( 'not' ( 'not' b)) '&' ( 'not' c))) 'or' ((( 'not' ( 'not' d)) '&' ( 'not' b)) 'or' (( 'not' a) 'or' (( 'not' d) 'or' c)))) by BVFUNC_1: 13

      .= ((a '&' (b '&' ( 'not' c))) 'or' (((d '&' ( 'not' b)) 'or' ( 'not' a)) 'or' (( 'not' d) 'or' c))) by BVFUNC_1: 8

      .= (((a '&' (b '&' ( 'not' c))) 'or' (( 'not' a) 'or' (d '&' ( 'not' b)))) 'or' (( 'not' d) 'or' c)) by BVFUNC_1: 8

      .= ((((a '&' (b '&' ( 'not' c))) 'or' ( 'not' a)) 'or' (d '&' ( 'not' b))) 'or' (( 'not' d) 'or' c)) by BVFUNC_1: 8

      .= ((((a 'or' ( 'not' a)) '&' ((b '&' ( 'not' c)) 'or' ( 'not' a))) 'or' (d '&' ( 'not' b))) 'or' (( 'not' d) 'or' c)) by BVFUNC_1: 11

      .= (((( I_el Y) '&' ((b '&' ( 'not' c)) 'or' ( 'not' a))) 'or' (d '&' ( 'not' b))) 'or' (( 'not' d) 'or' c)) by BVFUNC_4: 6

      .= ((((b '&' ( 'not' c)) 'or' ( 'not' a)) 'or' (d '&' ( 'not' b))) 'or' (( 'not' d) 'or' c)) by BVFUNC_1: 6

      .= (((b '&' ( 'not' c)) 'or' ( 'not' a)) 'or' ((d '&' ( 'not' b)) 'or' (( 'not' d) 'or' c))) by BVFUNC_1: 8

      .= (((b '&' ( 'not' c)) 'or' ( 'not' a)) 'or' (((( 'not' b) '&' d) 'or' ( 'not' d)) 'or' c)) by BVFUNC_1: 8

      .= (((b '&' ( 'not' c)) 'or' ( 'not' a)) 'or' (((( 'not' b) 'or' ( 'not' d)) '&' (d 'or' ( 'not' d))) 'or' c)) by BVFUNC_1: 11

      .= (((b '&' ( 'not' c)) 'or' ( 'not' a)) 'or' (((( 'not' b) 'or' ( 'not' d)) '&' ( I_el Y)) 'or' c)) by BVFUNC_4: 6

      .= (((b '&' ( 'not' c)) 'or' ( 'not' a)) 'or' ((( 'not' b) 'or' ( 'not' d)) 'or' c)) by BVFUNC_1: 6

      .= (( 'not' a) 'or' ((( 'not' c) '&' b) 'or' ((( 'not' b) 'or' ( 'not' d)) 'or' c))) by BVFUNC_1: 8

      .= (( 'not' a) 'or' (((( 'not' c) '&' b) 'or' (( 'not' b) 'or' ( 'not' d))) 'or' c)) by BVFUNC_1: 8

      .= (( 'not' a) 'or' ((((( 'not' c) '&' b) 'or' ( 'not' b)) 'or' ( 'not' d)) 'or' c)) by BVFUNC_1: 8

      .= (( 'not' a) 'or' ((((( 'not' c) 'or' ( 'not' b)) '&' (b 'or' ( 'not' b))) 'or' ( 'not' d)) 'or' c)) by BVFUNC_1: 11

      .= (( 'not' a) 'or' ((((( 'not' c) 'or' ( 'not' b)) '&' ( I_el Y)) 'or' ( 'not' d)) 'or' c)) by BVFUNC_4: 6

      .= (( 'not' a) 'or' (((( 'not' b) 'or' ( 'not' c)) 'or' ( 'not' d)) 'or' c)) by BVFUNC_1: 6

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

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

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

      .= (( 'not' a) 'or' (( 'not' b) 'or' (( 'not' d) 'or' ( I_el Y)))) by BVFUNC_4: 6

      .= (( 'not' a) 'or' (( 'not' b) 'or' ( I_el Y))) by BVFUNC_1: 10

      .= (( 'not' a) 'or' ( I_el Y)) by BVFUNC_1: 10

      .= ( I_el Y) by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:40

    ((((a 'imp' b) '&' a) '&' c) 'imp' b) = ( I_el Y)

    proof

      

      thus ((((a 'imp' b) '&' a) '&' c) 'imp' b) = ((((( 'not' a) 'or' b) '&' a) '&' c) 'imp' b) by BVFUNC_4: 8

      .= ((((( 'not' a) '&' a) 'or' (b '&' a)) '&' c) 'imp' b) by BVFUNC_1: 12

      .= (((( O_el Y) 'or' (b '&' a)) '&' c) 'imp' b) by BVFUNC_4: 5

      .= (((b '&' a) '&' c) 'imp' b) by BVFUNC_1: 9

      .= (( 'not' ((b '&' a) '&' c)) 'or' b) by BVFUNC_4: 8

      .= ((( 'not' (b '&' a)) 'or' ( 'not' c)) 'or' b) by BVFUNC_1: 14

      .= (((( 'not' b) 'or' ( 'not' a)) 'or' ( 'not' c)) 'or' b) by BVFUNC_1: 14

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

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

      .= ((( I_el Y) 'or' ( 'not' a)) 'or' ( 'not' c)) by BVFUNC_4: 6

      .= (( I_el Y) 'or' ( 'not' c)) by BVFUNC_1: 10

      .= ( I_el Y) by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:41

    ((b 'imp' c) 'imp' ((a '&' b) 'imp' c)) = ( I_el Y)

    proof

      

      thus ((b 'imp' c) 'imp' ((a '&' b) 'imp' c)) = (( 'not' (b 'imp' c)) 'or' ((a '&' b) 'imp' c)) by BVFUNC_4: 8

      .= (( 'not' (( 'not' b) 'or' c)) 'or' ((a '&' b) 'imp' c)) by BVFUNC_4: 8

      .= (( 'not' (( 'not' b) 'or' c)) 'or' (( 'not' (a '&' b)) 'or' c)) by BVFUNC_4: 8

      .= ((( 'not' ( 'not' b)) '&' ( 'not' c)) 'or' (( 'not' (a '&' b)) 'or' c)) by BVFUNC_1: 13

      .= ((b '&' ( 'not' c)) 'or' ((( 'not' a) 'or' ( 'not' b)) 'or' c)) by BVFUNC_1: 14

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

      .= (((b 'or' c) '&' (( 'not' c) 'or' c)) 'or' (( 'not' a) 'or' ( 'not' b))) by BVFUNC_1: 11

      .= (((b 'or' c) '&' ( I_el Y)) 'or' (( 'not' a) 'or' ( 'not' b))) by BVFUNC_4: 6

      .= ((( 'not' a) 'or' ( 'not' b)) 'or' (b 'or' c)) by BVFUNC_1: 6

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

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

      .= ((( 'not' a) 'or' ( I_el Y)) 'or' c) by BVFUNC_4: 6

      .= (( I_el Y) 'or' c) by BVFUNC_1: 10

      .= ( I_el Y) by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:42

    (((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b))) = ( I_el Y)

    proof

      (((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b))) = ((( 'not' (a '&' b)) 'or' c) 'imp' ((a '&' b) 'imp' (c '&' b))) by BVFUNC_4: 8

      .= (( 'not' (( 'not' (a '&' b)) 'or' c)) 'or' ((a '&' b) 'imp' (c '&' b))) by BVFUNC_4: 8

      .= (( 'not' (( 'not' (a '&' b)) 'or' c)) 'or' (( 'not' (a '&' b)) 'or' (c '&' b))) by BVFUNC_4: 8

      .= ((( 'not' ( 'not' (a '&' b))) '&' ( 'not' c)) 'or' (( 'not' (a '&' b)) 'or' (c '&' b))) by BVFUNC_1: 13

      .= (((a '&' b) '&' ( 'not' c)) 'or' ((( 'not' a) 'or' ( 'not' b)) 'or' (c '&' b))) by BVFUNC_1: 14

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

      .= (((a '&' b) '&' ( 'not' c)) 'or' (( 'not' a) 'or' ((( 'not' b) 'or' b) '&' (( 'not' b) 'or' c)))) by BVFUNC_1: 11

      .= (((a '&' b) '&' ( 'not' c)) 'or' (( 'not' a) 'or' (( I_el Y) '&' (( 'not' b) 'or' c)))) by BVFUNC_4: 6

      .= (((a '&' b) '&' ( 'not' c)) 'or' (( 'not' a) 'or' (( 'not' b) 'or' c))) by BVFUNC_1: 6

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

      .= ((((a '&' b) 'or' ( 'not' a)) '&' (( 'not' c) 'or' ( 'not' a))) 'or' (( 'not' b) 'or' c)) by BVFUNC_1: 11

      .= ((((a 'or' ( 'not' a)) '&' (b 'or' ( 'not' a))) '&' (( 'not' c) 'or' ( 'not' a))) 'or' (( 'not' b) 'or' c)) by BVFUNC_1: 11

      .= (((( I_el Y) '&' (b 'or' ( 'not' a))) '&' (( 'not' c) 'or' ( 'not' a))) 'or' (( 'not' b) 'or' c)) by BVFUNC_4: 6

      .= (((b 'or' ( 'not' a)) '&' (( 'not' c) 'or' ( 'not' a))) 'or' (( 'not' b) 'or' c)) by BVFUNC_1: 6

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

      .= ((((b 'or' ( 'not' a)) 'or' c) '&' ((( 'not' c) 'or' ( 'not' a)) 'or' c)) 'or' ( 'not' b)) by BVFUNC_1: 11

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

      .= ((((b 'or' ( 'not' a)) 'or' c) '&' (( 'not' a) 'or' ( I_el Y))) 'or' ( 'not' b)) by BVFUNC_4: 6

      .= ((((b 'or' ( 'not' a)) 'or' c) '&' ( I_el Y)) 'or' ( 'not' b)) by BVFUNC_1: 10

      .= (((b 'or' ( 'not' a)) 'or' c) 'or' ( 'not' b)) by BVFUNC_1: 6

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

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

      .= ((( I_el Y) 'or' ( 'not' a)) 'or' c) by BVFUNC_4: 6

      .= (( I_el Y) 'or' c) by BVFUNC_1: 10;

      hence thesis by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:43

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

    theorem :: BVFUNC25:44

    (((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c)) = ( I_el Y)

    proof

      (((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c)) = ((((a 'imp' b) '&' a) '&' c) 'imp' (b '&' c)) by BVFUNC_1: 4

      .= (((a '&' b) '&' c) 'imp' (b '&' c)) by BVFUNC_6: 56

      .= ((a '&' (b '&' c)) 'imp' (b '&' c)) by BVFUNC_1: 4;

      hence thesis by BVFUNC_6: 38;

    end;

    theorem :: BVFUNC25:45

    ((a '&' (a 'imp' b)) '&' (b 'imp' c)) '<' c

    proof

      (((a '&' (a 'imp' b)) '&' (b 'imp' c)) 'imp' c) = (( 'not' ((a '&' (a 'imp' b)) '&' (b 'imp' c))) 'or' c) by BVFUNC_4: 8

      .= (( 'not' ((a '&' b) '&' (b 'imp' c))) 'or' c) by BVFUNC_6: 56

      .= (( 'not' (a '&' (b '&' (b 'imp' c)))) 'or' c) by BVFUNC_1: 4

      .= (( 'not' (a '&' (b '&' c))) 'or' c) by BVFUNC_6: 56

      .= (( 'not' ((a '&' b) '&' c)) 'or' c) by BVFUNC_1: 4

      .= ((( 'not' (a '&' b)) 'or' ( 'not' c)) 'or' c) by BVFUNC_1: 14

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

      .= (( 'not' (a '&' b)) 'or' ( I_el Y)) by BVFUNC_4: 6

      .= ( I_el Y) by BVFUNC_1: 10;

      hence thesis by BVFUNC_1: 16;

    end;

    theorem :: BVFUNC25:46

    (((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c)) '<' (( 'not' a) 'imp' (b 'or' c))

    proof

      ((((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c)) 'imp' (( 'not' a) 'imp' (b 'or' c))) = (( 'not' (((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c))) 'or' (( 'not' a) 'imp' (b 'or' c))) by BVFUNC_4: 8

      .= (( 'not' (((a 'or' b) '&' (( 'not' a) 'or' c)) '&' (b 'imp' c))) 'or' (( 'not' a) 'imp' (b 'or' c))) by BVFUNC_4: 8

      .= (( 'not' (((a 'or' b) '&' (( 'not' a) 'or' c)) '&' (( 'not' b) 'or' c))) 'or' (( 'not' a) 'imp' (b 'or' c))) by BVFUNC_4: 8

      .= (( 'not' (((a 'or' b) '&' (( 'not' a) 'or' c)) '&' (( 'not' b) 'or' c))) 'or' (( 'not' ( 'not' a)) 'or' (b 'or' c))) by BVFUNC_4: 8

      .= ((( 'not' ((a 'or' b) '&' (( 'not' a) 'or' c))) 'or' ( 'not' (( 'not' b) 'or' c))) 'or' (( 'not' ( 'not' a)) 'or' (b 'or' c))) by BVFUNC_1: 14

      .= ((( 'not' ((a 'or' b) '&' (( 'not' a) 'or' c))) 'or' (( 'not' ( 'not' b)) '&' ( 'not' c))) 'or' (( 'not' ( 'not' a)) 'or' (b 'or' c))) by BVFUNC_1: 13

      .= (((( 'not' (a 'or' b)) 'or' ( 'not' (( 'not' a) 'or' c))) 'or' (b '&' ( 'not' c))) 'or' (( 'not' ( 'not' a)) 'or' (b 'or' c))) by BVFUNC_1: 14

      .= ((((( 'not' a) '&' ( 'not' b)) 'or' ( 'not' (( 'not' a) 'or' c))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_1: 13

      .= ((((( 'not' a) '&' ( 'not' b)) 'or' (( 'not' ( 'not' a)) '&' ( 'not' c))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_1: 13

      .= ((((( 'not' a) 'or' (a '&' ( 'not' c))) '&' (( 'not' b) 'or' (a '&' ( 'not' c)))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_1: 11

      .= (((((( 'not' a) 'or' a) '&' (( 'not' a) 'or' ( 'not' c))) '&' (( 'not' b) 'or' (a '&' ( 'not' c)))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_1: 11

      .= ((((( I_el Y) '&' (( 'not' a) 'or' ( 'not' c))) '&' (( 'not' b) 'or' (a '&' ( 'not' c)))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_4: 6

      .= ((((( 'not' a) 'or' ( 'not' c)) '&' (( 'not' b) 'or' (a '&' ( 'not' c)))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_1: 6

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' ((( 'not' a) 'or' ( 'not' c)) '&' (a '&' ( 'not' c)))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_1: 12

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' (((( 'not' a) 'or' ( 'not' c)) '&' a) '&' ( 'not' c))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_1: 4

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' (((( 'not' a) '&' a) 'or' (( 'not' c) '&' a)) '&' ( 'not' c))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_1: 12

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' ((( O_el Y) 'or' (( 'not' c) '&' a)) '&' ( 'not' c))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_4: 5

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' ((( 'not' c) '&' a) '&' ( 'not' c))) 'or' (b '&' ( 'not' c))) 'or' (a 'or' (b 'or' c))) by BVFUNC_1: 9

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

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

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

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

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' (b '&' ( 'not' c))) 'or' (((( 'not' c) '&' a) 'or' c) '&' (( 'not' c) 'or' c))) 'or' (a 'or' b)) by BVFUNC_1: 11

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' (b '&' ( 'not' c))) 'or' (((( 'not' c) '&' a) 'or' c) '&' ( I_el Y))) 'or' (a 'or' b)) by BVFUNC_4: 6

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' (b '&' ( 'not' c))) 'or' ((( 'not' c) '&' a) 'or' c)) 'or' (a 'or' b)) by BVFUNC_1: 6

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' (b '&' ( 'not' c))) 'or' ((( 'not' c) 'or' c) '&' (a 'or' c))) 'or' (a 'or' b)) by BVFUNC_1: 11

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' (b '&' ( 'not' c))) 'or' (( I_el Y) '&' (a 'or' c))) 'or' (a 'or' b)) by BVFUNC_4: 6

      .= (((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' (b '&' ( 'not' c))) 'or' (a 'or' c)) 'or' (a 'or' b)) by BVFUNC_1: 6

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

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

      .= ((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' (((b 'or' c) '&' (( 'not' c) 'or' c)) 'or' a)) 'or' (a 'or' b)) by BVFUNC_1: 11

      .= ((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' (((b 'or' c) '&' ( I_el Y)) 'or' a)) 'or' (a 'or' b)) by BVFUNC_4: 6

      .= ((((( 'not' a) 'or' ( 'not' c)) '&' ( 'not' b)) 'or' ((b 'or' c) 'or' a)) 'or' (a 'or' b)) by BVFUNC_1: 6

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

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

      .= (((((( 'not' a) 'or' ( 'not' c)) 'or' b) '&' (( 'not' b) 'or' b)) 'or' (c 'or' a)) 'or' (a 'or' b)) by BVFUNC_1: 11

      .= (((((( 'not' a) 'or' ( 'not' c)) 'or' b) '&' ( I_el Y)) 'or' (c 'or' a)) 'or' (a 'or' b)) by BVFUNC_4: 6

      .= ((((( 'not' a) 'or' ( 'not' c)) 'or' b) 'or' (c 'or' a)) 'or' (a 'or' b)) by BVFUNC_1: 6

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

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

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

      .= ((((( 'not' a) 'or' ( I_el Y)) 'or' b) 'or' a) 'or' (a 'or' b)) by BVFUNC_4: 6

      .= (((( I_el Y) 'or' b) 'or' a) 'or' (a 'or' b)) by BVFUNC_1: 10

      .= ((( I_el Y) 'or' a) 'or' (a 'or' b)) by BVFUNC_1: 10

      .= (( I_el Y) 'or' (a 'or' b)) by BVFUNC_1: 10

      .= ( I_el Y) by BVFUNC_1: 10;

      hence thesis by BVFUNC_1: 16;

    end;

    begin

    reserve Y for non empty set,

a,b,c for Function of Y, BOOLEAN ;

    definition

      let p,q be boolean-valued Function;

      :: BVFUNC25:def1

      func p 'nand' q -> Function means

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

      existence

      proof

        deffunc F( object) = ((p . $1) 'nand' (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) 'nand' (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) 'nand' (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) 'nand' (q . x)) by A3;

          hence thesis by A2, A4, A5, A6;

        end;

        hence thesis by A2, A4, FUNCT_1: 2;

      end;

      commutativity ;

      :: BVFUNC25:def2

      func p 'nor' q -> Function means

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

      existence

      proof

        deffunc F( object) = ((p . $1) 'nor' (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) 'nor' (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) 'nor' (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) 'nor' (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 'nand' q) -> boolean-valued;

      coherence

      proof

        let x be object;

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

        then

        consider y be object such that

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

        x = ((p . y) 'nand' (q . y)) by A1, Def1;

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

        hence thesis;

      end;

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

      coherence

      proof

        let x be object;

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

        then

        consider y be object such that

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

        x = ((p . y) 'nor' (q . y)) by A2, Def2;

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

      redefine

      :: BVFUNC25:def3

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

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

      coherence

      proof

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

        

        then

         A1: ( dom (p 'nand' q)) = (A /\ A) by Def1

        .= A;

        ( rng (p 'nand' 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 'nand' q);

          let x be Element of A;

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

          

          then ( dom (p 'nand' q)) = (A /\ A) by Def1

          .= A;

          hence (IT . x) = ((p . x) 'nand' (q . x)) by A3, Def1;

        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) 'nand' (q . x));

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

        hence thesis by A5, Def1;

      end;

      :: original: 'nor'

      redefine

      :: BVFUNC25:def4

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

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

      coherence

      proof

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

        

        then

         A6: ( dom (p 'nor' q)) = (A /\ A) by Def2

        .= A;

        ( rng (p 'nor' 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 'nor' q);

          let x be Element of A;

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

          

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

          .= A;

          hence (IT . x) = ((p . x) 'nor' (q . x)) by A8, Def2;

        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) 'nor' (q . x));

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

        hence thesis by A10, Def2;

      end;

    end

    definition

      let Y;

      let a,b be Function of Y, BOOLEAN ;

      :: original: 'nand'

      redefine

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

      coherence

      proof

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

        hence thesis;

      end;

      :: original: 'nor'

      redefine

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

      coherence

      proof

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

        hence thesis;

      end;

    end

    theorem :: BVFUNC25:47

    

     th1: (a 'nand' b) = ( 'not' (a '&' b))

    proof

      let x be Element of Y;

      

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

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

      .= ( 'not' ( 'not' ((a . x) 'nand' (b . x)))) by BVFUNC_1: 46

      .= ((a 'nand' b) . x) by Def3;

    end;

    theorem :: BVFUNC25:48

    

     Th2: (a 'nor' b) = ( 'not' (a 'or' b))

    proof

      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 BVFUNC_1:def 4

      .= ( 'not' ( 'not' ((a . x) 'nor' (b . x)))) by BVFUNC_1: 53

      .= ((a 'nor' b) . x) by Def4;

    end;

    theorem :: BVFUNC25:49

    

     Th3: (( I_el Y) 'nand' a) = ( 'not' a)

    proof

      (( I_el Y) 'nand' a) = ( 'not' (( I_el Y) '&' a)) by th1;

      hence thesis by BVFUNC_1: 6;

    end;

    theorem :: BVFUNC25:50

    

     Th4: (( O_el Y) 'nand' a) = ( I_el Y)

    proof

      (( O_el Y) 'nand' a) = ( 'not' (( O_el Y) '&' a)) & (( O_el Y) '&' a) = ( O_el Y) by th1, BVFUNC_1: 5;

      hence thesis by BVFUNC_1: 2;

    end;

    theorem :: BVFUNC25:51

    (( O_el Y) 'nand' ( O_el Y)) = ( I_el Y) & (( O_el Y) 'nand' ( I_el Y)) = ( I_el Y) & (( I_el Y) 'nand' ( I_el Y)) = ( O_el Y)

    proof

      thus (( O_el Y) 'nand' ( O_el Y)) = ( I_el Y) by Th4;

      thus (( O_el Y) 'nand' ( I_el Y)) = ( I_el Y) by Th4;

      

      thus (( I_el Y) 'nand' ( I_el Y)) = ( 'not' ( I_el Y)) by Th3

      .= ( O_el Y) by BVFUNC_1: 2;

    end;

    theorem :: BVFUNC25:52

    (a 'nand' a) = ( 'not' a) & ( 'not' (a 'nand' a)) = a

    proof

      (a 'nand' a) = ( 'not' (a '&' a)) by th1

      .= ( 'not' a);

      hence thesis;

    end;

    theorem :: BVFUNC25:53

    ( 'not' (a 'nand' b)) = (a '&' b)

    proof

      ( 'not' (a 'nand' b)) = ( 'not' ( 'not' (a '&' b))) by th1;

      hence thesis;

    end;

    theorem :: BVFUNC25:54

    (a 'nand' ( 'not' a)) = ( I_el Y) & ( 'not' (a 'nand' ( 'not' a))) = ( O_el Y)

    proof

      (a 'nand' ( 'not' a)) = ( 'not' (a '&' ( 'not' a))) by th1

      .= ( 'not' ( O_el Y)) by BVFUNC_4: 5

      .= ( I_el Y) by BVFUNC_1: 2;

      hence thesis by BVFUNC_1: 2;

    end;

    theorem :: BVFUNC25:55

    

     Th9: (a 'nand' (b '&' c)) = ( 'not' ((a '&' b) '&' c))

    proof

      (a 'nand' (b '&' c)) = ( 'not' (a '&' (b '&' c))) by th1;

      hence thesis by BVFUNC_1: 4;

    end;

    theorem :: BVFUNC25:56

    

     Th10: (a 'nand' (b '&' c)) = ((a '&' b) 'nand' c)

    proof

      ((a '&' b) 'nand' c) = ( 'not' ((a '&' b) '&' c)) by th1;

      hence thesis by Th9;

    end;

    theorem :: BVFUNC25:57

    

     th11: (a 'nand' (b 'or' c)) = (( 'not' (a '&' b)) '&' ( 'not' (a '&' c)))

    proof

      

      thus (a 'nand' (b 'or' c)) = ( 'not' (a '&' (b 'or' c))) by th1

      .= ( 'not' ((a '&' b) 'or' (a '&' c))) by BVFUNC_1: 12

      .= (( 'not' (a '&' b)) '&' ( 'not' (a '&' c))) by BVFUNC_1: 13;

    end;

    theorem :: BVFUNC25:58

    (a 'nand' (b 'xor' c)) = ((a '&' b) 'eqv' (a '&' c))

    proof

      

      thus (a 'nand' (b 'xor' c)) = ( 'not' (a '&' (b 'xor' c))) by th1

      .= ( 'not' ((a '&' b) 'xor' (a '&' c))) by Th11

      .= ( 'not' ( 'not' ((a '&' b) 'eqv' (a '&' c)))) by BVFUNC_6: 85

      .= ((a '&' b) 'eqv' (a '&' c));

    end;

    theorem :: BVFUNC25:59

    (a 'nand' (b 'nand' c)) = (( 'not' a) 'or' (b '&' c)) & (a 'nand' (b 'nand' c)) = (a 'imp' (b '&' c))

    proof

      (a 'nand' (b 'nand' c)) = ( 'not' (a '&' (b 'nand' c))) by th1

      .= ( 'not' (a '&' ( 'not' (b '&' c)))) by th1

      .= (( 'not' a) 'or' ( 'not' ( 'not' (b '&' c)))) by BVFUNC_1: 14

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

      hence thesis by BVFUNC_4: 8;

    end;

    theorem :: BVFUNC25:60

    (a 'nand' (b 'nor' c)) = ((( 'not' a) 'or' b) 'or' c) & (a 'nand' (b 'nor' c)) = (a 'imp' (b 'or' c))

    proof

      

       A1: (a 'nand' (b 'nor' c)) = ( 'not' (a '&' (b 'nor' c))) by th1

      .= ( 'not' (a '&' ( 'not' (b 'or' c)))) by Th2

      .= (( 'not' a) 'or' ( 'not' ( 'not' (b 'or' c)))) by BVFUNC_1: 14

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

      then (a 'nand' (b 'nor' c)) = (( 'not' a) 'or' (b 'or' c)) by BVFUNC_1: 8;

      hence thesis by A1, BVFUNC_4: 8;

    end;

    theorem :: BVFUNC25:61

    (a 'nand' (b 'eqv' c)) = (a 'imp' (b 'xor' c))

    proof

      (a 'nand' (b 'eqv' c)) = ( 'not' (a '&' (b 'eqv' c))) by th1

      .= (( 'not' a) 'or' ( 'not' (b 'eqv' c))) by BVFUNC_1: 14

      .= (( 'not' a) 'or' ( 'not' ( 'not' (b 'xor' c)))) by Th12

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

      hence thesis by BVFUNC_4: 8;

    end;

    theorem :: BVFUNC25:62

    (a 'nand' (a '&' b)) = (a 'nand' b)

    proof

      (a 'nand' (a '&' b)) = ((a '&' a) 'nand' b) by Th10;

      hence thesis;

    end;

    theorem :: BVFUNC25:63

    (a 'nand' (a 'or' b)) = (( 'not' a) '&' ( 'not' (a '&' b)))

    proof

      

      thus (a 'nand' (a 'or' b)) = (( 'not' (a '&' a)) '&' ( 'not' (a '&' b))) by th11

      .= (( 'not' a) '&' ( 'not' (a '&' b)));

    end;

    theorem :: BVFUNC25:64

    (a 'nand' (a 'eqv' b)) = (a 'imp' (a 'xor' b))

    proof

      (a 'nand' (a 'eqv' b)) = ( 'not' (a '&' (a 'eqv' b))) by th1

      .= (( 'not' a) 'or' ( 'not' (a 'eqv' b))) by BVFUNC_1: 14

      .= (( 'not' a) 'or' ( 'not' ( 'not' (a 'xor' b)))) by Th12

      .= (( 'not' a) 'or' (a 'xor' b));

      hence thesis by BVFUNC_4: 8;

    end;

    theorem :: BVFUNC25:65

    (a 'nand' (a 'nand' b)) = (( 'not' a) 'or' b) & (a 'nand' (a 'nand' b)) = (a 'imp' b)

    proof

      (a 'nand' (a 'nand' b)) = ( 'not' (a '&' (a 'nand' b))) by th1

      .= ( 'not' (a '&' ( 'not' (a '&' b)))) by th1

      .= (( 'not' a) 'or' ( 'not' ( 'not' (a '&' b)))) by BVFUNC_1: 14

      .= ((( 'not' a) 'or' a) '&' (( 'not' a) 'or' b)) by BVFUNC_1: 11

      .= (( I_el Y) '&' (( 'not' a) 'or' b)) by BVFUNC_4: 6

      .= (( 'not' a) 'or' b) by BVFUNC_1: 6;

      hence thesis by BVFUNC_4: 8;

    end;

    theorem :: BVFUNC25:66

    (a 'nand' (a 'nor' b)) = ( I_el Y)

    proof

      

      thus (a 'nand' (a 'nor' b)) = ( 'not' (a '&' (a 'nor' b))) by th1

      .= ( 'not' (a '&' ( 'not' (a 'or' b)))) by Th2

      .= (( 'not' a) 'or' ( 'not' ( 'not' (a 'or' b)))) by BVFUNC_1: 14

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

      .= (( I_el Y) 'or' b) by BVFUNC_4: 6

      .= ( I_el Y) by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:67

    (a 'nand' (a 'eqv' b)) = (( 'not' a) 'or' ( 'not' b))

    proof

      

      thus (a 'nand' (a 'eqv' b)) = ( 'not' (a '&' (a 'eqv' b))) by th1

      .= ( 'not' (a '&' ( 'not' (a 'xor' b)))) by Th12

      .= (( 'not' a) 'or' ( 'not' ( 'not' (a 'xor' b)))) by BVFUNC_1: 14

      .= (( 'not' a) 'or' ((a 'or' b) '&' (( 'not' a) 'or' ( 'not' b)))) by BVFUNC_6: 86

      .= ((( 'not' a) 'or' (a 'or' b)) '&' (( 'not' a) 'or' (( 'not' a) 'or' ( 'not' b)))) by BVFUNC_1: 11

      .= (((( 'not' a) 'or' a) 'or' b) '&' (( 'not' a) 'or' (( 'not' a) 'or' ( 'not' b)))) by BVFUNC_1: 8

      .= ((( I_el Y) 'or' b) '&' (( 'not' a) 'or' (( 'not' a) 'or' ( 'not' b)))) by BVFUNC_4: 6

      .= (( I_el Y) '&' (( 'not' a) 'or' (( 'not' a) 'or' ( 'not' b)))) by BVFUNC_1: 10

      .= (( 'not' a) 'or' (( 'not' a) 'or' ( 'not' b))) by BVFUNC_1: 6

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

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

    end;

    theorem :: BVFUNC25:68

    (a '&' b) = ((a 'nand' b) 'nand' (a 'nand' b))

    proof

      

      thus ((a 'nand' b) 'nand' (a 'nand' b)) = ( 'not' ((a 'nand' b) '&' (a 'nand' b))) by th1

      .= ((a '&' b) 'or' ( 'not' ( 'not' (a '&' b)))) by th1

      .= (a '&' b);

    end;

    theorem :: BVFUNC25:69

    ((a 'nand' b) 'nand' (a 'nand' c)) = (a '&' (b 'or' c))

    proof

      

      thus ((a 'nand' b) 'nand' (a 'nand' c)) = ( 'not' ((a 'nand' b) '&' (a 'nand' c))) by th1

      .= ( 'not' (( 'not' (a '&' b)) '&' (a 'nand' c))) by th1

      .= ( 'not' (( 'not' (a '&' b)) '&' ( 'not' (a '&' c)))) by th1

      .= (( 'not' ( 'not' (a '&' b))) 'or' ( 'not' ( 'not' (a '&' c)))) by BVFUNC_1: 14

      .= (a '&' (b 'or' c)) by BVFUNC_1: 12;

    end;

    theorem :: BVFUNC25:70

    

     Th24: (a 'nand' (b 'imp' c)) = ((( 'not' a) 'or' b) '&' ( 'not' (a '&' c)))

    proof

      

      thus (a 'nand' (b 'imp' c)) = ( 'not' (a '&' (b 'imp' c))) by th1

      .= ( 'not' (a '&' (( 'not' b) 'or' c))) by BVFUNC_4: 8

      .= ( 'not' ((a '&' ( 'not' b)) 'or' (a '&' c))) by BVFUNC_1: 12

      .= (( 'not' (a '&' ( 'not' b))) '&' ( 'not' (a '&' c))) by BVFUNC_1: 13

      .= ((( 'not' a) 'or' ( 'not' ( 'not' b))) '&' ( 'not' (a '&' c))) by BVFUNC_1: 14

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

    end;

    theorem :: BVFUNC25:71

    (a 'nand' (a 'imp' b)) = ( 'not' (a '&' b))

    proof

      

      thus (a 'nand' (a 'imp' b)) = ((( 'not' a) 'or' a) '&' ( 'not' (a '&' b))) by Th24

      .= (( I_el Y) '&' ( 'not' (a '&' b))) by BVFUNC_4: 6

      .= ( 'not' (a '&' b)) by BVFUNC_1: 6;

    end;

    theorem :: BVFUNC25:72

    

     Th26: (( I_el Y) 'nor' a) = ( O_el Y)

    proof

      

      thus (( I_el Y) 'nor' a) = ( 'not' (( I_el Y) 'or' a)) by Th2

      .= ( 'not' ( I_el Y)) by BVFUNC_1: 10

      .= ( O_el Y) by BVFUNC_1: 2;

    end;

    theorem :: BVFUNC25:73

    

     Th27: (( O_el Y) 'nor' a) = ( 'not' a)

    proof

      

      thus (( O_el Y) 'nor' a) = ( 'not' (( O_el Y) 'or' a)) by Th2

      .= ( 'not' a) by BVFUNC_1: 9;

    end;

    theorem :: BVFUNC25:74

    (( O_el Y) 'nor' ( O_el Y)) = ( I_el Y) & (( O_el Y) 'nor' ( I_el Y)) = ( O_el Y) & (( I_el Y) 'nor' ( I_el Y)) = ( O_el Y)

    proof

      

      thus (( O_el Y) 'nor' ( O_el Y)) = ( 'not' ( O_el Y)) by Th27

      .= ( I_el Y) by BVFUNC_1: 2;

      thus (( O_el Y) 'nor' ( I_el Y)) = ( O_el Y) by Th26;

      thus thesis by Th26;

    end;

    theorem :: BVFUNC25:75

    (a 'nor' a) = ( 'not' a) & ( 'not' (a 'nor' a)) = a

    proof

      (a 'nor' a) = ( 'not' (a 'or' a)) by Th2

      .= ( 'not' a);

      hence thesis;

    end;

    theorem :: BVFUNC25:76

    ( 'not' (a 'nor' b)) = (a 'or' b)

    proof

      ( 'not' (a 'nor' b)) = ( 'not' ( 'not' (a 'or' b))) by Th2;

      hence thesis;

    end;

    theorem :: BVFUNC25:77

    (a 'nor' ( 'not' a)) = ( O_el Y) & ( 'not' (a 'nor' ( 'not' a))) = ( I_el Y)

    proof

      (a 'nor' ( 'not' a)) = ( 'not' (a 'or' ( 'not' a))) by Th2

      .= ( 'not' ( I_el Y)) by BVFUNC_4: 6

      .= ( O_el Y) by BVFUNC_1: 2;

      hence thesis by BVFUNC_1: 2;

    end;

    theorem :: BVFUNC25:78

    (( 'not' a) '&' (a 'xor' b)) = (( 'not' a) '&' b)

    proof

      

      thus (( 'not' a) '&' (a 'xor' b)) = (( 'not' a) '&' ((( 'not' a) '&' b) 'or' (a '&' ( 'not' b)))) by BVFUNC_4: 9

      .= ((( 'not' a) '&' (( 'not' a) '&' b)) 'or' (( 'not' a) '&' (a '&' ( 'not' b)))) by BVFUNC_1: 12

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

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

      .= ((( 'not' a) '&' b) 'or' (( O_el Y) '&' ( 'not' b))) by BVFUNC_4: 5

      .= ((( 'not' a) '&' b) 'or' ( O_el Y)) by BVFUNC_1: 5

      .= (( 'not' a) '&' b) by BVFUNC_1: 9;

    end;

    theorem :: BVFUNC25:79

    

     Th33: (a 'nor' (b '&' c)) = (( 'not' (a 'or' b)) 'or' ( 'not' (a 'or' c)))

    proof

      (a 'nor' (b '&' c)) = ( 'not' (a 'or' (b '&' c))) by Th2

      .= ( 'not' ((a 'or' b) '&' (a 'or' c))) by BVFUNC_1: 11;

      hence thesis by BVFUNC_1: 14;

    end;

    theorem :: BVFUNC25:80

    

     Th34: (a 'nor' (b 'or' c)) = ( 'not' ((a 'or' b) 'or' c))

    proof

      

      thus (a 'nor' (b 'or' c)) = ( 'not' (a 'or' (b 'or' c))) by Th2

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

    end;

    theorem :: BVFUNC25:81

    

     Th35: (a 'nor' (b 'eqv' c)) = (( 'not' a) '&' (b 'xor' c))

    proof

      

      thus (a 'nor' (b 'eqv' c)) = ( 'not' (a 'or' (b 'eqv' c))) by Th2

      .= (( 'not' a) '&' ( 'not' (b 'eqv' c))) by BVFUNC_1: 13

      .= (( 'not' a) '&' ( 'not' ( 'not' (b 'xor' c)))) by Th12

      .= (( 'not' a) '&' (b 'xor' c));

    end;

    theorem :: BVFUNC25:82

    

     Th36: (a 'nor' (b 'imp' c)) = ((( 'not' a) '&' b) '&' ( 'not' c))

    proof

      

      thus (a 'nor' (b 'imp' c)) = ( 'not' (a 'or' (b 'imp' c))) by Th2

      .= (( 'not' a) '&' ( 'not' (b 'imp' c))) by BVFUNC_1: 13

      .= (( 'not' a) '&' (b '&' ( 'not' c))) by Th1

      .= ((( 'not' a) '&' b) '&' ( 'not' c)) by BVFUNC_1: 4;

    end;

    theorem :: BVFUNC25:83

    

     Th37: (a 'nor' (b 'nand' c)) = ((( 'not' a) '&' b) '&' c)

    proof

      

      thus (a 'nor' (b 'nand' c)) = ( 'not' (a 'or' (b 'nand' c))) by Th2

      .= ( 'not' (a 'or' ( 'not' (b '&' c)))) by th1

      .= (( 'not' a) '&' ( 'not' ( 'not' (b '&' c)))) by BVFUNC_1: 13

      .= ((( 'not' a) '&' b) '&' c) by BVFUNC_1: 4;

    end;

    theorem :: BVFUNC25:84

    

     Th38: (a 'nor' (b 'nor' c)) = (( 'not' a) '&' (b 'or' c))

    proof

      

      thus (a 'nor' (b 'nor' c)) = ( 'not' (a 'or' (b 'nor' c))) by Th2

      .= ( 'not' (a 'or' ( 'not' (b 'or' c)))) by Th2

      .= (( 'not' a) '&' ( 'not' ( 'not' (b 'or' c)))) by BVFUNC_1: 13

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

    end;

    theorem :: BVFUNC25:85

    (a 'nor' (a '&' b)) = ( 'not' (a '&' (a 'or' b)))

    proof

      

      thus (a 'nor' (a '&' b)) = (( 'not' (a 'or' a)) 'or' ( 'not' (a 'or' b))) by Th33

      .= ( 'not' (a '&' (a 'or' b))) by BVFUNC_1: 14;

    end;

    theorem :: BVFUNC25:86

    (a 'nor' (a 'or' b)) = ( 'not' (a 'or' b))

    proof

      

      thus (a 'nor' (a 'or' b)) = ( 'not' ((a 'or' a) 'or' b)) by Th34

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

    end;

    theorem :: BVFUNC25:87

    (a 'nor' (a 'eqv' b)) = (( 'not' a) '&' b)

    proof

      

      thus (a 'nor' (a 'eqv' b)) = (( 'not' a) '&' (a 'xor' b)) by Th35

      .= (( 'not' a) '&' ((( 'not' a) '&' b) 'or' (a '&' ( 'not' b)))) by BVFUNC_4: 9

      .= ((( 'not' a) '&' (( 'not' a) '&' b)) 'or' (( 'not' a) '&' (a '&' ( 'not' b)))) by BVFUNC_1: 12

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

      .= ((( 'not' a) '&' (( 'not' a) '&' b)) 'or' (( O_el Y) '&' ( 'not' b))) by BVFUNC_4: 5

      .= ((( 'not' a) '&' (( 'not' a) '&' b)) 'or' ( O_el Y)) by BVFUNC_1: 5

      .= (( 'not' a) '&' (( 'not' a) '&' b)) by BVFUNC_1: 9

      .= ((( 'not' a) '&' ( 'not' a)) '&' b) by BVFUNC_1: 4

      .= (( 'not' a) '&' b);

    end;

    theorem :: BVFUNC25:88

    (a 'nor' (a 'imp' b)) = ( O_el Y)

    proof

      

      thus (a 'nor' (a 'imp' b)) = ((( 'not' a) '&' a) '&' ( 'not' b)) by Th36

      .= (( O_el Y) '&' ( 'not' b)) by BVFUNC_4: 5

      .= ( O_el Y) by BVFUNC_1: 5;

    end;

    theorem :: BVFUNC25:89

    (a 'nor' (a 'nand' b)) = ( O_el Y)

    proof

      

      thus (a 'nor' (a 'nand' b)) = ((( 'not' a) '&' a) '&' b) by Th37

      .= (( O_el Y) '&' b) by BVFUNC_4: 5

      .= ( O_el Y) by BVFUNC_1: 5;

    end;

    theorem :: BVFUNC25:90

    (a 'nor' (a 'nor' b)) = (( 'not' a) '&' b)

    proof

      

      thus (a 'nor' (a 'nor' b)) = (( 'not' a) '&' (a 'or' b)) by Th38

      .= ((( 'not' a) '&' a) 'or' (( 'not' a) '&' b)) by BVFUNC_1: 12

      .= (( O_el Y) 'or' (( 'not' a) '&' b)) by BVFUNC_4: 5

      .= (( 'not' a) '&' b) by BVFUNC_1: 9;

    end;

    theorem :: BVFUNC25:91

    (( O_el Y) 'eqv' ( O_el Y)) = ( I_el Y)

    proof

      

      thus (( O_el Y) 'eqv' ( O_el Y)) = ( 'not' (( O_el Y) 'xor' ( O_el Y))) by Th12

      .= ( 'not' ( O_el Y)) by Th13

      .= ( I_el Y) by BVFUNC_1: 2;

    end;

    theorem :: BVFUNC25:92

    (( O_el Y) 'eqv' ( I_el Y)) = ( O_el Y)

    proof

      

      thus (( O_el Y) 'eqv' ( I_el Y)) = ( 'not' (( O_el Y) 'xor' ( I_el Y))) by Th12

      .= ( 'not' (( O_el Y) 'xor' ( 'not' ( O_el Y)))) by BVFUNC_1: 2

      .= ( 'not' ( I_el Y)) by Th14

      .= ( O_el Y) by BVFUNC_1: 2;

    end;

    theorem :: BVFUNC25:93

    (( I_el Y) 'eqv' ( I_el Y)) = ( I_el Y)

    proof

      

      thus (( I_el Y) 'eqv' ( I_el Y)) = ( 'not' (( I_el Y) 'xor' ( I_el Y))) by Th12

      .= ( 'not' ( 'not' ( I_el Y))) by BVFUNC_6: 87

      .= ( I_el Y);

    end;

    theorem :: BVFUNC25:94

    (a 'eqv' a) = ( I_el Y) & ( 'not' (a 'eqv' a)) = ( O_el Y)

    proof

      (a 'eqv' a) = ( 'not' (a 'xor' a)) by Th12

      .= ( 'not' ( O_el Y)) by Th13

      .= ( I_el Y) by BVFUNC_1: 2;

      hence thesis by BVFUNC_1: 2;

    end;

    theorem :: BVFUNC25:95

    (a 'eqv' (a 'or' b)) = (a 'or' ( 'not' b))

    proof

      

      thus (a 'eqv' (a 'or' b)) = ( 'not' (a 'xor' (a 'or' b))) by Th12

      .= ( 'not' ((( 'not' a) '&' (a 'or' b)) 'or' (a '&' ( 'not' (a 'or' b))))) by BVFUNC_4: 9

      .= ( 'not' (((( 'not' a) '&' a) 'or' (( 'not' a) '&' b)) 'or' (a '&' ( 'not' (a 'or' b))))) by BVFUNC_1: 12

      .= ( 'not' ((( O_el Y) 'or' (( 'not' a) '&' b)) 'or' (a '&' ( 'not' (a 'or' b))))) by BVFUNC_4: 5

      .= ( 'not' ((( 'not' a) '&' b) 'or' (a '&' ( 'not' (a 'or' b))))) by BVFUNC_1: 9

      .= ( 'not' ((( 'not' a) '&' b) 'or' (a '&' (( 'not' a) '&' ( 'not' b))))) by BVFUNC_1: 13

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

      .= ( 'not' ((( 'not' a) '&' b) 'or' (( O_el Y) '&' ( 'not' b)))) by BVFUNC_4: 5

      .= ( 'not' ((( 'not' a) '&' b) 'or' ( O_el Y))) by BVFUNC_1: 5

      .= ( 'not' (( 'not' a) '&' b)) by BVFUNC_1: 9

      .= (( 'not' ( 'not' a)) 'or' ( 'not' b)) by BVFUNC_1: 14

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

    end;

    theorem :: BVFUNC25:96

    

     Th50: (a '&' (b 'nand' c)) = ((a '&' ( 'not' b)) 'or' (a '&' ( 'not' c)))

    proof

      

      thus (a '&' (b 'nand' c)) = (a '&' ( 'not' (b '&' c))) by th1

      .= (a '&' (( 'not' b) 'or' ( 'not' c))) by BVFUNC_1: 14

      .= ((a '&' ( 'not' b)) 'or' (a '&' ( 'not' c))) by BVFUNC_1: 12;

    end;

    theorem :: BVFUNC25:97

    

     Th51: (a 'or' (b 'nand' c)) = ((a 'or' ( 'not' b)) 'or' ( 'not' c))

    proof

      

      thus (a 'or' (b 'nand' c)) = (a 'or' ( 'not' (b '&' c))) by th1

      .= (a 'or' (( 'not' b) 'or' ( 'not' c))) by BVFUNC_1: 14

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

    end;

    theorem :: BVFUNC25:98

    

     Th52: (a 'xor' (b 'nand' c)) = ((( 'not' a) '&' ( 'not' (b '&' c))) 'or' ((a '&' b) '&' c))

    proof

      

      thus (a 'xor' (b 'nand' c)) = (a 'xor' ( 'not' (b '&' c))) by th1

      .= ((( 'not' a) '&' ( 'not' (b '&' c))) 'or' (a '&' ( 'not' ( 'not' (b '&' c))))) by BVFUNC_4: 9

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

    end;

    theorem :: BVFUNC25:99

    

     Th53: (a 'eqv' (b 'nand' c)) = ((a '&' ( 'not' (b '&' c))) 'or' ((( 'not' a) '&' b) '&' c))

    proof

      

      thus (a 'eqv' (b 'nand' c)) = (a 'eqv' ( 'not' (b '&' c))) by th1

      .= ((a '&' ( 'not' (b '&' c))) 'or' (( 'not' a) '&' ( 'not' ( 'not' (b '&' c))))) by BVFUNC_6: 92

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

    end;

    theorem :: BVFUNC25:100

    

     Th54: (a 'imp' (b 'nand' c)) = ( 'not' ((a '&' b) '&' c))

    proof

      

      thus (a 'imp' (b 'nand' c)) = (a 'imp' ( 'not' (b '&' c))) by th1

      .= (( 'not' a) 'or' ( 'not' (b '&' c))) by BVFUNC_4: 8

      .= ( 'not' (a '&' (b '&' c))) by BVFUNC_1: 14

      .= ( 'not' ((a '&' b) '&' c)) by BVFUNC_1: 4;

    end;

    theorem :: BVFUNC25:101

    (a 'nor' (b 'nand' c)) = ( 'not' ((a 'or' ( 'not' b)) 'or' ( 'not' c)))

    proof

      

      thus (a 'nor' (b 'nand' c)) = (a 'nor' ( 'not' (b '&' c))) by th1

      .= ( 'not' (a 'or' ( 'not' (b '&' c)))) by Th2

      .= ( 'not' (a 'or' (( 'not' b) 'or' ( 'not' c)))) by BVFUNC_1: 14

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

    end;

    theorem :: BVFUNC25:102

    (a '&' (a 'nand' b)) = (a '&' ( 'not' b))

    proof

      

      thus (a '&' (a 'nand' b)) = ((a '&' ( 'not' a)) 'or' (a '&' ( 'not' b))) by Th50

      .= (( O_el Y) 'or' (a '&' ( 'not' b))) by BVFUNC_4: 5

      .= (a '&' ( 'not' b)) by BVFUNC_1: 9;

    end;

    theorem :: BVFUNC25:103

    (a 'or' (a 'nand' b)) = ( I_el Y)

    proof

      

      thus (a 'or' (a 'nand' b)) = ((a 'or' ( 'not' a)) 'or' ( 'not' b)) by Th51

      .= (( I_el Y) 'or' ( 'not' b)) by BVFUNC_4: 6

      .= ( I_el Y) by BVFUNC_1: 10;

    end;

    theorem :: BVFUNC25:104

    (a 'xor' (a 'nand' b)) = (( 'not' a) 'or' b)

    proof

      

      thus (a 'xor' (a 'nand' b)) = ((( 'not' a) '&' ( 'not' (a '&' b))) 'or' ((a '&' a) '&' b)) by Th52

      .= ((( 'not' a) 'or' (a '&' b)) '&' (( 'not' (a '&' b)) 'or' (a '&' b))) by BVFUNC_1: 11

      .= ((( 'not' a) 'or' (a '&' b)) '&' ( I_el Y)) by BVFUNC_4: 6

      .= (( 'not' a) 'or' (a '&' b)) by BVFUNC_1: 6

      .= ((( 'not' a) 'or' a) '&' (( 'not' a) 'or' b)) by BVFUNC_1: 11

      .= (( I_el Y) '&' (( 'not' a) 'or' b)) by BVFUNC_4: 6

      .= (( 'not' a) 'or' b) by BVFUNC_1: 6;

    end;

    theorem :: BVFUNC25:105

    (a 'eqv' (a 'nand' b)) = (a '&' ( 'not' b))

    proof

      

      thus (a 'eqv' (a 'nand' b)) = ((a '&' ( 'not' (a '&' b))) 'or' ((( 'not' a) '&' a) '&' b)) by Th53

      .= ((a '&' ( 'not' (a '&' b))) 'or' (( O_el Y) '&' b)) by BVFUNC_4: 5

      .= ((a '&' ( 'not' (a '&' b))) 'or' ( O_el Y)) by BVFUNC_1: 5

      .= (a '&' ( 'not' (a '&' b))) by BVFUNC_1: 9

      .= (a '&' (( 'not' a) 'or' ( 'not' b))) by BVFUNC_1: 14

      .= ((a '&' ( 'not' a)) 'or' (a '&' ( 'not' b))) by BVFUNC_1: 12

      .= (( O_el Y) 'or' (a '&' ( 'not' b))) by BVFUNC_4: 5

      .= (a '&' ( 'not' b)) by BVFUNC_1: 9;

    end;

    theorem :: BVFUNC25:106

    (a 'imp' (a 'nand' b)) = ( 'not' (a '&' b))

    proof

      

      thus (a 'imp' (a 'nand' b)) = ( 'not' ((a '&' a) '&' b)) by Th54

      .= ( 'not' (a '&' b));

    end;

    theorem :: BVFUNC25:107

    

     Th61: (a '&' (b 'nor' c)) = ((a '&' ( 'not' b)) '&' ( 'not' c))

    proof

      

      thus (a '&' (b 'nor' c)) = (a '&' ( 'not' (b 'or' c))) by Th2

      .= (a '&' (( 'not' b) '&' ( 'not' c))) by BVFUNC_1: 13

      .= ((a '&' ( 'not' b)) '&' ( 'not' c)) by BVFUNC_1: 4;

    end;

    theorem :: BVFUNC25:108

    

     Th62: (a 'or' (b 'nor' c)) = ((a 'or' ( 'not' b)) '&' (a 'or' ( 'not' c)))

    proof

      

      thus (a 'or' (b 'nor' c)) = (a 'or' ( 'not' (b 'or' c))) by Th2

      .= (a 'or' (( 'not' b) '&' ( 'not' c))) by BVFUNC_1: 13

      .= ((a 'or' ( 'not' b)) '&' (a 'or' ( 'not' c))) by BVFUNC_1: 11;

    end;

    theorem :: BVFUNC25:109

    

     Th63: (a 'xor' (b 'nor' c)) = ((a 'or' ( 'not' (b 'or' c))) '&' ((( 'not' a) 'or' b) 'or' c))

    proof

      

      thus (a 'xor' (b 'nor' c)) = (a 'xor' ( 'not' (b 'or' c))) by Th2

      .= ((a 'or' ( 'not' (b 'or' c))) '&' (( 'not' a) 'or' ( 'not' ( 'not' (b 'or' c))))) by BVFUNC_6: 86

      .= ((a 'or' ( 'not' (b 'or' c))) '&' ((( 'not' a) 'or' b) 'or' c)) by BVFUNC_1: 8;

    end;

    theorem :: BVFUNC25:110

    

     Th64: (a 'eqv' (b 'nor' c)) = (((a 'or' b) 'or' c) '&' (( 'not' a) 'or' ( 'not' (b 'or' c))))

    proof

      

      thus (a 'eqv' (b 'nor' c)) = (a 'eqv' ( 'not' (b 'or' c))) by Th2

      .= ((a 'or' ( 'not' ( 'not' (b 'or' c)))) '&' (( 'not' a) 'or' ( 'not' (b 'or' c)))) by BVFUNC_6: 91

      .= (((a 'or' b) 'or' c) '&' (( 'not' a) 'or' ( 'not' (b 'or' c)))) by BVFUNC_1: 8;

    end;

    theorem :: BVFUNC25:111

    

     Th65: (a 'imp' (b 'nor' c)) = ( 'not' (a '&' (b 'or' c)))

    proof

      

      thus (a 'imp' (b 'nor' c)) = (a 'imp' ( 'not' (b 'or' c))) by Th2

      .= (( 'not' a) 'or' ( 'not' (b 'or' c))) by BVFUNC_4: 8

      .= ( 'not' (a '&' (b 'or' c))) by BVFUNC_1: 14;

    end;

    theorem :: BVFUNC25:112

    (a 'nand' (b 'nor' c)) = ((( 'not' a) 'or' b) 'or' c)

    proof

      

      thus (a 'nand' (b 'nor' c)) = (a 'nand' ( 'not' (b 'or' c))) by Th2

      .= ( 'not' (a '&' ( 'not' (b 'or' c)))) by th1

      .= (( 'not' a) 'or' ( 'not' ( 'not' (b 'or' c)))) by BVFUNC_1: 14

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

    end;

    theorem :: BVFUNC25:113

    (a '&' (a 'nor' b)) = ( O_el Y)

    proof

      

      thus (a '&' (a 'nor' b)) = ((a '&' ( 'not' a)) '&' ( 'not' b)) by Th61

      .= (( O_el Y) '&' ( 'not' b)) by BVFUNC_4: 5

      .= ( O_el Y) by BVFUNC_1: 5;

    end;

    theorem :: BVFUNC25:114

    (a 'or' (a 'nor' b)) = (a 'or' ( 'not' b))

    proof

      

      thus (a 'or' (a 'nor' b)) = ((a 'or' ( 'not' a)) '&' (a 'or' ( 'not' b))) by Th62

      .= (( I_el Y) '&' (a 'or' ( 'not' b))) by BVFUNC_4: 6

      .= (a 'or' ( 'not' b)) by BVFUNC_1: 6;

    end;

    theorem :: BVFUNC25:115

    (a 'xor' (a 'nor' b)) = (a 'or' ( 'not' b))

    proof

      

      thus (a 'xor' (a 'nor' b)) = ((a 'or' ( 'not' (a 'or' b))) '&' ((( 'not' a) 'or' a) 'or' b)) by Th63

      .= ((a 'or' ( 'not' (a 'or' b))) '&' (( I_el Y) 'or' b)) by BVFUNC_4: 6

      .= ((a 'or' ( 'not' (a 'or' b))) '&' ( I_el Y)) by BVFUNC_1: 10

      .= (a 'or' ( 'not' (a 'or' b))) by BVFUNC_1: 6

      .= (a 'or' (( 'not' a) '&' ( 'not' b))) by BVFUNC_1: 13

      .= ((a 'or' ( 'not' a)) '&' (a 'or' ( 'not' b))) by BVFUNC_1: 11

      .= (( I_el Y) '&' (a 'or' ( 'not' b))) by BVFUNC_4: 6

      .= (a 'or' ( 'not' b)) by BVFUNC_1: 6;

    end;

    theorem :: BVFUNC25:116

    (a 'eqv' (a 'nor' b)) = (( 'not' a) '&' b)

    proof

      

      thus (a 'eqv' (a 'nor' b)) = (((a 'or' a) 'or' b) '&' (( 'not' a) 'or' ( 'not' (a 'or' b)))) by Th64

      .= (((a 'or' b) '&' ( 'not' a)) 'or' ((a 'or' b) '&' ( 'not' (a 'or' b)))) by BVFUNC_1: 12

      .= (((a 'or' b) '&' ( 'not' a)) 'or' ( O_el Y)) by BVFUNC_4: 5

      .= ((a 'or' b) '&' ( 'not' a)) by BVFUNC_1: 9

      .= ((a '&' ( 'not' a)) 'or' (b '&' ( 'not' a))) by BVFUNC_1: 12

      .= (( O_el Y) 'or' (b '&' ( 'not' a))) by BVFUNC_4: 5

      .= (( 'not' a) '&' b) by BVFUNC_1: 9;

    end;

    theorem :: BVFUNC25:117

    (a 'imp' (a 'nor' b)) = ( 'not' (a 'or' (a '&' b)))

    proof

      

      thus (a 'imp' (a 'nor' b)) = ( 'not' (a '&' (a 'or' b))) by Th65

      .= ( 'not' ((a '&' a) 'or' (a '&' b))) by BVFUNC_1: 12

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

    end;