Overview over all Laws of I-Semirings, Kleene Algebras ...

All presented properties are proven by automated theorem-prover Prover9.
(There is no special order in the presentation of the theorems.)

Laws for I-Semiring

ID Name Lemma Duals
IS1 isotony w.r.t. addition $x\leq y \Rightarrow x+z\leq y+z$ $x\leq y \Rightarrow z+x\leq z+y$
IS2 isotony w.r.t. multiplication $x\leq y \Rightarrow x\cdot z\leq y\cdot z$ $x\leq y \Rightarrow z\cdot x\leq z\cdot y$
IS3 splitting addition (supremum) $x+y\leq z \Leftrightarrow x\leq z \wedge y\leq z$ n/a
IS4 transitivity $x\leq y \wedge y\leq z \Rightarrow x\leq z$ n/a
IS5 splitting an equality into inequalities $x=y \Leftrightarrow x\leq y \wedge y\leq x$ n/a
IS6 Equivalence of idempotence and idempotence of $1$ $\forall x(x+x=x) \Leftrightarrow 1+1=1$ n/a
IS7 0 is least element $0 \leq x$ n/a
IS8 no non-trivial inverse w.r.t. addition $\forall x (x \neq 0 \Rightarrow \neg (\exists y (x+y=0)))$ n/a

Laws for I-Semiring with Tests

ID Name Lemma Duals
IST1 commutativity of tests w.r.t. multiplication $p\cdot q = q\cdot p$ n/a
IST2 multiplication coincides with meet $p\cdotq\leq p$ $p\cdotq\leq q$
IST3 tests restrict elements $p\cdot x\leq x$ $x\cdot p\leq x
IST4 tests are subidentities $p\leq 1$ n/a
IST5 idempotency of tests $p\cdot p = p$ n/a
IST6 shunting I $p\cdot\neg q\leq r \Rightarrow p\leq q+r$ n/a
IST7 shunting II $p\cdot\neg q\leq r \Leftarrow p\leq q+r$ n/a
IST8 splitting multiplication (infimum) $p\leq q\cdot r \Leftrightarrow p\leq q \wedge p\leq r$ n/a
IST9 splitting $p\cdot q\cdot r = p \Leftrightarrow p\cdot q = p \wedge p\cdot r = p$ n/a
IST10 negation of identities $\neg 0 = 1 \wedge \neg 1 = 0$ n/a
IST11 de Morgan I $\neg(\neg p+\neg q)=p\cdot q$ n/a
IST12 de Morgan II $\neg(\neg p\cdot \neg q) = p+q n/a
IST13 negation $p\leq q \Leftrightarrow \neg q\leq \neg p$ n/a
IST14 test equivalence I $p\cdot x\leq x\cdot q\Rightarrowx\cdot\neg q \leq \neg p \cdot x$ $x\cdot p\leq q\cdot x\Rightarrow\neg q\cdot x\leq x \cdot\neg p$
IST15 test equivalence II $x\cdot\neg q \leq \neg p \cdot x\Rightarrowp\cdot x\cdot\neg q = 0$ $\neg q\cdot x\leq x \cdot\neg p\Rightarrow\neg q\cdot x\cdot p= 0
IST16 test equivalence III $p\cdot x\cdot\neg q = 0\Rightarrow p\cdot x = p\cdot x\cdot q$ $\neg q\cdot x\cdot p= 0\Rightarrow x\cdot p = q\cdot x\cdot p$
IST17 test equivalence IV $p\cdot x = p\cdot x\cdot q\Rightarrow p\cdot x\leq x\cdot q$ $x\cdot p = q\cdot x\cdot p\Rightarrow x\cdot p\leq q\cdot x$
IST18 test set is closed under complement $\neg p \in \mbox{test}$ n/a
IST19 distributivity + over multiplication $p+(q\cdot r) = (p+q)\cdot(p+r)$ $(p\cdot q)+r = (p+r)\cdot(q+r)$
IST20 TBD $x \leq p \cdot x \Rightarrow x \leq p\cdot \top$ n/a
IST21 TBD $x \leq p \cdot x \Leftarrow x \leq p \cdot \top$ n/a
IST22 TBD $p=q \cdot r \wedge q= \neg p \cdot r \Rightarrow p=0 \wedge q=0 \wedge r=0$ n/a

Laws for I-Semiring with Domain

