Laws for Left I-Semiring

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)$
LIS16 if f,g weakly partition K then f is a kernel operation $f(x)\leq x$
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\cdot \F =\F$
$\N = \top\cdot 0$
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.
©2007. Peter Höfner