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
LIS1	join splitting	$x+y \leq z \Leftrightarrow x \leq z \wedge y\leq z$	n/a
LIS2	weak form of right distributivity	$y+z \leq w \Rightarrow x\cdot y + x\cdot z \leq x\cdot w$	n/a
LIS3	non-termination is equivalent to absence of terminating elements	$(\forall y (x\cdot y = x)) \Leftrightarrow x\cdot 0 = x$	n/a
LIS4	equivalence between |N| = 1 and multiplication is right-strict	$(\forall y (y\cdot 0 = 0)) \Leftrightarrow (\forall x ((\forall y (x\cdot y = x)) \Rightarrow x = 0))$	n/a
LIS5	equivalence between |N| = 1 and $\top \cdot 0 = 0$	$(\forall x ((\forall y (x\cdot y = x)) \Rightarrow x= 0)) \Leftrightarrow \top\cdot 0 = 0$	n/a
LIS6	equivalence of $\top;0 = 0$ and multiplication is right-strict	$\top\cdot 0 = 0 \Leftrightarrow \forall x (x\cdot0 \leq 0)$	n/a
LIS7	towards upward closedness of the set N	$(\forall y (x\cdot y = x) \wedge x \leq z) \Rightarrow x\cdot 0 \leq z\cdot 0$	n/a
LIS8	finite computations are closed unter choice (set theoretic)	$(x\cdot 0 = 0 \wedge y\cdot 0 = 0) \Rightarrow (x + y)\cdot 0 = 0$	n/a
LIS9	terminating computations are closed under choice	$x\cdot 0=0 \wedge x\neq 0 \wedge y\cdot 0=0 \wedge y\neq 0 -> (x+y)\cdot 0 = 0 \wedge x+y\neq 0$	n/a
LIS10	finite computations areclosed under composition	$x\cdot 0 = 0 \wedge y\cdot 0 = 0 \Rightarrow (x\cdot y)\cdot 0 = 0$	n/a
LIS11	zero the only finite and infinite element	$(\forall y (x\cdot y = x)) \wedge (x\cdot 0 = 0) \Rightarrow x = 0$	n/a
LIS12	splitting I	$x\cdot y = \inf(x) + \fin(x)\cdot y$	n/a
LIS13	lazy-additivity of multiplication	$\inf(x\cdot y) = \inf(x) + \fin(x)\cdot \inf(y)$	n/a
LIS14	fin-splitting w.r.t. multiplication	$\fin(x\cdot y) = \fin(\fin(x)\cdot y)$	n/a
LIS15	semi-additivity of multiplication	$\fin(x) \cdot \fin(y) \leq \fin(x \cdot y)$ $\fin(x) \cdot \fin(y) \leq \fin(\fin(x) \cdot y)$	n/a
LIS16	if f,g weakly partition K then f is a kernel operation	$f(x)\leq x$ $f(x)=f(f(x))$	n/a
LIS17	TBD	$x = f(x) \Leftrightarrow g(x) = 0$	n/a
LIS18	if f,g strongly partition thsn g-parts of elements are ignored by f	$f(g(x)+y) = f(y)$	n/a
LIS19	if f,g strongly partition K then f is uniquely defined by g	$y=g(y) + x \wedge x = f(x) \Rightarrow x = f(y)$	n/a
LIS20	If there is a least element and f is kernel function then f is strict	$0 \leq x \Rightarrow f(0) = 0$	n/a
LIS21	Kernel functions are closed under addition	$f(f(x) + f(y)) = f(x) + f(y)$	n/a
LIS22	fin and inf are disjoint	$y\leq \fin(x) \wedge y\leq \inf(x) \Rightarrow y=0$	n/a
LIS23	properties of F and N	$1\leq \F$ $\F+\N=\top$ $\F\cdot \F =\F$ $\N = \top\cdot 0$	n/a
LIS24	if residuals exist then F=0/0	$\F=0/0$	n/a
LIS25	TBD	$y\leq x \wedge y \leq 0/0 \Leftrightarrow y\leq \fin(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.