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