## 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.