Laws for Left 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
LOA1 existence of greatest element $\top = 1^\omega$ n/a
LOA2 isotony w.r.t. omega $x\leq y \Rightarrow x^\omega \leq y^\omega$ n/a
LOA3 omega star unfold $x^*\cdot x^\omega = x^\omega$ n/a
LOA4 $x^\omega$ is right ideal $x^\omega = x^\omega\cdot\top$ n/a
LOA5 TBD $x^\omega = \fin(x)^*\cdot \inf(x) + \fin(x)^\omega$ n/a
LOA6 TBD $\fin(x) = 0 \Rightarrow x^\omega = x$ 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