ID Name Lemma Duals
ISD1 strictness $\dom(x)=0 \Leftrightarrow x=0$ $\cod(x)=0 \Leftrightarrow x=0$
ISD2 domain of identities $\dom(0)=0\; \wedge\; \dom(1)=1$ $\cod(0)=0\; \wedge\; \cod(1)=1$
ISD3 domain of tests $\dom(p)=p$ $\cod(p)=p$
ISD4 TBD $\dom(y)\cdot\dom(x)\cdot x = \dom(y)\cdot x$ $x\cdot \cod(x)\cdot\cod(y) = x\cdot \cod(y)$
ISD5 additivity $\dom(x+y) = \dom(x)+\dom(y)$ $\cod(x+y) = \cod(x)+\cod(y)$
ISD6 domain commutes $\dom(x)\cdot\dom(y) = \dom(y)\cdot\dom(x)$ $\cod(x)\cdot\cod(y) = \cod(y)\cdot\cod(x)$
ISD7 isotonicity $x\leq y \Rightarrow \dom(x)\leq\dom(y)$ $x\leq y \Rightarrow \cod(x)\leq\cod(y)$
ISD8 idempotence of domain $\dom(\dom(x))=\dom(x)$ $\cod(\cod(x))=\cod(x)$
ISD9 test negation and domain commutes $\neg(\dom(p)) = \dom(\neg p)$ $\neg(\cod(p)) = \cod(\neg p)$
ISD10 separation $x\cdot y = 0 \Rightarrow x\cdot\dom(y)=0$ $x\cdot y = 0 \Rightarrow \cod(x)\cdot y=0$
ISD11 least left preserver $x=p\cdot x \Leftrightarrow \dom(x)\leq p$ $x=x\cdot p \Leftrightarrow \cod(x)\leq p$
ISD12 greatest left annihilator $\neg p\cdot x= 0 \Leftrightarrow \dom(x)\leq p$ $x\cdot\neg p = 0 \Leftrightarrow \cod(x)\leq p$
ISD13 TBD $\dom(x \cdot y) \leq \dom(x)$ n/a
ISD14 distributivity of update over addition $x \update (y+z) = x \update y + x \update z$ n/a
ISD15 property for update $x \update y = y \update x \Rightarrow (x+y) \update z = x \update (y \update z)$ n/a
ISD16 domain and update $\dom(x \update y) = \dom(x) + \dom(y)$ n/a
ISD17 neutrality of 0 w.r.t update $0 \update x = x$ n/a
ISD18 associativity of update $x \update (y \update z) = (x \update y) \update z$ n/a
ISD19 Idempotency $x + x = x$ n/a
ISD20 left invariant $\dom(x) \cdot x = x$ n/a
ISD21 projection $\dom (\dom (x)) = \dom (x)$ n/a
ISD22 prefix increasing $\dom(x \cdot y)+\dom(x) = \dom(x)$ n/a
ISD23 subidentity expansion $x+1 = 1 \Rightarrow x+\dom(x) = \dom(x)$ n/a
ISD24 very strictness $\dom(x) = 0 \Leftrightarrow x = 0$ n/a
ISD25 costrictness $\dom(1) = 1$ n/a
ISD26 isotonicity $x+y = y \Rightarrow \dom(x)+\dom(y) = \dom(y)$ n/a
ISD27 export $\dom(\dom(x) \cdot y) = \dom(x) \cdot \dom(y)$ n/a
ISD28 multiplicative idempotency $\dom(x) \cdot \dom(x) = \dom(x)$ n/a
ISD29 commutativity $\dom(x) \cdot \dom(y) = \dom(y) \cdot \dom(x)$ n/a
ISD30 least left preservation $x+ \dom(y) \cdot x = \dom(y) \cdot x \Leftrightarrow \dom(x)+\dom(y) = \dom(y)$ n/a
ISD31 weak locality $x \cdot y = 0 \Rightarrow x \cdot \dom(y) = 0$ n/a
ISD32 additive closure $\dom(\dom(x)+\dom(y)) = \dom(x)+\dom(y)$ n/a
ISD33 multiplicative closure $\dom(\dom(x) \cdot \dom(y)) = \dom(x) \cdot \dom(y)$ n/a
ISD34 absorption I $\dom(x) \cdot (\dom(x)+\dom(y)) = \dom(x)$ n/a
ISD35 absorption II $\dom(x)+\dom(x) \cdot \dom(y) = \dom(x)$ n/a
ISD36 first module axiom $\dom((x+y) \cdot \dom(z)) = \dom(x \cdot \dom(z))+\dom(y \cdot \dom(z))$ n/a
ISD37 second module axiom $\dom(x \cdot (\dom(y)+\dom(z))) = \dom(x \cdot \dom(y))+\dom(x \cdot \dom(z))$ n/a
ISD38 third module axiom $\dom((x \cdot y) \cdot \dom(z)) = \dom(x \cdot \dom(y \cdot \dom(z)))$ n/a
ISD39 fourth module axiom $\dom(1 \cdot \dom(x)) = \dom(x)$ n/a
ISD40 fifth module axiom $\dom(x \cdot \dom(0)) = 0$ n/a
ISD41 antidomain elements are domain elements $(\dom(x)+a(x) = 1 \wedge \dom(x) \cdot a(x) = 0) \Rightarrow \dom(a(x)) = a(x)$ n/a
ISD42 complementation $(\dom(x)+a(x) = 1 \wedge \dom(x) \cdot a(x) = 0) \Rightarrow a(x) \cdot \dom(x)=0$ n/a
ISD43 double negation $(\dom(x)+a(x) = 1 \wedge \dom(x) \cdot a(x) = 0) \Rightarrow a(a(x)) = \dom(x)$ n/a
ISD44 left annihilation $(\dom(x)+a(x) = 1 \wedge \dom(x) \cdot a(x) = 0) \Rightarrow a(x) \cdot x=0$ n/a
ISD45 antidomain locality $(\dom(x)+a(x) = 1 \wedge \dom(x) \dot a(x) = 0) \Rightarrow a(x \cdot y)+a(x \cdot \dom(y)) = a(x \cdot \dom(y))$ n/a
ISD46 left invariant $x = \dom(x) \cdot x$ n/a
ISD47 domain locality $\dom(x \cdot y) = \dom(x \cdot \dom(y))$ n/a
ISD48 subidentity $\dom(x)+1 = 1$ n/a
ISD49 strictness $\dom(0) = 0$ n/a
ISD50 additivity $\dom(x+y) = \dom(x)+\dom(y)$ n/a
ISD51 greatest left annihilation $\dom(y) \cdot x = 0 \Leftrightarrow \dom(y)+a(x)=a(x)$ n/a
ISD52 antitonicity $x+y = y \Rightarrow a(y)+a(x) = a(x)$ n/a
ISD53 codomain closure $\dom(cd(x)) = cd(x)$ n/a
ISD54 coantidomain closure $\dom(ca(x)) = ca(x)$ n/a

Laws for Modal I-Semiring

