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
KAD1	domain versus star	$\dom(x^*)=1$	$\cod(x^*)=1$
KAD2	domain of star	$\dom(x^*) = 1$	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.