Laws for Boolean Algebra

All presented properties are showed by automated theorem-prover Prover9.
(There is no special order in the presentation of the theorems.)
ID Name Lemma Duals
BA1 existence of a greatest element $x+\overline{x} = y+\overline{y}$ n/a
BA2 involution of complementation $\overline{\overline{x}}=x$ n/a
BA3 TBD $\overline{x}=\overline{x+y}+\overline{x+\overline{y}}$ n/a
BA4 TBD $x+(y+\overline{y})=z+\overline{z}$ n/a
BA5 TBD $x+x=x+\overline{y+\overline{y}}$ n/a
BA6 idempotence of join $x+x=x$ n/a
BA7 idempotence of meet $x\meet x=x$ n/a
BA8 commutativity of meet $x\meet y=y\meet x$ n/a
BA9 associtivity of meet $(x\meet y)\meet z=x\meet (y\meet z)$ n/a
BA10 absorption $(x+y)\meet x = x$ n/a
BA11 TBD $x=(x\meet y)+(x\meet\overline{y})$ n/a
BA12 TBD $x=(x+\overline{y})\meet(x+y)$ n/a
BA13 TBD $(x+y)\meet\overline{x} = y\meet\overline{x}$ n/a
BA14 TBD $x+(x\meet y) = x$ n/a
BA15 distributivity $x\meet(y+z) = (x\meet y)+(x\meet z)$ n/a
BA16 de Morgan I $\overline{x+y} = \overline{x}\meet\overline{y}$ n/a
BA17 de Morgan II $\overline{x\meet y} = \overline{x}+\overline{y}$ n/a
BA18 distributivity $x+(y\meet z) = (x+y)\meet (x+z)$ n/a
BA19 TBD $(\overline{x}\meet y)+(x\meet z) = (x+y)\meet (\overline{x}+z)$ n/a
BA20 TBD $((v\meet w)+(\overline{v}\meet x))\meet \overline{(v\meet y)+(\overline{v}\meet z)} = (v\meet w\meet \overline{y})+(\overline{v}\meet x\meet \overline{z})$ n/a
BA21 TBD $x+y = x+(\overline{x}\meet y)$ n/a
BA22 properties of $0$ and $\top$ $\overline{\top}=0$
$x\meet 0=0$
BA23 $\leq$ is a partial order $x\leq x$
$(x\leq y\wedge y\leq z \Rightarrow x\leq z)$
$(x\leq y\,\wedge\,y\leq x \Rightarrow x=y)$
BA24 $0$ is least and $\top$ greatest element $0\leq x \,\wedge\, x\leq\top$ n/a
BA25 isotonicity w.r.t. meet and join $x\leq y \Rightarrow x+z\leq y+z$
$x\leq y \Rightarrow x\meet z\leq y\meet z$
$x\leq y \Rightarrow z+x\leq z+y$
$x\leq y \Rightarrow z\meet x\leq z\meet y)$
BA26 equivalence I (antitonicity of complement) $x\leq y \Leftrightarrow \overline{y}\leq\overline{x}$ n/a
BA27 equivalence II $ \overline{y}\leq\overline{x}\Leftrightarrow x+y=y$ n/a
BA28 equivalence III $x+y=y \Leftrightarrow x\meet y=x$ n/a
BA29 equivalence IV $x\meet y=x \Leftrightarrow \overline{x}+y=\top$ n/a
BA30 equivalence V $\overline{x}+y=\top \Leftrightarrow x\meet \overline{y}=0$ n/a
BA31 splitting I $x\leq y\meet z \Leftrightarrow x\leq y \,\wedge\, x\leq z$ n/a
BA32 splitting II $x+y\leq z \Leftrightarrow x\leq z \,\wedge\, y\leq z$ n/a
BA33 shunting $x\meet z \leq y \Leftrightarrow x \leq y+\overline{z}$ n/a
BA34 shunting (another version) $x\meet \overline{z} \leq y \Leftrightarrow x \leq y+z$ n/a
BA35 existence of least element $x\meet \overline{x}=y\meet \overline{y}$ n/a
BA36 Maddux's axioms $x+y = y+x$
$x+(y+z) = (x+y)+z$
$x = \overline{\overline{x} + \overline{y}}+\overline{\overline{x}+y}$
$x\meet y = \overline{\overline{x}+\overline{y}}$

In general, we write x,y... and a,b... for arbitrary semiring elements and p,q... for tests. If other letters are involved we adapted the original notation of the authors.
©2007. Peter Höfner