Laws for Omega Algebra

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
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$
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

In general, we write x,y... and a,b... for arbitrary semiring elements and p,q... for tests. If other letters are involved we adapted the original notation of the authors.
©2007. Peter Höfner