Laws for Boolean Algebra with Operators

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
BAO1 'almost' additivity $f(x+y)\leq z \Leftrightarrow f(x)+f(y) \leq z$ $g(x+y)\leq z \Leftrightarrow g(x)+g(y) \leq z$
BAO2 additivity $f(x+y) = f(x)+f(y)$ $g(x+y) = g(x)+g(y)$
BAO3 isotonicity $x\leq y \Rightarrow f(x)\leq f(x)$ $x\leq y \Rightarrow g(x)\leq g(x)$
BAO4 cancellation laws $f(\overline{g(x)}) \leq \overline{x}$ $g(\overline{f(x)}) \leq \overline{x}$
BAO5 addititivity wrt. meet $f(x\meet y) \leq f(x)\meet f(y)$ $g(x\meet y) \leq g(x)\meet g(y)$
BAO6 modular laws $f(x)\meet y \leq (f(x\meet g(y))\meet y)$ $g(x)\meet y \leq (g(x\meet f(y))\meet y)$
BAO7 strictness $f(0)=0$ $g(0)=0$
BAO8 Galois connection between conjugates I $f(x)\leq y \Rightarrow x\leq \overline{g(\overline{y})}$ n/a
BAO9 Galois connection between conjugates II $f(x)\leq y \Leftarrow x\leq \overline{g(\overline{y})}$ n/a
BAO10 uniqueness of conjungates $(\forall x.\forall y.(f(x)\meet y\leq 0 \Leftrightarrow x\meet h(y)\leq 0)) \Rightarrow \forall z.(g(z)=h(z))$ n/a
BAO11 TBD $f(x\meet \overline{g(y)}) \leq f(x)\meet\overline{y}$ n/a

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