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
and
for
arbitrary semiring elements and
for tests. If other letters are involved we
adapted the original notation of the authors.