Laws for Modal Kleene Algebra

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

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