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.