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$ |
n/a |
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$ |
n/a |
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 |
©2007. Peter Höfner |