ID Name Lemma Duals
MIS1 TBD $|x\rangle p \leq q \Leftrightarrow x\cdot p \leq q\cdot x$ $\langle x| p \leq q \Leftrightarrow p\cdot x \leq x\cdot q$
MIS2 TBD $|x\rangle p \leq q \Leftrightarrow \neg q\cdot x\cdot p = 0$ $\langle x| p \leq q \Leftrightarrow p\cdot x\cdot \neg q = 0$
MIS3 covariance/contravariance $|x\rangle |y\rangle p = |x\cdot y\rangle p$ $\langle y| \langle x| p = \langle x\cdot y| p$
MIS4 additivity $|x\rangle p+ |y\rangle p = |x+y\rangle p$ $\langle x| p+ \langle y| p = \langle x+y| p$
MIS5 additivity II $|x\rangle p + |x\rangle q = |x\rangle (p+q)$ $\langle x| p + \langle x|q = \langle x| (p+q)$
MIS6 covariance/contravariance $|x] |y] p = |x\cdot y] p$ $[y| [x| p = [x\cdot y| p$
MIS7 TBD $|x]p \cdot |y]p = |x+y]p$ $[x|p \cdot [y|p = [x+y|p$
MIS8 multiplicativity $|x]p \cdot |x]q = |x](p\cdot q)$ $[x|p \cdot [x|q = [x|(p\cdot q)$
MIS9 Galois connection I $|x\rangle p \leq q\Leftarrow p\leq [x|q$ $\langle x| p \leq q\Leftarrow p\leq |x]q$
MIS10 Galois connection II $|x\rangle p \leq q\Rightarrow p\leq [x|q$ $\langle x| p \leq q\Rightarrow p\leq |x]q$
MIS11 conjugation $|x\rangle p \leq q \Leftarrow \langle x|\neg q \leq \neg p$ $|x\rangle p \leq q \Rightarrow \langle x|\neg q \leq \neg p$
MIS12 TBD $p \cdot |x\rangle q= |p\cdot x\rangle q$ n/a
MIS13 properties of neutral elements $|x\rangle 0 = 0$
$|x] 1 = 1$
$\langle x| 0 = 0$
$[x| 1 = 1$
MIS14 isotonicity $p\leq q \Rightarrow |x\rangle p \leq |x\rangle q$ $p\leq q \Rightarrow \langle x|p \leq \langle x|q$
MIS15 isotonicity $p\leq q \Rightarrow |x] p \leq |x] q$ $p\leq q \Rightarrow [x|p \leq [x|q$
MIS16 conjugation II $p\cdot |x\rangle q=0 \Leftrightarrow q\cdot \langle x|p=0)$ n/a
MIS17 diamond for tests $|p \rangle q = p \cdot q$ n/a
MIS18 idempotence of diamond for tests $|p \rangle |p] q = |p \rangle q$ n/a
MIS19 a cancellativity law $ \langle x| |x ] p \leq p$ n/a
MIS20 a cancellativity law $p \leq |x] \langle x| p$ n/a
MIS21 demodalisation $|x\rangle \dom(y) + \dom(z) = \dom(z) \Leftarrow x \cdot \dom(y)+\dom(z) \cdot x = \dom(z) \cdot x$ n/a
MIS22 demodalisation $|x\rangle \dom(y)+\dom(z) = \dom(z) \Leftrightarrow a(z) \cdot (x \cdot \dom(y)) = 0$ n/a
MIS23 diamond conjugation I $|x \rangle \dom(y) \cdot \dom(z) = 0 \Rightarrow \dom(y) \cdot \langle x|d(z) = 0$ n/a
MIS24 diamond conjugation II $|x \rangle \dom(y) \cdot \dom(z) = 0 \Leftarrow \dom(y) \cdot \langle x|d(z) = 0$ n/a
MIS25 box conjugation I $|x] \dom(y) + \dom(z) = 1 \Rightarrow \dom(y) + [x| \dom(z) = 1$ n/a
MIS26 box conjugation II $|x] \dom(y) + \dom(z) = 1 \Leftarrow \dom(y) + [x| \dom(z) = 1$ n/a
MIS27 galois connection I $|x\rangle \dom(y)+\dom(z) = \dom(z) \Rightarrow \dom(y)+[x|\dom(z) = [x|\dom(z)$ n/a
MIS28 galois connection II $|x\rangle \dom(y)+\dom(z) = \dom(z) \Leftarrow \dom(y)+[x|\dom(z) = [x|\dom(z)$ n/a
MIS29 galois connection III $\langle x|\dom(y)+\dom(z) = \dom(z) \Rightarrow \dom(y)+ |x] \dom(z) = |x] \dom(z)$ n/a
MIS30 galois connection IV $\langle x|\dom(y)+\dom(z) = \dom(z) \Leftarrow \dom(y)+ |x] \dom(z) = |x] \dom(z)$ n/a
MIS31 Cancellation I $|x\rangle [x|\dom(y) + \dom(y) = \dom(y)$ n/a
MIS32 Cancellation II $\dom(y) + [x| |x\rangle \dom(y) = [x| |x\rangle \dom(y)$ n/a
MIS33 Cancellation III $\langle x| |x] \dom(y)+\dom(y)=\dom(y)$ n/a
MIS34 Cancellation IV $\dom(y)+|x] \langle x|\dom(y) = |x] \langle x|\dom(y)$ n/a
MIS35 diamond strictness $|x\rangle 0 = 0$ n/a
MIS36 box costrictness $|x]1=1$ n/a
MIS37 diamonds additivity $|x\rangle \dom(y)+\dom(z) = |x\rangle \dom(y) + |x\rangle \dom(z)$ n/a
MIS38 box multiplicativity $|x] \dom(y) \cdot \dom(z) = |x]\dom(y) \cdot |x] \dom(z)$ n/a
MIS39 validity of abort rule $\langle 0| \dom(x) + \dom(y) = \dom(y)$ n/a
MIS40 validity of skip rule $\langle 1| \dom(x)+\dom(x) = \dom(x)$ n/a
MIS41 validity of composition rule $\forall a \forall b (\langle a| \dom(x) + \dom(y) = \dom(y) & \langle b|\dom(y) +\dom(z) = \dom(z)) \Rightarrow \langle a \cdot b| \dom(x) + \dom(z) = \dom(z)$ n/a

Laws for Kleene Algebra

