| 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$ $1^*=1$ |
n/a |
| 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 |
| ©2007. Peter Höfner |