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
LKA1	TBD	$x \leq x^*$	n/a
LKA2	Idempotence I	$(x^*)^* = x^*$	n/a
LKA3	Idempotence II	$x^*\cdot x^* = x^*$	n/a
LKA4	unfold can be strengthend to an equality	$x^*\leq 1 + x\cdot x^*$	n/a
LKA5	decomposition	$(x + y)^* = x^*\cdot (y\cdot x^*)^*$	n/a
LKA6	semicommutation	$x\cdot y \leq y\cdot z \Rightarrow x^*\cdot y \leq y\cdot z^*$	n/a
LKA7	semi-selfcommutation I	$x^*\cdot x \leq x\cdot x^*$	n/a
LKA8	semi-sliding I	$(x\cdot y)^*\cdot x \leq x\cdot(y\cdot x)^*$	n/a
LKA9	right star unfold	$1 + x^*\cdot x \leq x^*$	n/a
LKA10	semi-selfcommutation II	$x\cdot x^* \leq x^*\cdot x$	n/a
LKA11	right unfold II	$x^* \leq 1+x^*\cdot x$	n/a
LKA12	semi-sliding II	$x\cdot (y\cdot x)^* \leq (x\cdot y)^*\cdot x$	n/a
LKA13	finite elements are closed under star	$x\leq \F \Leftrightarrow x^*\leq\F$	n/a
LKA14	star splitting	$x^* = \fin(x)^*\cdot (1+\inf(x))$	n/a
LKA15	TBD	$\inf(x^*) = \fin(x)^*\cdot\inf(x)$	n/a
LKA16	TBD	$x\cdot \fin(x)^*\cdot \inf(x) = \fin(x)^*\cdot \inf(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.