## 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.