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.)
 ID Name Lemma Duals MTA1 right unfold $1 + x^*\cdot x \leq x^*$ n/a MTA2 right monoidic unfold $1 + x^*\cdot (x+1) \leq x^*$ 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.