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

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.