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
and
for
arbitrary semiring elements and
for tests. If other letters are involved we
adapted the original notation of the authors.