ID Name Lemma Duals
KA1 unfold equation $1+x\cdot x^*=x^*$ $1+x^*\cdot x=x^*$
KA2 reflexivity of star $1\leq x^*$ n/a
KA3 TBD $x\leq x^*$ n/a
KA4 star is closed $(x^*)^*=x^*$ n/a
KA5 TBD $x\cdot x^*\leq x^*$ $x^*\cdot x\leq x^*$
KA6 star is idempotent w.r.t. multiplication $x^*\cdot x^* = x^*$ n/a
KA7 isotony $x\leq y \Rightarrow x^*\leq y^*$ n/a
KA8 simple/short induction $x\cdot y\leq y \Rightarrow x^*\cdoty\leq y$ $y\cdot x\leq y \Rightarrow y\cdot x^*\leq y$
KA9 iteration of neutral elements $0^*=1$
$1^*=1$
n/a
KA10 star of subidentities is equal to 1 $x\leq 1 \Rightarrow x^*=1$ n/a
KA11 star sliding $(x\cdot y)^*\cdot x = x\cdot(y\cdot x)^*$ n/a
KA12 unfold for a*b $x^*\cdot y = y+(x\cdot x^*)\cdot y$ $y\cdot x^* = y+y\cdot(x^*\cdot x)$
$x^*\cdot y = y+(x^*\cdot x)\cdot y$
$y\cdot x^* = y+y\cdot(x\cdot x^*)$
KA13 TBD $(1+x)^* = x^*$ n/a
KA14 simulation theorem $x\cdot z\leq z\cdot y \Rightarrow x^*\cdot z\leq z\cdot y^*$ $z\cdot x\leq y\cdot z \Rightarrow z\cdot x^*\leq y^*\cdot z$
KA15 simple induction $x\cdot y\leq y \Rightarrow x^*\cdot y\leq y$ $y\cdot x\leq y \Rightarrow y\cdot x^*\leq y$
KA16 TBD $(y\cdot x^*)\cdot(y\cdot x^*)^*\leq x^*\cdot(y\cdot x^*)^*$ $(x^*\cdot y)^*\cdot(x^*\cdot y)\leq(x^*\cdot y)^*\cdot x^*$
KA17 TBD $(x\cdot x^*)\cdot(y\cdot x^*)^* \leq x^*\cdot(y\cdot x^*)^*$ n/a
KA18 TBD $(x\cdot x^*)\cdot(y\cdot x^*)^*+(y\cdot x^*)\cdot(y\cdot x^*)^*\leq x^*\cdot(y\cdot x^*)^*$ n/a
KA19 Church Rosser Theorem $y^*\cdot x^*\leq x^*\cdot y^* \Rightarrow (x+y)^*\leq x^*\cdot y^*$ $x^*\cdot y^*\leq y^*\cdot x^* \Rightarrow (x+y)^*\leq y^*\cdot x^*$
KA20 decomposition $(x+y)^* = x^*\cdot(y\cdot x^*)^*$ $(x+y)^* = (x^*\cdot y)^*\cdot x^*$
KA21 star sliding II $x^*\cdot x = x\cdot x^*$ n/a
KA22 TBD $y\cdot x^*\leq x^*\cdot y^* \Rightarrow y^*\cdot x^*\leq x^*\cdot y^*$ $x^*\cdot y\leq y^*\cdot x^* \Rightarrow x^*\cdot y^*\leq y^*\cdot x^*$
KA23 TBD $y\cdot x^*\leq x^*\cdot y^* \Leftarrow y^*\cdot x^*\leq x^*\cdot y^*$ $x^*\cdot y\leq y^*\cdot x^* \Leftarrow x^*\cdot y^*\leq y^*\cdot x^*$
KA24 TBD $(x+y)^*\leq (x^*\cdot y^*)^*$ n/a
KA25 TBD $y^*\cdot x^*\leq x^*\cdot y^* \Rightarrow(y^*\cdot x^*)^*\leq x^*\cdot y^*$ n/a
KA26 bubble sort $y\cdot x\leq x\cdot y \Rightarrow (x+y)^*\leq x^*\cdot y^*$ n/a
KA27 TBD $(x+y)^* = (x+y^*)^*$ n/a
KA28 TBD $(x+y)^* = (x^*+y^*)^*$ n/a
KA29 TBD $y\cdot (1+x)\leq (1+x)\cdot y^* \Leftrightarrow y\cdot x\leq (1+x)\cdot y^*$ $(1+x)\cdot y\leq y^*\cdot (1+x) \Leftrightarrow x\cdot y\leq y^*\cdot (1+x)$
KA30 TBD $x^*\cdot y^*\leq (x+y)^*$ n/a
KA31 simple simulation $x\cdot y = 0 \Rightarrow x^*\cdot y =y$ $x\cdot y = 0 \Rightarrow x\cdot y^* =x$
KA32 TBD $(x \cdot y)^* = 1 + (x \cdot (y \cdot x)^*) \cdot y$ n/a
KA33 TBD $x \cdot y + 1 \leq y \Rightarrow x^* \leq y$ n/a

Laws for Kleene Algebra with Tests

ID Name Lemma Duals
KAT1 test-iteration is 1 $p^*=1$ n/a

Laws for Kleene Algebra with Domain

ID Name Lemma Duals
KAD1 domain versus star $\dom(x^*)=1$ $\cod(x^*)=1$
KAD2 domain of star $\dom(x^*) = 1$ n/a

Laws for Modal Kleene Algebra

ID Name Lemma Duals
MKA1 TBD $p+ |x\rangle |x^*\rangle p = |x^*\rangle p$ $p+ |x^*\rangle |x\rangle p = |x^*\rangle p$
$p+ \langle x| \langle x^*| p = \langle x^*|p$
$p+ \langle x^*| \langle x| p = \langle x^*|p$
MKA2 TBD $|x\rangle p \leq p \Rightarrow |x^*\rangle p \leq p$ $\langle x| p \leq p \Rightarrow \langle x^*|p \leq p$
MKA3 TBD $q + |x\rangle p \leq p \Rightarrow |x^*\rangle q \leq p$ $q + \langle x|p \leq p \Rightarrow \langle x^*|q \leq p$
MKA4 Segerberg's induction axiom $|x^*\rangle p\cdot \neg p \leq |x^*\rangle (|x\rangle p\cdot \neg p)$ n/a
MKA5 two notions of termination $div(x)=0 \Leftarrow \forall y (\dom(y)+|x\rangle \dom(y) = |x\rangle \dom(y) \Rightarrow \dom(y)=0)$ n/a
MKA6 two notions of termination $div(x)=0 \Leftarrow (\forall y \dom(y)+|x^* \rangle (\dom(y) - |x \rangle \dom(y)) = |x^*\rangle (\dom(y) - |x\rangle \dom(y)))$ n/a
MKA7 Loeb's formula and wellfoundedness $((\forall y (\dom(y)+|x^*\rangle (\dom(y) - |x\rangle \dom(y)) = |x^*\rangle (\dom(y) - |x\rangle \dom(y))) & (\forall y (|x\rangle |x\rangle \dom(y)) = |x\rangle \dom(y))) \Rightarrow (\forall y ( |x\rangle \dom(y) + |x^*\rangle (\dom(y) - |x\rangle \dom n/a

Laws for Omega Algebra

ID Name Lemma Duals
OA1 isotonicity of omega $x\leq y \Rightarrow x^\omega\leq y^\omega$ n/a
OA2 simple induction law $y\leq x\cdot y \Rightarrow y\leq x^\omega$ n/a
OA3 infinite iteration of zero $0^\omega=0$ n/a
OA4 greatest element $x\leq 1^\omega$ n/a
OA5 unfold laws $x\cdot x^*\cdot x^\omega = x^\omega$
$x^*\cdot x^\omega = x^\omega$
n/a
OA6 TBD $(x\cdot x^*)^\omega = x^\omega$ n/a
OA7 star versus omega I $(x^*)^\omega = 1^\omega$ n/a
OA8 star versus omega II $(x^\omega)^* = 1+x^\omega$ n/a
OA9 another unfold $x^\omega\cdot(x^\omega)^* = x^\omega$ n/a
OA10 TBD $x^\omega\cdot y\leq x^\omega$ n/a
OA11 left annihilator $x^\omega\cdot 1^\omega = x^\omega$ n/a
OA12 TBD $(x^\omega)^\omega\leq x^\omega$ n/a
OA13 TBD $(x+y)^\omega = (x^*\cdot y)\cdot (x+y)^\omega + x^\omega$ n/a
OA14 TBD $(x+y)^\omega = (x^*\cdot y)^\omega+(x^*\cdot y)^*\cdot x^\omega$ n/a
OA15 TBD $(x+y)^\omega = 0 \Rightarrow x^\omega+y^\omega=0$ n/a
OA16 Bachmair/Dershowitz $y\cdot x \leq x\cdot (x+y)^* \Rightarrow (x^\omega + y^\omega = 0 \Leftrightarrow (x+y)^\omega = 0). $ n/a
OA17 a simulation law $x \cdot y \leq z \cdot x \Rightarrow x \cdot y^\omega \leq z^\omega$ n/a
OA18 x^ is left ideal $x^\omega = x^\omega \cdot 1^\omega$ n/a

