| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| ID | Name | Lemma | Duals |
| KAT1 | test-iteration is 1 | $p^*=1$ | n/a |
| ID | Name | Lemma | Duals |
| KAD1 | domain versus star | $\dom(x^*)=1$ | $\cod(x^*)=1$ |
| KAD2 | domain of star | $\dom(x^*) = 1$ | n/a |
| 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 |
| 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 |
| ID | Name | Lemma | Duals |
| OAT1 | iteration of tests | $p^\omega = p\cdot 1^\omega$ | n/a |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| ID | Name | Lemma | Duals |