## Laws for Feature Algebra (OOP)

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 FT1 idempotence (as a consequence of distance idempotence) $x+x=x$ n/a FT2 reflexivity (as a consequence of distance idempotence) $x\leq x$ n/a FT3 transitivity (as a consequence of distance idempotence) $x \leq y \wedge y \leq z \Rightarrow x \leq z$ n/a FT4 upper bound (as a consequence of distance idempotence) $x \leq x+y$$y \leq x+y n/a FT5 supremum (sum split) (as a consequence of distance idempotence) x+y \leq z \Leftrightarrow x \leq z \wedge y \leq z n/a FT6 quasicommutativity (as a consequence of distance idempotence) \mbox{eqv}(x+y,y+x) n/a FT7 isotony (as a consequence of distance idempotence) x \leq y \Rightarrow x+z \leq y+z$$x \leq y \Rightarrow z+x \leq z+y$ n/a FT8 equivalence of superdistributivity and isotony (as a consequence of distance idempotence) $\forall x \forall y.(f(x)+f(y) \leq f(x+y)) \Leftrightarrow \forall x \forall y.(x \leq y \Rightarrow f(x) \leq f(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