Laws for Omega Algebra with Tests

ID Name Lemma Duals
OAT1 iteration of tests $p^\omega = p\cdot 1^\omega$ n/a

Laws for Left I-Semiring

ID Name Lemma Duals
LIS1 join splitting $x+y \leq z \Leftrightarrow x \leq z \wedge y\leq z$ n/a
LIS2 weak form of right distributivity $y+z \leq w \Rightarrow x\cdot y + x\cdot z \leq x\cdot w$ n/a
LIS3 non-termination is equivalent to absence of terminating elements $(\forall y (x\cdot y = x)) \Leftrightarrow x\cdot 0 = x$ n/a
LIS4 equivalence between |N| = 1 and multiplication is right-strict $(\forall y (y\cdot 0 = 0)) \Leftrightarrow (\forall x ((\forall y (x\cdot y = x)) \Rightarrow x = 0))$ n/a
LIS5 equivalence between |N| = 1 and $\top \cdot 0 = 0$ $(\forall x ((\forall y (x\cdot y = x)) \Rightarrow x= 0)) \Leftrightarrow \top\cdot 0 = 0$ n/a
LIS6 equivalence of $\top;0 = 0$ and multiplication is right-strict $\top\cdot 0 = 0 \Leftrightarrow \forall x (x\cdot0 \leq 0)$ n/a
LIS7 towards upward closedness of the set N $(\forall y (x\cdot y = x) \wedge x \leq z) \Rightarrow x\cdot 0 \leq z\cdot 0$ n/a
LIS8 finite computations are closed unter choice (set theoretic) $(x\cdot 0 = 0 \wedge y\cdot 0 = 0) \Rightarrow (x + y)\cdot 0 = 0$ n/a
LIS9 terminating computations are closed under choice $x\cdot 0=0 \wedge x\neq 0 \wedge y\cdot 0=0 \wedge y\neq 0 -> (x+y)\cdot 0 = 0 \wedge x+y\neq 0$ n/a
LIS10 finite computations areclosed under composition $x\cdot 0 = 0 \wedge y\cdot 0 = 0 \Rightarrow (x\cdot y)\cdot 0 = 0$ n/a
LIS11 zero the only finite and infinite element $(\forall y (x\cdot y = x)) \wedge (x\cdot 0 = 0) \Rightarrow x = 0$ n/a
LIS12 splitting I $x\cdot y = \inf(x) + \fin(x)\cdot y$ n/a
LIS13 lazy-additivity of multiplication $\inf(x\cdot y) = \inf(x) + \fin(x)\cdot \inf(y)$ n/a
LIS14 fin-splitting w.r.t. multiplication $\fin(x\cdot y) = \fin(\fin(x)\cdot y)$ n/a
LIS15 semi-additivity of multiplication $\fin(x) \cdot \fin(y) \leq \fin(x \cdot y)$
$\fin(x) \cdot \fin(y) \leq \fin(\fin(x) \cdot y)$
n/a
LIS16 if f,g weakly partition K then f is a kernel operation $f(x)\leq x$
$f(x)=f(f(x))$
n/a
LIS17 TBD $x = f(x) \Leftrightarrow g(x) = 0$ n/a
LIS18 if f,g strongly partition thsn g-parts of elements are ignored by f $f(g(x)+y) = f(y)$ n/a
LIS19 if f,g strongly partition K then f is uniquely defined by g $y=g(y) + x \wedge x = f(x) \Rightarrow x = f(y)$ n/a
LIS20 If there is a least element and f is kernel function then f is strict $0 \leq x \Rightarrow f(0) = 0$ n/a
LIS21 Kernel functions are closed under addition $f(f(x) + f(y)) = f(x) + f(y)$ n/a
LIS22 fin and inf are disjoint $y\leq \fin(x) \wedge y\leq \inf(x) \Rightarrow y=0$ n/a
LIS23 properties of F and N $1\leq \F$
$\F+\N=\top$
$\F\cdot \F =\F$
$\N = \top\cdot 0$
n/a
LIS24 if residuals exist then F=0/0 $\F=0/0$ n/a
LIS25 TBD $y\leq x \wedge y \leq 0/0 \Leftrightarrow y\leq \fin(x)$ n/a

Laws for Left Kleene Algebra

ID Name Lemma Duals
LKA1 TBD $x \leq x^*$ n/a
LKA2 Idempotence I $(x^*)^* = x^*$ n/a
LKA3 Idempotence II $x^*\cdot x^* = x^*$ n/a
LKA4 unfold can be strengthend to an equality $x^*\leq 1 + x\cdot x^*$ n/a
LKA5 decomposition $(x + y)^* = x^*\cdot (y\cdot x^*)^*$ n/a
LKA6 semicommutation $x\cdot y \leq y\cdot z \Rightarrow x^*\cdot y \leq y\cdot z^*$ n/a
LKA7 semi-selfcommutation I $x^*\cdot x \leq x\cdot x^*$ n/a
LKA8 semi-sliding I $(x\cdot y)^*\cdot x \leq x\cdot(y\cdot x)^*$ n/a
LKA9 right star unfold $1 + x^*\cdot x \leq x^*$ n/a
LKA10 semi-selfcommutation II $x\cdot x^* \leq x^*\cdot x$ n/a
LKA11 right unfold II $x^* \leq 1+x^*\cdot x$ n/a
LKA12 semi-sliding II $x\cdot (y\cdot x)^* \leq (x\cdot y)^*\cdot x$ n/a
LKA13 finite elements are closed under star $x\leq \F \Leftrightarrow x^*\leq\F$ n/a
LKA14 star splitting $x^* = \fin(x)^*\cdot (1+\inf(x))$ n/a
LKA15 TBD $\inf(x^*) = \fin(x)^*\cdot\inf(x)$ n/a
LKA16 TBD $x\cdot \fin(x)^*\cdot \inf(x) = \fin(x)^*\cdot \inf(x)$ n/a

Laws for Demonic Refinement Algebra

