boolealg.miz



    begin

    reserve L for Lattice;

    reserve X,Y,Z,V for Element of L;

    definition

      let L, X, Y;

      :: BOOLEALG:def1

      func X \ Y -> Element of L equals (X "/\" (Y ` ));

      coherence ;

    end

    definition

      let L, X, Y;

      :: BOOLEALG:def2

      func X \+\ Y -> Element of L equals ((X \ Y) "\/" (Y \ X));

      coherence ;

    end

    definition

      let L, X, Y;

      :: original: =

      redefine

      :: BOOLEALG:def3

      pred X = Y means X [= Y & Y [= X;

      compatibility by LATTICES: 8;

    end

    definition

      let L, X, Y;

      :: BOOLEALG:def4

      pred X meets Y means (X "/\" Y) <> ( Bottom L);

    end

    notation

      let L, X, Y;

      antonym X misses Y for X meets Y;

    end

    theorem :: BOOLEALG:1

    (X "\/" Y) [= Z implies X [= Z

    proof

      assume (X "\/" Y) [= Z;

      then (X "/\" (X "\/" Y)) [= (X "/\" Z) by LATTICES: 9;

      then

       A1: X [= (X "/\" Z) by LATTICES:def 9;

      (X "/\" Z) [= Z by LATTICES: 6;

      hence thesis by A1, LATTICES: 7;

    end;

    theorem :: BOOLEALG:2

    (X "/\" Y) [= (X "\/" Z)

    proof

      (X "/\" Y) [= X & X [= (X "\/" Z) by LATTICES: 5, LATTICES: 6;

      hence thesis by LATTICES: 7;

    end;

    theorem :: BOOLEALG:3

    X [= Z implies (X \ Y) [= Z

    proof

      assume X [= Z;

      then

       A1: (X "/\" (Y ` )) [= (Z "/\" (Y ` )) by LATTICES: 9;

      (Z "/\" (Y ` )) [= Z by LATTICES: 6;

      hence thesis by A1, LATTICES: 7;

    end;

    theorem :: BOOLEALG:4

    (X \ Y) [= Z & (Y \ X) [= Z implies (X \+\ Y) [= Z by FILTER_0: 6;

    theorem :: BOOLEALG:5

    X = (Y "\/" Z) iff Y [= X & Z [= X & for V st Y [= V & Z [= V holds X [= V

    proof

      thus X = (Y "\/" Z) implies Y [= X & Z [= X & for V st Y [= V & Z [= V holds X [= V by FILTER_0: 6, LATTICES: 5;

      assume that

       A1: Y [= X & Z [= X and

       A2: for V st Y [= V & Z [= V holds X [= V;

      

       A3: (Y "\/" Z) [= X by A1, FILTER_0: 6;

      Y [= (Y "\/" Z) & Z [= (Y "\/" Z) by LATTICES: 5;

      then X [= (Y "\/" Z) by A2;

      hence thesis by A3;

    end;

    theorem :: BOOLEALG:6

    X = (Y "/\" Z) iff X [= Y & X [= Z & for V st V [= Y & V [= Z holds V [= X

    proof

      thus X = (Y "/\" Z) implies X [= Y & X [= Z & for V st V [= Y & V [= Z holds V [= X by FILTER_0: 7, LATTICES: 6;

      assume that

       A1: X [= Y & X [= Z and

       A2: for V st V [= Y & V [= Z holds V [= X;

      

       A3: X [= (Y "/\" Z) by A1, FILTER_0: 7;

      (Y "/\" Z) [= Y & (Y "/\" Z) [= Z by LATTICES: 6;

      then (Y "/\" Z) [= X by A2;

      hence thesis by A3;

    end;

    theorem :: BOOLEALG:7

    X meets X iff X <> ( Bottom L);

    definition

      let L, X, Y;

      :: original: meets

      redefine

      pred X meets Y;

      symmetry ;

      :: original: \+\

      redefine

      func X \+\ Y;

      commutativity ;

      :: original: misses

      redefine

      pred X misses Y;

      symmetry ;

    end

    begin

    begin

    reserve L for D_Lattice;

    reserve X,Y,Z for Element of L;

    theorem :: BOOLEALG:8

    ((X "/\" Y) "\/" (X "/\" Z)) = X implies X [= (Y "\/" Z)

    proof

      assume ((X "/\" Y) "\/" (X "/\" Z)) = X;

      then (X "/\" (Y "\/" Z)) = X by LATTICES:def 11;

      hence thesis by LATTICES: 4;

    end;

    begin

    reserve L for 0_Lattice;

    reserve X,Y,Z for Element of L;

    theorem :: BOOLEALG:9

    

     Th9: X [= ( Bottom L) implies X = ( Bottom L) by LATTICES: 16;

    theorem :: BOOLEALG:10

    X [= Y & X [= Z & (Y "/\" Z) = ( Bottom L) implies X = ( Bottom L) by Th9, FILTER_0: 7;

    theorem :: BOOLEALG:11

    

     Th11: (X "\/" Y) = ( Bottom L) iff X = ( Bottom L) & Y = ( Bottom L) by LATTICES: 5, LATTICES: 16;

    theorem :: BOOLEALG:12

    X [= Y & (Y "/\" Z) = ( Bottom L) implies (X "/\" Z) = ( Bottom L) by Th9, LATTICES: 9;

    theorem :: BOOLEALG:13

    

     Th13: X meets Y & Y [= Z implies X meets Z by Th9, LATTICES: 9;

    theorem :: BOOLEALG:14

    

     Th14: X meets (Y "/\" Z) implies X meets Y & X meets Z

    proof

      assume X meets (Y "/\" Z);

      then

       A1: (X "/\" (Y "/\" Z)) <> ( Bottom L);

      then ((X "/\" Z) "/\" Y) <> ( Bottom L) by LATTICES:def 7;

      then

       A2: (X "/\" Z) <> ( Bottom L);

      ((X "/\" Y) "/\" Z) <> ( Bottom L) by A1, LATTICES:def 7;

      then (X "/\" Y) <> ( Bottom L);

      hence thesis by A2;

    end;

    theorem :: BOOLEALG:15

    X meets (Y \ Z) implies X meets Y

    proof

      assume X meets (Y \ Z);

      then (X "/\" (Y \ Z)) <> ( Bottom L);

      then ((X "/\" Y) "/\" (Z ` )) <> ( Bottom L) by LATTICES:def 7;

      then (X "/\" Y) <> ( Bottom L);

      hence thesis;

    end;

    theorem :: BOOLEALG:16

    X misses ( Bottom L);

    theorem :: BOOLEALG:17

    X misses Z & Y [= Z implies X misses Y by Th13;

    theorem :: BOOLEALG:18

    X misses Y or X misses Z implies X misses (Y "/\" Z) by Th14;

    theorem :: BOOLEALG:19

    X [= Y & X [= Z & Y misses Z implies X = ( Bottom L) by Th9, FILTER_0: 7;

    theorem :: BOOLEALG:20

    X misses Y implies (Z "/\" X) misses (Z "/\" Y)

    proof

      assume

       A1: X misses Y;

      ((Z "/\" X) "/\" (Z "/\" Y)) = (Z "/\" (X "/\" (Y "/\" Z))) by LATTICES:def 7

      .= (Z "/\" ((X "/\" Y) "/\" Z)) by LATTICES:def 7

      .= (Z "/\" ( Bottom L)) by A1

      .= ( Bottom L);

      hence thesis;

    end;

    begin

    reserve L for B_Lattice;

    reserve X,Y,Z,V for Element of L;

    theorem :: BOOLEALG:21

    (X \ Y) [= Z implies X [= (Y "\/" Z)

    proof

      assume (X \ Y) [= Z;

      then (Y "\/" (X "/\" (Y ` ))) [= (Y "\/" Z) by FILTER_0: 1;

      then ((Y "\/" X) "/\" (Y "\/" (Y ` ))) [= (Y "\/" Z) by LATTICES: 11;

      then

       A1: ((Y "\/" X) "/\" ( Top L)) [= (Y "\/" Z) by LATTICES: 21;

      X [= (X "\/" Y) by LATTICES: 5;

      hence thesis by A1, LATTICES: 7;

    end;

    theorem :: BOOLEALG:22

    

     Th22: X [= Y implies (Z \ Y) [= (Z \ X)

    proof

      assume X [= Y;

      then (Y ` ) [= (X ` ) by LATTICES: 26;

      hence thesis by LATTICES: 9;

    end;

    theorem :: BOOLEALG:23

    X [= Y & Z [= V implies (X \ V) [= (Y \ Z)

    proof

      assume X [= Y & Z [= V;

      then (X \ V) [= (Y \ V) & (Y \ V) [= (Y \ Z) by Th22, LATTICES: 9;

      hence thesis by LATTICES: 7;

    end;

    theorem :: BOOLEALG:24

    X [= (Y "\/" Z) implies (X \ Y) [= Z

    proof

      assume X [= (Y "\/" Z);

      then (X "/\" (Y ` )) [= ((Y "\/" Z) "/\" (Y ` )) by LATTICES: 9;

      then (X "/\" (Y ` )) [= ((Y "/\" (Y ` )) "\/" (Z "/\" (Y ` ))) by LATTICES:def 11;

      then

       A1: (X \ Y) [= (( Bottom L) "\/" (Z "/\" (Y ` ))) by LATTICES: 20;

      (Z "/\" (Y ` )) [= Z by LATTICES: 6;

      hence thesis by A1, LATTICES: 7;

    end;

    theorem :: BOOLEALG:25

    (X ` ) [= ((X "/\" Y) ` )

    proof

      (X ` ) [= ((X ` ) "\/" (Y ` )) by LATTICES: 5;

      hence thesis by LATTICES: 23;

    end;

    theorem :: BOOLEALG:26

    ((X "\/" Y) ` ) [= (X ` )

    proof

      ((X "\/" Y) ` ) = ((X ` ) "/\" (Y ` )) by LATTICES: 24;

      hence thesis by LATTICES: 6;

    end;

    theorem :: BOOLEALG:27

    X [= (Y \ X) implies X = ( Bottom L)

    proof

      

       A1: (X "/\" (Y "/\" (X ` ))) = (Y "/\" ((X ` ) "/\" X)) by LATTICES:def 7

      .= (Y "/\" ( Bottom L)) by LATTICES: 20

      .= ( Bottom L);

      assume X [= (Y \ X);

      hence thesis by A1, LATTICES: 4;

    end;

    theorem :: BOOLEALG:28

    X [= Y implies Y = (X "\/" (Y \ X))

    proof

      assume

       A1: X [= Y;

      Y = (Y "/\" ( Top L))

      .= (Y "/\" (X "\/" (X ` ))) by LATTICES: 21

      .= ((Y "/\" X) "\/" (Y "/\" (X ` ))) by LATTICES:def 11

      .= (X "\/" (Y \ X)) by A1, LATTICES: 4;

      hence thesis;

    end;

    theorem :: BOOLEALG:29

    

     Th29: (X \ Y) = ( Bottom L) iff X [= Y

    proof

      thus (X \ Y) = ( Bottom L) implies X [= Y

      proof

        

         A1: (X "/\" (Y ` )) = ( Bottom L) implies X [= ((Y ` ) ` ) by LATTICES: 25;

        assume (X \ Y) = ( Bottom L);

        hence thesis by A1;

      end;

      assume X [= Y;

      then (X "/\" (Y ` )) [= ((Y ` ) "/\" Y) by LATTICES: 9;

      then

       A2: (X "/\" (Y ` )) [= ( Bottom L) by LATTICES: 20;

      ( Bottom L) [= (X \ Y) by LATTICES: 16;

      hence thesis by A2;

    end;

    theorem :: BOOLEALG:30

    X [= (Y "\/" Z) & (X "/\" Z) = ( Bottom L) implies X [= Y

    proof

      assume that

       A1: X [= (Y "\/" Z) and

       A2: (X "/\" Z) = ( Bottom L);

      (X "/\" (Y "\/" Z)) = X by A1, LATTICES: 4;

      then ((X "/\" Y) "\/" ( Bottom L)) = X by A2, LATTICES:def 11;

      hence thesis by LATTICES: 4;

    end;

    theorem :: BOOLEALG:31

    (X "\/" Y) = ((X \ Y) "\/" Y)

    proof

      

      thus (X "\/" Y) = ((X "\/" Y) "/\" ( Top L))

      .= ((X "\/" Y) "/\" ((Y ` ) "\/" Y)) by LATTICES: 21

      .= ((X \ Y) "\/" Y) by LATTICES: 11;

    end;

    theorem :: BOOLEALG:32

    (X \ (X "\/" Y)) = ( Bottom L) by Th29, LATTICES: 5;

    theorem :: BOOLEALG:33

    

     Th33: (X \ (X "/\" Y)) = (X \ Y)

    proof

      (X \ (X "/\" Y)) = (X "/\" ((X ` ) "\/" (Y ` ))) by LATTICES: 23

      .= ((X "/\" (X ` )) "\/" (X "/\" (Y ` ))) by LATTICES:def 11

      .= (( Bottom L) "\/" (X "/\" (Y ` ))) by LATTICES: 20

      .= (X "/\" (Y ` ));

      hence thesis;

    end;

    theorem :: BOOLEALG:34

    ((X \ Y) "/\" Y) = ( Bottom L)

    proof

      ((X \ Y) "/\" Y) = (X "/\" ((Y ` ) "/\" Y)) by LATTICES:def 7

      .= (X "/\" ( Bottom L)) by LATTICES: 20;

      hence thesis;

    end;

    theorem :: BOOLEALG:35

    

     Th35: (X "\/" (Y \ X)) = (X "\/" Y)

    proof

      (X "\/" (Y \ X)) = ((X "\/" Y) "/\" (X "\/" (X ` ))) by LATTICES: 11

      .= ((X "\/" Y) "/\" ( Top L)) by LATTICES: 21;

      hence thesis;

    end;

    theorem :: BOOLEALG:36

    

     Th36: ((X "/\" Y) "\/" (X \ Y)) = X

    proof

      ((X "/\" Y) "\/" (X \ Y)) = (((X "/\" Y) "\/" X) "/\" ((X "/\" Y) "\/" (Y ` ))) by LATTICES: 11

      .= (X "/\" ((X "/\" Y) "\/" (Y ` ))) by LATTICES:def 8

      .= (X "/\" ((X "\/" (Y ` )) "/\" (Y "\/" (Y ` )))) by LATTICES: 11

      .= (X "/\" ((X "\/" (Y ` )) "/\" ( Top L))) by LATTICES: 21

      .= X by LATTICES:def 9;

      hence thesis;

    end;

    theorem :: BOOLEALG:37

    

     Th37: (X \ (Y \ Z)) = ((X \ Y) "\/" (X "/\" Z))

    proof

      (X \ (Y \ Z)) = (X "/\" ((Y ` ) "\/" ((Z ` ) ` ))) by LATTICES: 23

      .= (X "/\" ((Y ` ) "\/" Z))

      .= ((X "/\" (Y ` )) "\/" (X "/\" Z)) by LATTICES:def 11;

      hence thesis;

    end;

    theorem :: BOOLEALG:38

    (X \ (X \ Y)) = (X "/\" Y)

    proof

      (X \ (X \ Y)) = (X "/\" ((X ` ) "\/" ((Y ` ) ` ))) by LATTICES: 23

      .= (X "/\" ((X ` ) "\/" Y))

      .= ((X "/\" (X ` )) "\/" (X "/\" Y)) by LATTICES:def 11

      .= (( Bottom L) "\/" (X "/\" Y)) by LATTICES: 20;

      hence thesis;

    end;

    theorem :: BOOLEALG:39

    ((X "\/" Y) \ Y) = (X \ Y)

    proof

      ((X "\/" Y) \ Y) = ((X "/\" (Y ` )) "\/" (Y "/\" (Y ` ))) by LATTICES:def 11

      .= ((X "/\" (Y ` )) "\/" ( Bottom L)) by LATTICES: 20

      .= (X "/\" (Y ` ));

      hence thesis;

    end;

    theorem :: BOOLEALG:40

    (X "/\" Y) = ( Bottom L) iff (X \ Y) = X

    proof

      thus (X "/\" Y) = ( Bottom L) implies (X \ Y) = X

      proof

        assume (X "/\" Y) = ( Bottom L);

        then

         A1: (X "/\" X) [= (X "/\" (Y ` )) by LATTICES: 9, LATTICES: 25;

        (X \ Y) [= X by LATTICES: 6;

        hence thesis by A1;

      end;

      assume (X \ Y) = X;

      then ((X ` ) "\/" ((Y ` ) ` )) = (X ` ) by LATTICES: 23;

      then (X "/\" ((X ` ) "\/" Y)) [= (X "/\" (X ` ));

      then ((X "/\" (X ` )) "\/" (X "/\" Y)) [= (X "/\" (X ` )) by LATTICES:def 11;

      then (( Bottom L) "\/" (X "/\" Y)) [= (X "/\" (X ` )) by LATTICES: 20;

      then

       A2: (X "/\" Y) [= ( Bottom L) by LATTICES: 20;

      ( Bottom L) [= (X "/\" Y) by LATTICES: 16;

      hence thesis by A2;

    end;

    theorem :: BOOLEALG:41

    (X \ (Y "\/" Z)) = ((X \ Y) "/\" (X \ Z))

    proof

      

      thus (X \ (Y "\/" Z)) = (X "/\" ((Y ` ) "/\" (Z ` ))) by LATTICES: 24

      .= (((X "/\" X) "/\" (Y ` )) "/\" (Z ` )) by LATTICES:def 7

      .= ((X "/\" (X "/\" (Y ` ))) "/\" (Z ` )) by LATTICES:def 7

      .= ((X \ Y) "/\" (X \ Z)) by LATTICES:def 7;

    end;

    theorem :: BOOLEALG:42

    

     Th42: (X \ (Y "/\" Z)) = ((X \ Y) "\/" (X \ Z))

    proof

      

      thus (X \ (Y "/\" Z)) = (X "/\" ((Y ` ) "\/" (Z ` ))) by LATTICES: 23

      .= ((X \ Y) "\/" (X \ Z)) by LATTICES:def 11;

    end;

    theorem :: BOOLEALG:43

    (X "/\" (Y \ Z)) = ((X "/\" Y) \ (X "/\" Z))

    proof

      ((X "/\" Y) \ (X "/\" Z)) = (((X "/\" Y) \ X) "\/" ((X "/\" Y) \ Z)) by Th42

      .= (( Bottom L) "\/" ((X "/\" Y) \ Z)) by Th29, LATTICES: 6

      .= ((X "/\" Y) \ Z);

      hence thesis by LATTICES:def 7;

    end;

    theorem :: BOOLEALG:44

    

     Th44: ((X "\/" Y) \ (X "/\" Y)) = ((X \ Y) "\/" (Y \ X))

    proof

      ((X "\/" Y) \ (X "/\" Y)) = ((X "\/" Y) "/\" ((X ` ) "\/" (Y ` ))) by LATTICES: 23

      .= (((X "\/" Y) "/\" (X ` )) "\/" ((X "\/" Y) "/\" (Y ` ))) by LATTICES:def 11

      .= (((X "/\" (X ` )) "\/" (Y "/\" (X ` ))) "\/" ((X "\/" Y) "/\" (Y ` ))) by LATTICES:def 11

      .= (((X "/\" (X ` )) "\/" (Y "/\" (X ` ))) "\/" ((X "/\" (Y ` )) "\/" (Y "/\" (Y ` )))) by LATTICES:def 11

      .= ((( Bottom L) "\/" (Y "/\" (X ` ))) "\/" ((X "/\" (Y ` )) "\/" (Y "/\" (Y ` )))) by LATTICES: 20

      .= ((Y "/\" (X ` )) "\/" ((X "/\" (Y ` )) "\/" ( Bottom L))) by LATTICES: 20

      .= ((X \ Y) "\/" (Y \ X));

      hence thesis;

    end;

    theorem :: BOOLEALG:45

    

     Th45: ((X \ Y) \ Z) = (X \ (Y "\/" Z))

    proof

      

      thus ((X \ Y) \ Z) = (X "/\" ((Y ` ) "/\" (Z ` ))) by LATTICES:def 7

      .= (X \ (Y "\/" Z)) by LATTICES: 24;

    end;

    theorem :: BOOLEALG:46

    (X \ Y) = (Y \ X) implies X = Y

    proof

      assume

       A1: (X \ Y) = (Y \ X);

      

      then ((X "/\" (Y ` )) "/\" X) = (Y "/\" ((X ` ) "/\" X)) by LATTICES:def 7

      .= (Y "/\" ( Bottom L)) by LATTICES: 20

      .= ( Bottom L);

      then ((X "/\" X) "/\" (Y ` )) = ( Bottom L) by LATTICES:def 7;

      

      then ((X "/\" (Y ` )) "\/" (X ` )) = ((X "/\" (X ` )) "\/" (X ` )) by LATTICES: 20

      .= (X ` ) by LATTICES:def 8;

      then ((X "\/" (X ` )) "/\" ((Y ` ) "\/" (X ` ))) = (X ` ) by LATTICES: 11;

      then (( Top L) "/\" ((Y ` ) "\/" (X ` ))) = (X ` ) by LATTICES: 21;

      then ((Y ` ) "/\" (X ` )) = (Y ` ) by LATTICES:def 9;

      then ((X ` ) ` ) [= ((Y ` ) ` ) by LATTICES: 4, LATTICES: 26;

      then X [= ((Y ` ) ` );

      then

       A2: X [= Y;

      (X "/\" ((Y ` ) "/\" Y)) = ((Y "/\" (X ` )) "/\" Y) by A1, LATTICES:def 7;

      then (X "/\" ( Bottom L)) = ((Y "/\" (X ` )) "/\" Y) by LATTICES: 20;

      

      then ( Bottom L) = ((X ` ) "/\" (Y "/\" Y)) by LATTICES:def 7

      .= ((X ` ) "/\" Y);

      then Y [= ((X ` ) ` ) by LATTICES: 25;

      then Y [= X;

      hence thesis by A2;

    end;

    theorem :: BOOLEALG:47

    

     Th47: (X \ ( Bottom L)) = X

    proof

      (X \ ( Bottom L)) = (X "/\" ( Top L)) by LATTICE4: 30

      .= X;

      hence thesis;

    end;

    theorem :: BOOLEALG:48

    ((X \ Y) ` ) = ((X ` ) "\/" Y)

    proof

      ((X \ Y) ` ) = ((X ` ) "\/" ((Y ` ) ` )) by LATTICES: 23;

      hence thesis;

    end;

    theorem :: BOOLEALG:49

    

     Th49: X meets (Y "\/" Z) iff X meets Y or X meets Z

    proof

      thus X meets (Y "\/" Z) implies X meets Y or X meets Z

      proof

        assume X meets (Y "\/" Z);

        then (X "/\" (Y "\/" Z)) <> ( Bottom L);

        then ((X "/\" Y) "\/" (X "/\" Z)) <> ( Bottom L) by LATTICES:def 11;

        then (X "/\" Y) <> ( Bottom L) or (X "/\" Z) <> ( Bottom L);

        hence thesis;

      end;

      assume

       A1: X meets Y or X meets Z;

      per cases by A1;

        suppose

         A2: X meets Y;

        (X "/\" Y) [= ((X "/\" Y) "\/" (X "/\" Z)) by LATTICES: 5;

        then

         A3: (X "/\" Y) [= (X "/\" (Y "\/" Z)) by LATTICES:def 11;

        (X "/\" (Y "\/" Z)) <> ( Bottom L) by A3, Th9, A2;

        hence thesis;

      end;

        suppose

         A4: X meets Z;

        

         A5: ((X "/\" Z) "\/" (X "/\" Y)) = (X "/\" (Y "\/" Z)) by LATTICES:def 11;

        (X "/\" Z) <> ( Bottom L) by A4;

        then (X "/\" (Y "\/" Z)) <> ( Bottom L) by A5, Th11;

        hence thesis;

      end;

    end;

    theorem :: BOOLEALG:50

    

     Th50: (X "/\" Y) misses (X \ Y)

    proof

      ((X "/\" Y) "/\" (X \ Y)) = (((X "/\" Y) "/\" (Y ` )) "/\" X) by LATTICES:def 7

      .= ((X "/\" (Y "/\" (Y ` ))) "/\" X) by LATTICES:def 7

      .= (( Bottom L) "/\" X) by LATTICES: 20

      .= ( Bottom L);

      hence thesis;

    end;

    theorem :: BOOLEALG:51

    X misses (Y "\/" Z) iff X misses Y & X misses Z by Th49;

    theorem :: BOOLEALG:52

    (X \ Y) misses Y

    proof

      ((X \ Y) "/\" Y) = (X "/\" ((Y ` ) "/\" Y)) by LATTICES:def 7

      .= (X "/\" ( Bottom L)) by LATTICES: 20

      .= ( Bottom L);

      hence thesis;

    end;

    theorem :: BOOLEALG:53

    X misses Y implies ((X "\/" Y) \ Y) = X

    proof

      assume (X "/\" Y) = ( Bottom L);

      then ((X ` ) "\/" (X "/\" Y)) = (X ` );

      then (((X ` ) "\/" X) "/\" ((X ` ) "\/" Y)) = (X ` ) by LATTICES: 11;

      then (( Top L) "/\" ((X ` ) "\/" Y)) = (X ` ) by LATTICES: 21;

      then (((X ` ) "\/" Y) ` ) = X;

      then

       A1: (((X ` ) ` ) "/\" (Y ` )) = X by LATTICES: 24;

      ((X "\/" Y) \ Y) = ((X "/\" (Y ` )) "\/" (Y "/\" (Y ` ))) by LATTICES:def 11

      .= ((X "/\" (Y ` )) "\/" ( Bottom L)) by LATTICES: 20

      .= (X "/\" (Y ` ));

      hence thesis by A1;

    end;

    theorem :: BOOLEALG:54

    ((X ` ) "\/" (Y ` )) = (X "\/" Y) & X misses (X ` ) & Y misses (Y ` ) implies X = (Y ` ) & Y = (X ` )

    proof

      assume that

       A1: ((X ` ) "\/" (Y ` )) = (X "\/" Y) and

       A2: X misses (X ` ) and

       A3: Y misses (Y ` );

      

       A4: (X "/\" (X ` )) = ( Bottom L) by A2;

      

       A5: (Y "/\" (Y ` )) = ( Bottom L) by A3;

      then

       A6: ((Y ` ) "/\" ((X ` ) "\/" (Y ` ))) = (((Y ` ) "/\" X) "\/" ( Bottom L)) by A1, LATTICES:def 11;

      ((Y "/\" (X ` )) "\/" (Y "/\" (Y ` ))) = (Y "/\" (X "\/" Y)) by A1, LATTICES:def 11;

      then (Y "/\" (X ` )) = (Y "/\" (X "\/" Y)) by A5;

      then

       A7: (Y "/\" (X ` )) = Y by LATTICES:def 9;

      ((X "/\" (X ` )) "\/" (X "/\" (Y ` ))) = (X "/\" (X "\/" Y)) by A1, LATTICES:def 11;

      

      then (X "/\" (Y ` )) = (X "/\" (X "\/" Y)) by A4

      .= X by LATTICES:def 9;

      hence X = (Y ` ) by A6, LATTICES:def 9;

      ((X ` ) "/\" ((X ` ) "\/" (Y ` ))) = (( Bottom L) "\/" ((X ` ) "/\" Y)) by A1, A4, LATTICES:def 11;

      hence thesis by A7, LATTICES:def 9;

    end;

    theorem :: BOOLEALG:55

    ((X ` ) "\/" (Y ` )) = (X "\/" Y) & Y misses (X ` ) & X misses (Y ` ) implies X = (X ` ) & Y = (Y ` )

    proof

      assume that

       A1: ((X ` ) "\/" (Y ` )) = (X "\/" Y) and

       A2: Y misses (X ` ) and

       A3: X misses (Y ` );

      

       A4: (Y "/\" (X ` )) = ( Bottom L) by A2;

      then ((X "\/" Y) "/\" (X "\/" (X ` ))) = (X "\/" ( Bottom L)) by LATTICES: 11;

      then ((X "\/" Y) "/\" ( Top L)) = X by LATTICES: 21;

      then ((Y "/\" X) ` ) [= (Y ` ) by LATTICES:def 9;

      then

       A5: (X "\/" Y) [= (Y ` ) by A1, LATTICES: 23;

      

       A6: (X "/\" (Y ` )) = ( Bottom L) by A3;

      then ((Y "\/" X) "/\" (Y "\/" (Y ` ))) = (Y "\/" ( Bottom L)) by LATTICES: 11;

      then ((Y "\/" X) "/\" ( Top L)) = Y by LATTICES: 21;

      then ((X "/\" Y) ` ) [= (X ` ) by LATTICES:def 9;

      then

       A7: (X "\/" Y) [= (X ` ) by A1, LATTICES: 23;

      (((Y ` ) "\/" Y) "/\" ((Y ` ) "\/" (X ` ))) = ((Y ` ) "\/" ( Bottom L)) by A4, LATTICES: 11;

      then (( Top L) "/\" ((Y ` ) "\/" (X ` ))) = (Y ` ) by LATTICES: 21;

      then (((X ` ) "/\" (Y ` )) ` ) [= ((X ` ) ` ) by LATTICES:def 9;

      then (((X ` ) "/\" (Y ` )) ` ) [= X;

      then (((X ` ) ` ) "\/" ((Y ` ) ` )) [= X by LATTICES: 23;

      then (X "\/" ((Y ` ) ` )) [= X;

      then

       A8: ((X ` ) "\/" (Y ` )) [= X by A1;

      (X ` ) [= ((X ` ) "\/" (Y ` )) by LATTICES: 5;

      then

       A9: (X ` ) [= X by A8, LATTICES: 7;

      (((X ` ) "\/" X) "/\" ((X ` ) "\/" (Y ` ))) = ((X ` ) "\/" ( Bottom L)) by A6, LATTICES: 11;

      then (( Top L) "/\" ((X ` ) "\/" (Y ` ))) = (X ` ) by LATTICES: 21;

      then (((Y ` ) "/\" (X ` )) ` ) [= ((Y ` ) ` ) by LATTICES:def 9;

      then (((Y ` ) ` ) "\/" ((X ` ) ` )) [= ((Y ` ) ` ) by LATTICES: 23;

      then (((Y ` ) ` ) "\/" ((X ` ) ` )) [= Y;

      then (((Y ` ) ` ) "\/" X) [= Y;

      then

       A10: ((X ` ) "\/" (Y ` )) [= Y by A1;

      (Y ` ) [= ((X ` ) "\/" (Y ` )) by LATTICES: 5;

      then

       A11: (Y ` ) [= Y by A10, LATTICES: 7;

      X [= (X "\/" Y) by LATTICES: 5;

      then

       A12: X [= (X ` ) by A7, LATTICES: 7;

      Y [= (X "\/" Y) by LATTICES: 5;

      then Y [= (Y ` ) by A5, LATTICES: 7;

      hence thesis by A11, A9, A12;

    end;

    theorem :: BOOLEALG:56

    (X \+\ ( Bottom L)) = X by Th47;

    theorem :: BOOLEALG:57

    (X \+\ X) = ( Bottom L) by LATTICES: 20;

    theorem :: BOOLEALG:58

    (X "/\" Y) misses (X \+\ Y)

    proof

      (X "/\" Y) misses (X \ Y) & (X "/\" Y) misses (Y \ X) by Th50;

      hence thesis by Th49;

    end;

    theorem :: BOOLEALG:59

    (X "\/" Y) = (X \+\ (Y \ X))

    proof

      (X "\/" Y) = ((X "\/" Y) "/\" ( Top L))

      .= ((X "\/" Y) "/\" (X "\/" (X ` ))) by LATTICES: 21

      .= (X "\/" (Y "/\" (X ` ))) by LATTICES: 11

      .= (((X "/\" (Y ` )) "\/" (X "/\" X)) "\/" (Y "/\" (X ` ))) by LATTICES:def 8

      .= (((X "/\" (Y ` )) "\/" (X "/\" ((X ` ) ` ))) "\/" (Y "/\" ((X ` ) "/\" (X ` ))))

      .= ((X "/\" ((Y ` ) "\/" ((X ` ) ` ))) "\/" (Y "/\" ((X ` ) "/\" (X ` )))) by LATTICES:def 11

      .= ((X "/\" ((Y "/\" (X ` )) ` )) "\/" (Y "/\" ((X ` ) "/\" (X ` )))) by LATTICES: 23

      .= (X \+\ (Y \ X)) by LATTICES:def 7;

      hence thesis;

    end;

    theorem :: BOOLEALG:60

    (X \+\ (X "/\" Y)) = (X \ Y)

    proof

      (X \+\ (X "/\" Y)) = ((X "/\" ((X "/\" Y) ` )) "\/" (Y "/\" (X "/\" (X ` )))) by LATTICES:def 7

      .= ((X "/\" ((X "/\" Y) ` )) "\/" (Y "/\" ( Bottom L))) by LATTICES: 20

      .= (X "/\" ((X ` ) "\/" (Y ` ))) by LATTICES: 23

      .= ((X "/\" (X ` )) "\/" (X "/\" (Y ` ))) by LATTICES:def 11

      .= (( Bottom L) "\/" (X "/\" (Y ` ))) by LATTICES: 20

      .= (X "/\" (Y ` ));

      hence thesis;

    end;

    theorem :: BOOLEALG:61

    (X "\/" Y) = ((X \+\ Y) "\/" (X "/\" Y))

    proof

      

      thus (X "\/" Y) = ((Y \ X) "\/" X) by Th35

      .= ((Y \ X) "\/" ((X \ Y) "\/" (X "/\" Y))) by Th36

      .= ((X \+\ Y) "\/" (X "/\" Y)) by LATTICES:def 5;

    end;

    

     Lm1: ((X "\/" Y) \ (X \+\ Y)) = (X "/\" Y)

    proof

      set XY = (X "\/" Y);

      

      thus (XY \ (X \+\ Y)) = (XY "/\" (((X "/\" (Y ` )) ` ) "/\" ((Y "/\" (X ` )) ` ))) by LATTICES: 24

      .= (XY "/\" (((X "/\" (Y ` )) ` ) "/\" ((Y ` ) "\/" ((X ` ) ` )))) by LATTICES: 23

      .= (XY "/\" (((X ` ) "\/" ((Y ` ) ` )) "/\" ((Y ` ) "\/" ((X ` ) ` )))) by LATTICES: 23

      .= (XY "/\" (((X ` ) "\/" ((Y ` ) ` )) "/\" ((Y ` ) "\/" X)))

      .= (XY "/\" (((X ` ) "\/" Y) "/\" ((Y ` ) "\/" X)))

      .= ((XY "/\" ((X ` ) "\/" Y)) "/\" ((Y ` ) "\/" X)) by LATTICES:def 7

      .= (((XY "/\" (X ` )) "\/" ((X "\/" Y) "/\" Y)) "/\" ((Y ` ) "\/" X)) by LATTICES:def 11

      .= (((XY "/\" (X ` )) "\/" Y) "/\" ((Y ` ) "\/" X)) by LATTICES:def 9

      .= ((((X "/\" (X ` )) "\/" (Y "/\" (X ` ))) "\/" Y) "/\" ((Y ` ) "\/" X)) by LATTICES:def 11

      .= (((( Bottom L) "\/" (Y "/\" (X ` ))) "\/" Y) "/\" ((Y ` ) "\/" X)) by LATTICES: 20

      .= (Y "/\" ((Y ` ) "\/" X)) by LATTICES:def 8

      .= ((Y "/\" (Y ` )) "\/" (Y "/\" X)) by LATTICES:def 11

      .= (( Bottom L) "\/" (Y "/\" X)) by LATTICES: 20

      .= (X "/\" Y);

    end;

    theorem :: BOOLEALG:62

    ((X \+\ Y) \+\ (X "/\" Y)) = (X "\/" Y)

    proof

      set XY = (X \+\ Y), A = (Y "/\" (X ` ));

      (XY \+\ (X "/\" Y)) = ((XY "/\" ((X ` ) "\/" (Y ` ))) "\/" ((X "/\" Y) "/\" (XY ` ))) by LATTICES: 23

      .= (((XY "/\" (X ` )) "\/" (XY "/\" (Y ` ))) "\/" ((X "/\" Y) "/\" (XY ` ))) by LATTICES:def 11

      .= (((XY \ X) "\/" (XY \ Y)) "\/" ((X "/\" Y) "/\" (((X "/\" (Y ` )) ` ) "/\" (A ` )))) by LATTICES: 24

      .= (((XY \ X) "\/" (XY \ Y)) "\/" ((X "/\" Y) "/\" (((X ` ) "\/" ((Y ` ) ` )) "/\" (A ` )))) by LATTICES: 23

      .= (((XY \ X) "\/" (XY \ Y)) "\/" ((X "/\" Y) "/\" (((X ` ) "\/" ((Y ` ) ` )) "/\" ((Y ` ) "\/" ((X ` ) ` ))))) by LATTICES: 23

      .= (((XY \ X) "\/" (XY \ Y)) "\/" ((X "/\" Y) "/\" (((X ` ) "\/" Y) "/\" ((Y ` ) "\/" ((X ` ) ` )))))

      .= (((XY \ X) "\/" (XY \ Y)) "\/" ((X "/\" Y) "/\" (((X ` ) "\/" Y) "/\" ((Y ` ) "\/" X))))

      .= (((XY \ X) "\/" (XY \ Y)) "\/" (((X "/\" Y) "/\" ((X ` ) "\/" Y)) "/\" ((Y ` ) "\/" X))) by LATTICES:def 7

      .= (((XY \ X) "\/" (XY \ Y)) "\/" ((((X "/\" Y) "/\" (X ` )) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y ` ) "\/" X))) by LATTICES:def 11

      .= (((XY \ X) "\/" (XY \ Y)) "\/" (((Y "/\" (X "/\" (X ` ))) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y ` ) "\/" X))) by LATTICES:def 7

      .= (((XY \ X) "\/" (XY \ Y)) "\/" (((Y "/\" ( Bottom L)) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y ` ) "\/" X))) by LATTICES: 20

      .= (((XY \ X) "\/" (XY \ Y)) "\/" ((X "/\" (Y "/\" Y)) "/\" ((Y ` ) "\/" X))) by LATTICES:def 7

      .= (((XY \ X) "\/" (XY \ Y)) "\/" (((X "/\" Y) "/\" (Y ` )) "\/" ((X "/\" Y) "/\" X))) by LATTICES:def 11

      .= (((XY \ X) "\/" (XY \ Y)) "\/" ((X "/\" (Y "/\" (Y ` ))) "\/" ((X "/\" Y) "/\" X))) by LATTICES:def 7

      .= (((XY \ X) "\/" (XY \ Y)) "\/" ((X "/\" ( Bottom L)) "\/" ((X "/\" Y) "/\" X))) by LATTICES: 20

      .= (((XY \ X) "\/" (XY \ Y)) "\/" (Y "/\" (X "/\" X))) by LATTICES:def 7

      .= (((((X "/\" (Y ` )) "/\" (X ` )) "\/" (A "/\" (X ` ))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y ` ))) "\/" (Y "/\" X)) by LATTICES:def 11

      .= (((((Y ` ) "/\" (X "/\" (X ` ))) "\/" (A "/\" (X ` ))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y ` ))) "\/" (Y "/\" X)) by LATTICES:def 7

      .= (((((Y ` ) "/\" (X "/\" (X ` ))) "\/" (Y "/\" ((X ` ) "/\" (X ` )))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y ` ))) "\/" (Y "/\" X)) by LATTICES:def 7

      .= (((((Y ` ) "/\" ( Bottom L)) "\/" (Y "/\" ((X ` ) "/\" (X ` )))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y ` ))) "\/" (Y "/\" X)) by LATTICES: 20

      .= ((A "\/" (((X "/\" (Y ` )) "/\" (Y ` )) "\/" (A "/\" (Y ` )))) "\/" (Y "/\" X)) by LATTICES:def 11

      .= ((A "\/" ((X "/\" ((Y ` ) "/\" (Y ` ))) "\/" (A "/\" (Y ` )))) "\/" (Y "/\" X)) by LATTICES:def 7

      .= ((A "\/" ((X "/\" (Y ` )) "\/" ((X ` ) "/\" (Y "/\" (Y ` ))))) "\/" (Y "/\" X)) by LATTICES:def 7

      .= ((A "\/" ((X "/\" (Y ` )) "\/" ((X ` ) "/\" ( Bottom L)))) "\/" (Y "/\" X)) by LATTICES: 20

      .= (A "\/" ((X "/\" (Y ` )) "\/" (Y "/\" X))) by LATTICES:def 5

      .= (A "\/" (X "/\" ((Y ` ) "\/" Y))) by LATTICES:def 11

      .= (A "\/" (X "/\" ( Top L))) by LATTICES: 21

      .= ((Y "\/" X) "/\" ((X ` ) "\/" X)) by LATTICES: 11

      .= ((Y "\/" X) "/\" ( Top L)) by LATTICES: 21

      .= (Y "\/" X);

      hence thesis;

    end;

    theorem :: BOOLEALG:63

    ((X \+\ Y) \+\ (X "\/" Y)) = (X "/\" Y)

    proof

      ((X \+\ Y) \+\ (X "\/" Y)) = (((X \+\ Y) "/\" ((X ` ) "/\" (Y ` ))) "\/" ((X "\/" Y) \ (X \+\ Y))) by LATTICES: 24

      .= ((((X "/\" (Y ` )) "/\" ((X ` ) "/\" (Y ` ))) "\/" ((Y "/\" (X ` )) "/\" ((X ` ) "/\" (Y ` )))) "\/" ((X "\/" Y) \ (X \+\ Y))) by LATTICES:def 11

      .= (((X "/\" ((Y ` ) "/\" ((Y ` ) "/\" (X ` )))) "\/" ((Y "/\" (X ` )) "/\" ((X ` ) "/\" (Y ` )))) "\/" ((X "\/" Y) \ (X \+\ Y))) by LATTICES:def 7

      .= (((X "/\" (((Y ` ) "/\" (Y ` )) "/\" (X ` ))) "\/" ((Y "/\" (X ` )) "/\" ((X ` ) "/\" (Y ` )))) "\/" ((X "\/" Y) \ (X \+\ Y))) by LATTICES:def 7

      .= ((((X "/\" (X ` )) "/\" (Y ` )) "\/" ((Y "/\" (X ` )) "/\" ((X ` ) "/\" (Y ` )))) "\/" ((X "\/" Y) \ (X \+\ Y))) by LATTICES:def 7

      .= (((( Bottom L) "/\" (Y ` )) "\/" ((Y "/\" (X ` )) "/\" ((X ` ) "/\" (Y ` )))) "\/" ((X "\/" Y) \ (X \+\ Y))) by LATTICES: 20

      .= ((Y "/\" ((X ` ) "/\" ((X ` ) "/\" (Y ` )))) "\/" ((X "\/" Y) \ (X \+\ Y))) by LATTICES:def 7

      .= ((Y "/\" (((X ` ) "/\" (X ` )) "/\" (Y ` ))) "\/" ((X "\/" Y) \ (X \+\ Y))) by LATTICES:def 7

      .= (((Y "/\" (Y ` )) "/\" (X ` )) "\/" ((X "\/" Y) \ (X \+\ Y))) by LATTICES:def 7

      .= ((( Bottom L) "/\" (X ` )) "\/" ((X "\/" Y) \ (X \+\ Y))) by LATTICES: 20

      .= (Y "/\" X) by Lm1;

      hence thesis;

    end;

    theorem :: BOOLEALG:64

    

     Th64: (X \+\ Y) = ((X "\/" Y) \ (X "/\" Y))

    proof

      

      thus (X \+\ Y) = ((X \ (X "/\" Y)) "\/" (Y \ X)) by Th33

      .= ((X \ (X "/\" Y)) "\/" (Y \ (X "/\" Y))) by Th33

      .= ((X "\/" Y) \ (X "/\" Y)) by LATTICES:def 11;

    end;

    theorem :: BOOLEALG:65

    ((X \+\ Y) \ Z) = ((X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z)))

    proof

      

      thus ((X \+\ Y) \ Z) = (((X \ Y) \ Z) "\/" ((Y \ X) \ Z)) by LATTICES:def 11

      .= ((X \ (Y "\/" Z)) "\/" ((Y \ X) \ Z)) by Th45

      .= ((X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))) by Th45;

    end;

    theorem :: BOOLEALG:66

    (X \ (Y \+\ Z)) = ((X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z))

    proof

      (X \ (Y \+\ Z)) = (X \ ((Y "\/" Z) \ (Y "/\" Z))) by Th64

      .= ((X \ (Y "\/" Z)) "\/" (X "/\" (Y "/\" Z))) by Th37

      .= ((X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)) by LATTICES:def 7;

      hence thesis;

    end;

    theorem :: BOOLEALG:67

    ((X \+\ Y) \+\ Z) = (X \+\ (Y \+\ Z))

    proof

      set S1 = (X \ (Y "\/" Z)), S2 = (Y \ (X "\/" Z)), S3 = (Z \ (X "\/" Y)), S4 = ((X "/\" Y) "/\" Z);

      

      thus ((X \+\ Y) \+\ Z) = ((((X \ Y) \ Z) "\/" ((Y \ X) \ Z)) "\/" (Z \ ((X \ Y) "\/" (Y \ X)))) by LATTICES:def 11

      .= ((S1 "\/" ((Y \ X) \ Z)) "\/" (Z \ ((X \ Y) "\/" (Y \ X)))) by Th45

      .= ((S1 "\/" S2) "\/" (Z \ ((X \ Y) "\/" (Y \ X)))) by Th45

      .= ((S1 "\/" S2) "\/" (Z \ ((X "\/" Y) \ (X "/\" Y)))) by Th44

      .= ((S1 "\/" S2) "\/" (S3 "\/" ((X "/\" Y) "/\" Z))) by Th37

      .= (((S1 "\/" S2) "\/" S4) "\/" S3) by LATTICES:def 5

      .= (((S1 "\/" S4) "\/" S2) "\/" S3) by LATTICES:def 5

      .= ((S1 "\/" S4) "\/" (S2 "\/" S3)) by LATTICES:def 5

      .= ((S1 "\/" (X "/\" (Y "/\" Z))) "\/" (S2 "\/" S3)) by LATTICES:def 7

      .= ((X \ ((Y "\/" Z) \ (Y "/\" Z))) "\/" (S2 "\/" S3)) by Th37

      .= ((X \ ((Y \ Z) "\/" (Z \ Y))) "\/" (S2 "\/" S3)) by Th44

      .= ((X \ ((Y \ Z) "\/" (Z \ Y))) "\/" (S2 "\/" ((Z \ Y) \ X))) by Th45

      .= ((X \ ((Y \ Z) "\/" (Z \ Y))) "\/" (((Y \ Z) \ X) "\/" ((Z \ Y) \ X))) by Th45

      .= (X \+\ (Y \+\ Z)) by LATTICES:def 11;

    end;

    theorem :: BOOLEALG:68

    ((X \+\ Y) ` ) = ((X "/\" Y) "\/" ((X ` ) "/\" (Y ` )))

    proof

      

      thus ((X \+\ Y) ` ) = (((X \ Y) ` ) "/\" ((Y \ X) ` )) by LATTICES: 24

      .= (((X ` ) "\/" ((Y ` ) ` )) "/\" ((Y "/\" (X ` )) ` )) by LATTICES: 23

      .= (((X ` ) "\/" ((Y ` ) ` )) "/\" ((Y ` ) "\/" ((X ` ) ` ))) by LATTICES: 23

      .= (((X ` ) "\/" Y) "/\" ((Y ` ) "\/" ((X ` ) ` )))

      .= (((X ` ) "\/" Y) "/\" ((Y ` ) "\/" X))

      .= (((X ` ) "/\" ((Y ` ) "\/" X)) "\/" (Y "/\" ((Y ` ) "\/" X))) by LATTICES:def 11

      .= ((((X ` ) "/\" (Y ` )) "\/" ((X ` ) "/\" X)) "\/" (Y "/\" ((Y ` ) "\/" X))) by LATTICES:def 11

      .= ((((X ` ) "/\" (Y ` )) "\/" ((X ` ) "/\" X)) "\/" ((Y "/\" (Y ` )) "\/" (Y "/\" X))) by LATTICES:def 11

      .= ((((X ` ) "/\" (Y ` )) "\/" ( Bottom L)) "\/" ((Y "/\" (Y ` )) "\/" (Y "/\" X))) by LATTICES: 20

      .= (((X ` ) "/\" (Y ` )) "\/" (( Bottom L) "\/" (Y "/\" X))) by LATTICES: 20

      .= ((X "/\" Y) "\/" ((X ` ) "/\" (Y ` )));

    end;