Laws for I-Semiring with Tests

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
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

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