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 |
©2007. Peter Höfner |