Laws for 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
IS1 isotony w.r.t. addition $x\leq y \Rightarrow x+z\leq y+z$ $x\leq y \Rightarrow z+x\leq z+y$
IS2 isotony w.r.t. multiplication $x\leq y \Rightarrow x\cdot z\leq y\cdot z$ $x\leq y \Rightarrow z\cdot x\leq z\cdot y$
IS3 splitting addition (supremum) $x+y\leq z \Leftrightarrow x\leq z \wedge y\leq z$ n/a
IS4 transitivity $x\leq y \wedge y\leq z \Rightarrow x\leq z$ n/a
IS5 splitting an equality into inequalities $x=y \Leftrightarrow x\leq y \wedge y\leq x$ n/a
IS6 Equivalence of idempotence and idempotence of $1$ $\forall x(x+x=x) \Leftrightarrow 1+1=1$ n/a
IS7 0 is least element $0 \leq x$ n/a
IS8 no non-trivial inverse w.r.t. addition $\forall x (x \neq 0 \Rightarrow \neg (\exists y (x+y=0)))$ 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