# How to Apply Elementary Axioms from Kleene Star to an Inequality

## Axioms For *

\begin{align} 1 + aa^* &\leq a^* \\ 1 + a^*a &\leq a^* \\ b + ax &\leq x \to a^*b \leq x \\ b + xa &\leq x \to ba^* \leq x \\ \end{align}

## Elementary Results

\begin{align} a \leq b &\to a + c \leq b + c \\ a \leq b &\to ac \leq bc\, \wedge\, ca \leq cb \\ a \leq b &\to a^* \leq b^* \end{align}

## Problem

Prove the following identity in a Kleene algebra using only the axioms and elementary results. $$(a + ab + b)^* = (a + b)^*$$

Solution: \begin{align} (a + b)^* &= (a + ab + b)^* \\ (a + b)^* &\leq (a + ab + b)^* \\ 1 + (a + b)(a + b)^* &\leq 1 + (a + ab + b)(a + ab + b)^* \\ (a + b)(a + b)^* &\leq (a + ab + b)(a + ab + b)^* \\ \end{align}

## Quesiton

1. So for them to be equal the sets should be contained in each other. At which point do I transition to an inequality?

2. Is it right to say a $$*$$ cannot be removed since it has no inverse?

3. Can I distribute into a $$*$$? Say $$(a +b)(a + b)^*$$ or do they need to have the same $$*$$ height?

Some hints to get further would be greatly appreciated.

I assume that in your definition $$a \leq b$$ iff $$a + b = b$$.

First, note that if $$a \leq b$$ and $$b \leq a$$, then $$a = a + b = b + a = b$$. Therefore, in order to show that $$a = b$$, it is sufficient to show that $$a \leq b$$ and $$b \leq a$$.

Now, you want to show that $$(a + b)^\ast = (a + ab + b)^\ast$$. As explained in the previous paragraph, it is sufficient to show that inequalities with $$\leq$$ in both directions hold ("[...] for them to be equal the sets should be contained in each other").

The inequality $$(a + b)^\ast \leq (a + ab + b)^\ast$$ is almost trivial:

$$(a + b) + ab = a + ab + b$$

therefore $$(a + b) \leq (a + ab + b)$$, and by monotonicity (your ER-3), it thus holds

$$(a + b)^\ast \leq (a + ab + b)^\ast.$$

The other direction is a bit trickier.

By monotonicity (ER-2), (def-$$\leq$$), (Ax-1):

$$a(a + b)^\ast \leq (a + b)(a + b)^\ast \leq 1 + (a + b)(a + b)^\ast \leq (a+b)^\ast$$

Analogously, $$b(a + b)^\ast \leq (a+b)^\ast$$.

From both previous statements, again using monotonicity (ER-2):

$$ab(a+b)^\ast \leq a(a+b)^\ast \leq (a+b)^\ast.$$

To summarize: so far, we know that $$a$$,$$b$$ and $$ab$$ are all $$\leq (a+b)^\ast$$.

Now, observe that from (ER-1), it follows that if $$x \leq w$$ and $$y \leq w$$, then $$x + y \leq w + y \leq w + w = w$$. Thus, from $$a\leq (a + b)^\ast$$, $$ab \leq (a + b)^\ast$$ and $$b \leq (a + b)^\ast$$, you obtain:

$$(a + ab + b)(a+b)^\ast = a(a+b)^\ast + ab(a+b)^\ast + b(a+b)^\ast \leq (a + b)^\ast.$$

Since additionally $$1 \leq (a+b)^\ast$$ (directly from Ax-1), you obtain:

$$1 + (a + ab + b)(a+b)^\ast \leq (a+b)^\ast.$$

With (Ax-3) it follows:

$$(a + ab + b)^\ast = 1\cdot(a + ab + b)^\ast \leq (a + b)^\ast$$

Thus, both inequalities hold, hence we get the equality.

You cannot simply "remove" $$^\ast$$, nothing is told about "inverse" in the definition of a Kleene algebra. I also don't know what you mean by "$$\ast$$-height".

• So this expression $(a+b)+ab=a+ab+b$ you can use to deduce $(a+b)\leq(a+ab+b)$. I understand this but I just wonder if it is ok since we did not arrive there by manipulating the equation? This is why I was asking if is was possible to remove a $*$. For 3. I meant to say do the both need to have the same amount of stars so I can distribute say $(a+b)*(a+b)∗$ instead of $(a+b)(a+b)∗$? Thanks so much for your answer. Oct 7, 2018 at 2:03
• @grant2088 "$(a + b) + ab = a + ab + b$ hence $(a + b)\leq(a + ab + b)$" holds by definition of $\leq$, it's a zero-step "deduction". The "amount of stars" doesn't matter, because the closure operation is idemponent - either there is a star, or there isn't. But you can, of course, distribute $(a +b)c$ into $ac + bc$, again, by definition. As you can see, the list of properties in the Wiki is way longer than your 4 axioms. Oct 7, 2018 at 11:34
• Neither $+$ nor $\cdot$ distributes particularly well over the $\bullet^\ast$, e.g. $(a + b)^\ast c \neq a^\ast c + b ^\ast c$, or anything of that kind. Oct 7, 2018 at 11:35