All presented properties are showed by automated theorem-prover Prover9.
ID |
Name |
Lemma |
Duals |
OA1 |
isotonicity of omega |
$x\leq y \Rightarrow x^\omega\leq y^\omega$ |
n/a |
OA2 |
simple induction law |
$y\leq x\cdot y \Rightarrow y\leq x^\omega$ |
n/a |
OA3 |
infinite iteration of zero |
$0^\omega=0$ |
n/a |
OA4 |
greatest element |
$x\leq 1^\omega$ |
n/a |
OA5 |
unfold laws |
$x\cdot x^*\cdot x^\omega = x^\omega$ $x^*\cdot x^\omega = x^\omega$ |
n/a |
OA6 |
TBD |
$(x\cdot x^*)^\omega = x^\omega$ |
n/a |
OA7 |
star versus omega I |
$(x^*)^\omega = 1^\omega$ |
n/a |
OA8 |
star versus omega II |
$(x^\omega)^* = 1+x^\omega$ |
n/a |
OA9 |
another unfold |
$x^\omega\cdot(x^\omega)^* = x^\omega$ |
n/a |
OA10 |
TBD |
$x^\omega\cdot y\leq x^\omega$ |
n/a |
OA11 |
left annihilator |
$x^\omega\cdot 1^\omega = x^\omega$ |
n/a |
OA12 |
TBD |
$(x^\omega)^\omega\leq x^\omega$ |
n/a |
OA13 |
TBD |
$(x+y)^\omega = (x^*\cdot y)\cdot (x+y)^\omega + x^\omega$ |
n/a |
OA14 |
TBD |
$(x+y)^\omega = (x^*\cdot y)^\omega+(x^*\cdot y)^*\cdot x^\omega$ |
n/a |
OA15 |
TBD |
$(x+y)^\omega = 0 \Rightarrow x^\omega+y^\omega=0$ |
n/a |
OA16 |
Bachmair/Dershowitz |
$y\cdot x \leq x\cdot (x+y)^* \Rightarrow (x^\omega + y^\omega = 0 \Leftrightarrow (x+y)^\omega = 0). $ |
n/a |
OA17 |
a simulation law |
$x \cdot y \leq z \cdot x \Rightarrow x \cdot y^\omega \leq z^\omega$ |
n/a |
OA18 |
x^ is left ideal |
$x^\omega = x^\omega \cdot 1^\omega$ |
n/a |
for tests. If other letters are involved we
adapted the original notation of the authors.