Laws for 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
KA1 unfold equation $1+x\cdot x^*=x^*$ $1+x^*\cdot x=x^*$
KA2 reflexivity of star $1\leq x^*$ n/a
KA3 TBD $x\leq x^*$ n/a
KA4 star is closed $(x^*)^*=x^*$ n/a
KA5 TBD $x\cdot x^*\leq x^*$ $x^*\cdot x\leq x^*$
KA6 star is idempotent w.r.t. multiplication $x^*\cdot x^* = x^*$ n/a
KA7 isotony $x\leq y \Rightarrow x^*\leq y^*$ n/a
KA8 simple/short induction $x\cdot y\leq y \Rightarrow x^*\cdoty\leq y$ $y\cdot x\leq y \Rightarrow y\cdot x^*\leq y$
KA9 iteration of neutral elements $0^*=1$
KA10 star of subidentities is equal to 1 $x\leq 1 \Rightarrow x^*=1$ n/a
KA11 star sliding $(x\cdot y)^*\cdot x = x\cdot(y\cdot x)^*$ n/a
KA12 unfold for a*b $x^*\cdot y = y+(x\cdot x^*)\cdot y$ $y\cdot x^* = y+y\cdot(x^*\cdot x)$
$x^*\cdot y = y+(x^*\cdot x)\cdot y$
$y\cdot x^* = y+y\cdot(x\cdot x^*)$
KA13 TBD $(1+x)^* = x^*$ n/a
KA14 simulation theorem $x\cdot z\leq z\cdot y \Rightarrow x^*\cdot z\leq z\cdot y^*$ $z\cdot x\leq y\cdot z \Rightarrow z\cdot x^*\leq y^*\cdot z$
KA15 simple induction $x\cdot y\leq y \Rightarrow x^*\cdot y\leq y$ $y\cdot x\leq y \Rightarrow y\cdot x^*\leq y$
KA16 TBD $(y\cdot x^*)\cdot(y\cdot x^*)^*\leq x^*\cdot(y\cdot x^*)^*$ $(x^*\cdot y)^*\cdot(x^*\cdot y)\leq(x^*\cdot y)^*\cdot x^*$
KA17 TBD $(x\cdot x^*)\cdot(y\cdot x^*)^* \leq x^*\cdot(y\cdot x^*)^*$ n/a
KA18 TBD $(x\cdot x^*)\cdot(y\cdot x^*)^*+(y\cdot x^*)\cdot(y\cdot x^*)^*\leq x^*\cdot(y\cdot x^*)^*$ n/a
KA19 Church Rosser Theorem $y^*\cdot x^*\leq x^*\cdot y^* \Rightarrow (x+y)^*\leq x^*\cdot y^*$ $x^*\cdot y^*\leq y^*\cdot x^* \Rightarrow (x+y)^*\leq y^*\cdot x^*$
KA20 decomposition $(x+y)^* = x^*\cdot(y\cdot x^*)^*$ $(x+y)^* = (x^*\cdot y)^*\cdot x^*$
KA21 star sliding II $x^*\cdot x = x\cdot x^*$ n/a
KA22 TBD $y\cdot x^*\leq x^*\cdot y^* \Rightarrow y^*\cdot x^*\leq x^*\cdot y^*$ $x^*\cdot y\leq y^*\cdot x^* \Rightarrow x^*\cdot y^*\leq y^*\cdot x^*$
KA23 TBD $y\cdot x^*\leq x^*\cdot y^* \Leftarrow y^*\cdot x^*\leq x^*\cdot y^*$ $x^*\cdot y\leq y^*\cdot x^* \Leftarrow x^*\cdot y^*\leq y^*\cdot x^*$
KA24 TBD $(x+y)^*\leq (x^*\cdot y^*)^*$ n/a
KA25 TBD $y^*\cdot x^*\leq x^*\cdot y^* \Rightarrow(y^*\cdot x^*)^*\leq x^*\cdot y^*$ n/a
KA26 bubble sort $y\cdot x\leq x\cdot y \Rightarrow (x+y)^*\leq x^*\cdot y^*$ n/a
KA27 TBD $(x+y)^* = (x+y^*)^*$ n/a
KA28 TBD $(x+y)^* = (x^*+y^*)^*$ n/a
KA29 TBD $y\cdot (1+x)\leq (1+x)\cdot y^* \Leftrightarrow y\cdot x\leq (1+x)\cdot y^*$ $(1+x)\cdot y\leq y^*\cdot (1+x) \Leftrightarrow x\cdot y\leq y^*\cdot (1+x)$
KA30 TBD $x^*\cdot y^*\leq (x+y)^*$ n/a
KA31 simple simulation $x\cdot y = 0 \Rightarrow x^*\cdot y =y$ $x\cdot y = 0 \Rightarrow x\cdot y^* =x$
KA32 TBD $(x \cdot y)^* = 1 + (x \cdot (y \cdot x)^*) \cdot y$ n/a
KA33 TBD $x \cdot y + 1 \leq y \Rightarrow x^* \leq y$ 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