Laws for Left 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
LKA1 TBD $x \leq x^*$ n/a
LKA2 Idempotence I $(x^*)^* = x^*$ n/a
LKA3 Idempotence II $x^*\cdot x^* = x^*$ n/a
LKA4 unfold can be strengthend to an equality $x^*\leq 1 + x\cdot x^*$ n/a
LKA5 decomposition $(x + y)^* = x^*\cdot (y\cdot x^*)^*$ n/a
LKA6 semicommutation $x\cdot y \leq y\cdot z \Rightarrow x^*\cdot y \leq y\cdot z^*$ n/a
LKA7 semi-selfcommutation I $x^*\cdot x \leq x\cdot x^*$ n/a
LKA8 semi-sliding I $(x\cdot y)^*\cdot x \leq x\cdot(y\cdot x)^*$ n/a
LKA9 right star unfold $1 + x^*\cdot x \leq x^*$ n/a
LKA10 semi-selfcommutation II $x\cdot x^* \leq x^*\cdot x$ n/a
LKA11 right unfold II $x^* \leq 1+x^*\cdot x$ n/a
LKA12 semi-sliding II $x\cdot (y\cdot x)^* \leq (x\cdot y)^*\cdot x$ n/a
LKA13 finite elements are closed under star $x\leq \F \Leftrightarrow x^*\leq\F$ n/a
LKA14 star splitting $x^* = \fin(x)^*\cdot (1+\inf(x))$ n/a
LKA15 TBD $\inf(x^*) = \fin(x)^*\cdot\inf(x)$ n/a
LKA16 TBD $x\cdot \fin(x)^*\cdot \inf(x) = \fin(x)^*\cdot \inf(x)$ 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