Laws for Modal I-Semiring

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

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