ID Name Lemma Duals
DRA1 top element $x\leq 1^\infty$ n/a
DRA2 strong iteration of zero $0^\infty=1$ n/a
DRA3 right unfold $x^\infty = x^\infty\cdot x+1$ n/a
DRA4 isotonicity of strong iteration $x\leq y \Rightarrow x^\infty\leq y^\infty$ n/a
DRA5 top is left annihilator $1^\infty\cdot x = 1^\infty$ n/a
DRA6 infinitity of intfinity is magic $(x^\infty)^\infty = 1^\infty$ n/a
DRA7 strong iteration is idempotent w.r.t. multiplication $x^\infty\cdot x^\infty = x^\infty$ n/a
DRA8 strong iteration over iteration is magic $(x^*)^\infty = 1^\infty$ n/a
DRA9 strong iteration dominates iteration $(x^\infty)^* = x^\infty$ n/a
DRA10 strong iteration is a superidentity $1\leq x^\infty$ n/a
DRA11 an unfold law $x^*\cdot x^\infty = x^\infty$ $x^\infty\cdot x^* = x^\infty$
DRA12 an unfold law $(x^*\cdot y)^\infty = y^*\cdot(x^*\cdot y)^\infty$ n/a
DRA13 simple simulation $x\cdot y =0 \Rightarrow x\cdot y^\infty =x$ n/a
DRA14 the simple inequality of Church Rosser $x^\infty\cdot y^\infty \leq (x+y)^\infty$ n/a
DRA15 special unfold $(x+y)^\infty = y^*\cdot x\cdot (x+y)^\infty + y^\infty$ n/a
DRA16 strong iteration of special elements $(x\cdot 0)^\infty = 1+x\cdot 0$ n/a
DRA17 sliding I $x\cdot (y\cdot x)^\infty \leq (x\cdot y)^\infty\cdot x$ n/a
DRA18 sliding II $(x\cdot y)^\infty\cdot x\leq x\cdot (y\cdot x)^\infty$ n/a
DRA19 denest I $(x+y)^\infty = x^\infty\cdot(y\cdot x^\infty)^\infty$ n/a
DRA20 denest II $(x+y)^\infty\leq (x^*\cdot y)^\infty\cdot x^\infty$ n/a
DRA21 denest IIa $(x^*\cdot y)^\infty\cdot x^\infty\leq (x+y)^\infty$ n/a
DRA22 bubble sort w.r.t. star $y\cdot x\leq x\cdot y \Rightarrow (x+y)^*\leq x^*\cdot y^*$ n/a
DRA23 bubble sort w.r.t. strong iteration $y\cdot x\leq x\cdot y \Rightarrow (x+y)^\infty\leq x^\infty\cdot y^\infty$ n/a
DRA24 simulation w.r.t. strong iteration $z\cdot x\leq y\cdot z \Rightarrow z\cdot x^\infty\leq y^\infty\cdot z$ n/a
DRA25 simulation w.r.t. star I $z\cdot x\leq y\cdot z \Rightarrow z\cdot x^*\leq y^*\cdot z$ n/a
DRA26 simulation w.r.t. star II $x\cdot z\leq z\cdot y \Leftarrow x^*\cdot z\leq z\cdot y^*$ n/a
DRA27 a classical refinement law $s'\leq s\cdot z,\; z\cdot e'\leq e,\; z\cdot a'\leq a\cdot z,\; z\cdot b\leq b,\; b^\infty=b^*$
$\Rightarrow s'\cdot(a'+b)^\infty\cdot e'\leq s\cdot a^\infty\cdot e$
n/a
DRA28 towards Back's Atomicity Refinement Theory (step I) $s=sq,\; a=qa,\; qb = 0$
$\Rightarrow s(a+b)^\infty q\leq s(a\cdot b^\infty q)^\infty$
n/a
DRA29 towards Back's Atomicity Refinement Theory (step II) $s=sq,\; a=qa,\; qb = 0,\; (a+b)l\leq l(a+b),\; ql\leq lq,\; q\leq 1$
$\Rightarrow s(a+b+l)^\infty q\leq s(ab^\inftyq+l)^\infty$
n/a
DRA30 Back's Atomicity Refinement Theory (part I) $s\leq sq,\; a\leq qa,\; qb=0,\; (a+b+r)l\leq l(a+b+r),\; ql\leq lq,\; rb\leq br,\; rq\leq qr,\; r^\infty=r^*$
$\Rightarrow s(a+b+r+l)^\infty q\leq sl^\infty qr^\infty q(ab^\infty qr^\infty)^\infty$
n/a
DRA31 Back's Atomicity Refinement Theory (part II) $s\leq sq,\; a\leq qa,\; qb=0,\; (a+b+r)l\leq l(a+b+r),\; ql\leq lq,\; rb\leq br,\; rq\leq qr,\; r^\infty=r^*,\; q\leq 1$
$\Rightarrow sl^\infty qr^\infty q(ab^\infty qr^\infty)^\infty \leq s(ab^\infty q+r+l)^\infty$
n/a
DRA32 a refinement law $y\cdot x \leq x\cdot (x+y)^\infty \Rightarrow (x+y)^\infty= x^\infty\cdot y^\infty$ n/a
DRA33 TBD $ (x+y)^\infty\cdot 0 =0 \Rightarrow x^\infty\cdot 0+y^\infty\cdot 0=0$ n/a
DRA34 TBD $ y\cdot x \leq x\cdot (x+y)^\infty \Rightarrow ((x+y)^\infty\cdot 0 =0 \Leftarrow x^\infty\cdot 0+y^\infty\cdot 0=0)$ n/a
DRA35 star sliding $(x \cdot y)^* \cdot x = x \cdot (y \cdot x)^*$ n/a
DRA36 decomposition $(x+y)^* = x^* \cdot (y \cdot x^*)^*$ n/a
DRA37 TBD $(x+y)^\omega = (x^* \cdot y)^\omega \cdot x^\omega$ n/a
DRA38 special decomposition $(x+y)^* = y^* \cdot (x \cdot (x+y)^*)+y^*$ n/a
DRA39 a simultion theorem $x \cdot y \leq y \cdot x \Rightarrow x^* \cdot y^* \leq y^* \cdot x^*$ n/a
DRA40 a simulation theorem $x \cdot y \leq y \cdot x \Rightarrow x^\omega \cdot y^\omega \leq y^\omega \cdot x^\omega$ n/a
DRA41 simple simulation law w.r.t. star $x \cdot y = 0 \Rightarrow x \cdot y^* = x$ n/a
DRA42 simple simulation law $x \cdot y = 0 \Rightarrow x \cdot y^\omega = x$ n/a

Laws for Boolean Algebra

