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 |