Laws for Kleene Algebra with Domain

 
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.
 
©2007. Peter Höfner