ID Name Lemma Duals
BA1 existence of a greatest element $x+\overline{x} = y+\overline{y}$ n/a
BA2 involution of complementation $\overline{\overline{x}}=x$ n/a
BA3 TBD $\overline{x}=\overline{x+y}+\overline{x+\overline{y}}$ n/a
BA4 TBD $x+(y+\overline{y})=z+\overline{z}$ n/a
BA5 TBD $x+x=x+\overline{y+\overline{y}}$ n/a
BA6 idempotence of join $x+x=x$ n/a
BA7 idempotence of meet $x\meet x=x$ n/a
BA8 commutativity of meet $x\meet y=y\meet x$ n/a
BA9 associtivity of meet $(x\meet y)\meet z=x\meet (y\meet z)$ n/a
BA10 absorption $(x+y)\meet x = x$ n/a
BA11 TBD $x=(x\meet y)+(x\meet\overline{y})$ n/a
BA12 TBD $x=(x+\overline{y})\meet(x+y)$ n/a
BA13 TBD $(x+y)\meet\overline{x} = y\meet\overline{x}$ n/a
BA14 TBD $x+(x\meet y) = x$ n/a
BA15 distributivity $x\meet(y+z) = (x\meet y)+(x\meet z)$ n/a
BA16 de Morgan I $\overline{x+y} = \overline{x}\meet\overline{y}$ n/a
BA17 de Morgan II $\overline{x\meet y} = \overline{x}+\overline{y}$ n/a
BA18 distributivity $x+(y\meet z) = (x+y)\meet (x+z)$ n/a
BA19 TBD $(\overline{x}\meet y)+(x\meet z) = (x+y)\meet (\overline{x}+z)$ n/a
BA20 TBD $((v\meet w)+(\overline{v}\meet x))\meet \overline{(v\meet y)+(\overline{v}\meet z)} = (v\meet w\meet \overline{y})+(\overline{v}\meet x\meet \overline{z})$ n/a
BA21 TBD $x+y = x+(\overline{x}\meet y)$ n/a
BA22 properties of $0$ and $\top$ $\overline{\top}=0$
$\overline{0}=\top$
$x+\top=\top$
$x\meet 0=0$
$x+0=x$
$x\meet\top=x$
n/a
BA23 $\leq$ is a partial order $x\leq x$
$(x\leq y\wedge y\leq z \Rightarrow x\leq z)$
$(x\leq y\,\wedge\,y\leq x \Rightarrow x=y)$
n/a
BA24 $0$ is least and $\top$ greatest element $0\leq x \,\wedge\, x\leq\top$ n/a
BA25 isotonicity w.r.t. meet and join $x\leq y \Rightarrow x+z\leq y+z$
$x\leq y \Rightarrow x\meet z\leq y\meet z$
$x\leq y \Rightarrow z+x\leq z+y$
$x\leq y \Rightarrow z\meet x\leq z\meet y)$
BA26 equivalence I (antitonicity of complement) $x\leq y \Leftrightarrow \overline{y}\leq\overline{x}$ n/a
BA27 equivalence II $ \overline{y}\leq\overline{x}\Leftrightarrow x+y=y$ n/a
BA28 equivalence III $x+y=y \Leftrightarrow x\meet y=x$ n/a
BA29 equivalence IV $x\meet y=x \Leftrightarrow \overline{x}+y=\top$ n/a
BA30 equivalence V $\overline{x}+y=\top \Leftrightarrow x\meet \overline{y}=0$ n/a
BA31 splitting I $x\leq y\meet z \Leftrightarrow x\leq y \,\wedge\, x\leq z$ n/a
BA32 splitting II $x+y\leq z \Leftrightarrow x\leq z \,\wedge\, y\leq z$ n/a
BA33 shunting $x\meet z \leq y \Leftrightarrow x \leq y+\overline{z}$ n/a
BA34 shunting (another version) $x\meet \overline{z} \leq y \Leftrightarrow x \leq y+z$ n/a
BA35 existence of least element $x\meet \overline{x}=y\meet \overline{y}$ n/a
BA36 Maddux's axioms $x+y = y+x$
$x+(y+z) = (x+y)+z$
$x = \overline{\overline{x} + \overline{y}}+\overline{\overline{x}+y}$
$x\meet y = \overline{\overline{x}+\overline{y}}$
n/a

Laws for Boolean Algebra with Operators

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

Laws for Relation Algebra

