Laws for Feature Algebra (Product Families)

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
FA1 refinement is a preorder $x\rord x \wedge(x\rord y \wedge y\rord z \Rightarrow x\rord z)$ n/a
FA2 natural order implies refinement $x\leq y \Rightarrow x\rord y$ n/a
FA3 infima and suprema of refinement $x;y\rord y$
$x\rord x+y$
FA4 isotony w.r.t. refinement and addition $x\rord y \Rightarrow x+z\rord y+z$ $x\rord y \Rightarrow z+x\rord z+y$
FA5 isotony w.r.t. refinement and multiplication $x\rord y \Rightarrow x\cdot z\rord y\cdot z$ $x\rord y \Rightarrow z\cdot x\rord z\cdot y$
FA6 strictness of refinement order $(x\rord 0 \Leftrightarrow x=0) \wedge (x\rord 0 \Leftrightarrow x\leq0)$ n/a
FA7 least and greatest element w.r.t. refinement $0\rord x$
$x\rord 1$
FA8 refinement equivalence I $x\rord y \Rightarrow x\leq y\cdot \top$ n/a
FA9 refinement equivalence II $x\rord y \Leftarrow x\leq y\cdot \top$ n/a
FA10 ideal equivalence I $x\leq y\cdot \top \Rightarrow x\cdot \top\leq y\cdot\top$ n/a
FA11 ideal equivalence II $x\leq y\cdot \top\top \Leftarrow x\cdot \top\leq y\cdot\top$ n/a
FA12 antisymmetry $\forall x \forall y(x\rord y \wedge y\rord x \Rightarrow x=y) \Leftarrow \forall x \forall y (x\rord y \Rightarrow x=y)$ n/a
FA13 join splitting I $x+y\rord z \Rightarrow x\rord z \wedge y\rord z$ n/a
FA14 join splitting II $x+y\rord z \Leftarrow x\rord z \wedge y\rord z$ n/a
FA15 requirement relation is reflexive $p\pims p$ n/a
FA16 requirement relation is transitive $(p\pims q \wedge q\pims r)\Rightarrow p\pims r$ 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