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.