ID Name Lemma Duals
RA1 isotonicity wrt converse $x\leq y \Leftrightarrow x\conv \leq y\conv$ n/a
RA2 simple properties of converse $0\conv = 0$
$\top\conv=\top$
$(\overline{x})\conv = \overline{(x\conv)}$
$(x\meet y)\conv = x\conv\meet y\conv$
n/a
RA3 TBD $x\conv\meet y=0 \Leftrightarrow x\meet y\conv =0$ n/a
RA4 converse of 1 $1\conv = 1$ n/a
RA5 distributivity of composition over addition $x;(y\join z) = x;y \join x;z$ $(x\join y);z = x;z \join y;z$
RA6 isotonicity wrt. composition $x\leq y \Rightarrow (x;z\leq y;z\; \wedge\; z;x\leq z;y)$ n/a
RA7 Schroeder I $x;y\meet z=0 \Rightarrow y\meet(x\conv;z)=0$ n/a
RA8 Schroeder II $x;y\meet z=0 \Leftarrow y\meet(x\conv;z)=0$ n/a
RA9 TBD $\overline{y;x};x\conv \leq \overline{y}$ n/a
RA10 annihilation $x;0=0$
$0;x=0$
n/a
RA11 properties of identity $x;1=x \;\wedge\;1;x=x$ n/a
RA12 properties for top $x\leq x;\top$
$x\leq \top;x$
$\top;\top=\top$
n/a
RA13 TBD $x;y\meet\overline{x;z} = x;(y\meet\overline{z})\meet \overline{x;z}$ n/a
RA14 TBD $\overline{x;y} \join x;z = \overline{x;(y\meet \overline{z})}+x;z$ n/a
RA15 TBD $x;\top=x \Rightarrow \overline{x};\top=\overline{x}$ n/a
RA16 TBD $x;\top=x\,\wedge\, y;\top=y \Rightarrow (x\meet y);\top=x\meet y$ n/a
RA17 TBD $x;\top=x \Rightarrow (x\meet 1);y = x\meet y$ n/a
RA18 TBD $x;\top=x \Rightarrow (y\meet x\conv);(x\meet z) \leq y;(x\meet z)\,\wedge\, (y\meet x\conv);(x\meet z) \leq (y\meet x\conv);z$ n/a
RA19 TBD $x\leq 1 \Rightarrow x\conv = x$ n/a
RA20 TBD $x\leq 1 \Rightarrow (x;\top)\meet y=x;y$ n/a
RA21 TBD $x\leq 1 \Rightarrow \overline{x;\top}\meet 1 = \overline{x}\meet 1$ n/a
RA22 TBD $x\leq 1\,\wedge\, y\leq1 \Rightarrow x;y=x\meet y$ n/a
RA23 distributivity $x \leq 1\,\wedge\, y \leq 1 \Rightarrow (x;z\meet y;z) = (x\meet y);z$ n/a
RA24 TBD $x\leq 1 \Rightarrow (x;y)\meet\overline{z} = (x;y)\meet\overline{x;z}$ n/a
RA25 functions are preserved under composition $x\conv;x\leq 1\,\wedge\, y\conv;y\leq 1\Rightarrow (x;y)\conv;(x;y)\leq 1$ n/a
RA26 subdistributivity $x;(y\meet z) + (x;y\meet x;z)=(x;y\meet x;z)$ n/a
RA27 TBD $ x;\top=x \Rightarrow (x\meet y);z = x\meet (y;z)$ n/a
RA28 TBD $x;\top=x \Rightarrow (y\meet x\conv);(x\meet z) = y;(x\meet z)$
$x;\top=x \Rightarrow (y\meet x\conv);(x\meet z)=(y\meet x\conv);z$
n/a
RA29 modular laws $z;x\meet y \leq z;(x\meet z\conv;y)\meet y$ $x;z\meet y \leq (x\meet y;z\conv);z\meet y$
RA30 Dedekind $z;x\meet y \leq (z\meet y;x\conv);(x\meet z\conv ;y)$ n/a
RA31 distributivity $x\conv ;x\leq 1 \Rightarrow x;(y\meet z) = x;y\meet x;z$ n/a
RA32 TBD $\forall x.\, (\forall y.\, x;y\meet x;\overline{y}=0 \Leftarrow x\conv;x\leq 1)$ n/a
RA33 TBD $\forall x (\forall y x;y\meet x;\overline{y}=0 \Rightarrow x\conv;x\leq 1)$ n/a
RA34 equivalence I of x,y forms rectangle inside z $x;y\conv\leq z \Leftrightarrow \overline{z};y\leq x\conv$ n/a
RA35 equivalence II of x,y forms rectangle inside z $x;y\conv\leq z \Leftrightarrow \overline{z}\conv;x \leq\overline{y}$ n/a
RA36 fringe property I $\mbox{fringe}(x\conv) = \mbox{fringe}(x)\conv$ n/a
RA37 fringe property II If $E$ is an order, then $\mbox{fringe}(E)=1$ n/a
RA38 Exercise 9.1.1 of [Schmidt07] $(x;\top);x =x \Leftrightarrow (x;\overline{x}\conv);x=0$ n/a
RA39 Proposition 9.4.2 of [Schmidt07] $\mbox{fringe}(x) = \mbox{syq}(\overline{(\overline{x};x\conv)},x)$ n/a
RA40 properties of symmetric quotient (Prop. 7.6.1 of [Schmidt07]) $\mbox{syq}(\overline{x},\overline{y}) = \mbox{syq}(x,y)$
$\mbox{syq}(x,y)\conv = \mbox{syq}(y,x)$
n/a
RA41 properties of symmetric quotient (Prop. 7.6.2 of [Schmidt07]) $x;\mbox{syq}(x,x)\leq x$ n/a
RA42 $(\overline{x;\overline{x}\conv;x})\conv$ is the greatest subinverse of $x$ (Lemma 9.5.4 of [Schmidt07]) $x;y;x\leq x \Leftrightarrow y\leq\overline{(x;\overline{x}\conv;x)}\conv$ n/a
RA43 Moore-Penrose inverses are uniquely determined provided they exist. (Lemma 9.5.8 of [Schmidt07]) $(x;y;x=x \wedge y;x;y=y \wedge (x;y)\conv =x;y \wedge (y;x)\conv=y;x \wedge x;z;x=x \wedge z;x;z=z \wedge (x;z)\conv=x;z \wedge (z;x)\conv=z;x) \Rightarrow y=z$ n/a
RA44 Properties of Ferrers $\mbox{ferrers}(x) \Rightarrow \mbox{ferrers}(x\conv) \wedge \mbox{ferrers}(\overline{x}) \wedge \mbox{ferrers}(\overline{x}\conv;x)$ n/a
RA45 Properties of Ferrers $\mbox{ferrers}(x) \Rightarrow \mbox{ferrers}(\overline{x};x\conv)$ n/a
RA46 Properties of Ferrers $\mbox{ferrers}(x) \Rightarrow \mbox{ferrers}(x;\overline{x}\conv ;x)$ n/a
RA47 TBD $x;(y \meet z) = x;y \meet x;z \Rightarrow x\conv ;x \leq 1$ n/a
RA48 symmetric quotient is reflexive $1 \leq \mbox{syq}(x,x)$ n/a
RA49 isotonicity of symmentric quotient $\mbox{syq}(x,y) \leq \mbox{syq}(z;x,z;y)$ n/a
RA50 an unfold law $x \leq (x;x\conv);x$ n/a
RA51 an important property for subidentities $x \leq 1 \Rightarrow \overline{x;\top} = (1 \meet \overline{x});\top$ n/a
RA52 a prop of symmentric quotient $x\conv ;x \leq 1 \wedge 1 \leq x;x\conv \Rightarrow x;\mbox{syq}(y,z) = \mbox{syq}(y;x\conv,z)$ n/a
RA53 TBD $x;\overline{\overline{y};z} \leq \overline{\overline{x;y};z}$ n/a
RA54 some strictness property $x \neq 0 \Leftrightarrow x\conv ;x \neq 0$ n/a
RA55 complement of xT is left ideal $\overline{x;\top} = \overline{x;\top};\top$ n/a
RA56 associativity of demonic composition $\demonic(x,\demonic(y,z)) = \demonic(\demonic(x,y),z)$ n/a
RA57 consequense of the Tarski rule $(x;\top);x = x \Rightarrow (x;\overline{x}\conv);x = 0$ n/a
RA58 meet splitting $x \leq y \meet z \Leftrightarrow x \leq y \wedge x \leq z$ n/a
RA59 join splitting $x + y \leq z \Leftrightarrow x \leq z \wedge y \leq z$ n/a
RA60 relational unfold with subidentity and converse $x = (1 \meet x;x^\omega);x$ n/a

Laws for Monodic Tree Algebra

ID Name Lemma Duals
MTA1 right unfold $1 + x^*\cdot x \leq x^*$ n/a
MTA2 right monoidic unfold $1 + x^*\cdot (x+1) \leq x^*$ n/a

Laws for Feature Algebra (Product Families)

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

Laws for Feature Algebra (OOP)

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

Laws for Misc

ID Name Lemma Duals
# Feature Algebra (Object-Oriented Programming)
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