Laws for Monodic Tree Algebra
All presented properties are showed by automated theorem-prover Prover9.
(There is no special order in the presentation of the theorems.)
||$1 + x^*\cdot x \leq x^*$
||right monoidic unfold
||$1 + x^*\cdot (x+1) \leq x^*$
In general, we write
arbitrary semiring elements and
for tests. If other letters are involved we
adapted the original notation of the authors.