Laws for I-Semiring with Domain

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
ISD1 strictness $\dom(x)=0 \Leftrightarrow x=0$ $\cod(x)=0 \Leftrightarrow x=0$
ISD2 domain of identities $\dom(0)=0\; \wedge\; \dom(1)=1$ $\cod(0)=0\; \wedge\; \cod(1)=1$
ISD3 domain of tests $\dom(p)=p$ $\cod(p)=p$
ISD4 TBD $\dom(y)\cdot\dom(x)\cdot x = \dom(y)\cdot x$ $x\cdot \cod(x)\cdot\cod(y) = x\cdot \cod(y)$
ISD5 additivity $\dom(x+y) = \dom(x)+\dom(y)$ $\cod(x+y) = \cod(x)+\cod(y)$
ISD6 domain commutes $\dom(x)\cdot\dom(y) = \dom(y)\cdot\dom(x)$ $\cod(x)\cdot\cod(y) = \cod(y)\cdot\cod(x)$
ISD7 isotonicity $x\leq y \Rightarrow \dom(x)\leq\dom(y)$ $x\leq y \Rightarrow \cod(x)\leq\cod(y)$
ISD8 idempotence of domain $\dom(\dom(x))=\dom(x)$ $\cod(\cod(x))=\cod(x)$
ISD9 test negation and domain commutes $\neg(\dom(p)) = \dom(\neg p)$ $\neg(\cod(p)) = \cod(\neg p)$
ISD10 separation $x\cdot y = 0 \Rightarrow x\cdot\dom(y)=0$ $x\cdot y = 0 \Rightarrow \cod(x)\cdot y=0$
ISD11 least left preserver $x=p\cdot x \Leftrightarrow \dom(x)\leq p$ $x=x\cdot p \Leftrightarrow \cod(x)\leq p$
ISD12 greatest left annihilator $\neg p\cdot x= 0 \Leftrightarrow \dom(x)\leq p$ $x\cdot\neg p = 0 \Leftrightarrow \cod(x)\leq p$
ISD13 TBD $\dom(x \cdot y) \leq \dom(x)$ n/a
ISD14 distributivity of update over addition $x \update (y+z) = x \update y + x \update z$ n/a
ISD15 property for update $x \update y = y \update x \Rightarrow (x+y) \update z = x \update (y \update z)$ n/a
ISD16 domain and update $\dom(x \update y) = \dom(x) + \dom(y)$ n/a
ISD17 neutrality of 0 w.r.t update $0 \update x = x$ n/a
ISD18 associativity of update $x \update (y \update z) = (x \update y) \update z$ n/a
ISD19 Idempotency $x + x = x$ n/a
ISD20 left invariant $\dom(x) \cdot x = x$ n/a
ISD21 projection $\dom (\dom (x)) = \dom (x)$ n/a
ISD22 prefix increasing $\dom(x \cdot y)+\dom(x) = \dom(x)$ n/a
ISD23 subidentity expansion $x+1 = 1 \Rightarrow x+\dom(x) = \dom(x)$ n/a
ISD24 very strictness $\dom(x) = 0 \Leftrightarrow x = 0$ n/a
ISD25 costrictness $\dom(1) = 1$ n/a
ISD26 isotonicity $x+y = y \Rightarrow \dom(x)+\dom(y) = \dom(y)$ n/a
ISD27 export $\dom(\dom(x) \cdot y) = \dom(x) \cdot \dom(y)$ n/a
ISD28 multiplicative idempotency $\dom(x) \cdot \dom(x) = \dom(x)$ n/a
ISD29 commutativity $\dom(x) \cdot \dom(y) = \dom(y) \cdot \dom(x)$ n/a
ISD30 least left preservation $x+ \dom(y) \cdot x = \dom(y) \cdot x \Leftrightarrow \dom(x)+\dom(y) = \dom(y)$ n/a
ISD31 weak locality $x \cdot y = 0 \Rightarrow x \cdot \dom(y) = 0$ n/a
ISD32 additive closure $\dom(\dom(x)+\dom(y)) = \dom(x)+\dom(y)$ n/a
ISD33 multiplicative closure $\dom(\dom(x) \cdot \dom(y)) = \dom(x) \cdot \dom(y)$ n/a
ISD34 absorption I $\dom(x) \cdot (\dom(x)+\dom(y)) = \dom(x)$ n/a
ISD35 absorption II $\dom(x)+\dom(x) \cdot \dom(y) = \dom(x)$ n/a
ISD36 first module axiom $\dom((x+y) \cdot \dom(z)) = \dom(x \cdot \dom(z))+\dom(y \cdot \dom(z))$ n/a
ISD37 second module axiom $\dom(x \cdot (\dom(y)+\dom(z))) = \dom(x \cdot \dom(y))+\dom(x \cdot \dom(z))$ n/a
ISD38 third module axiom $\dom((x \cdot y) \cdot \dom(z)) = \dom(x \cdot \dom(y \cdot \dom(z)))$ n/a
ISD39 fourth module axiom $\dom(1 \cdot \dom(x)) = \dom(x)$ n/a
ISD40 fifth module axiom $\dom(x \cdot \dom(0)) = 0$ n/a
ISD41 antidomain elements are domain elements $(\dom(x)+a(x) = 1 \wedge \dom(x) \cdot a(x) = 0) \Rightarrow \dom(a(x)) = a(x)$ n/a
ISD42 complementation $(\dom(x)+a(x) = 1 \wedge \dom(x) \cdot a(x) = 0) \Rightarrow a(x) \cdot \dom(x)=0$ n/a
ISD43 double negation $(\dom(x)+a(x) = 1 \wedge \dom(x) \cdot a(x) = 0) \Rightarrow a(a(x)) = \dom(x)$ n/a
ISD44 left annihilation $(\dom(x)+a(x) = 1 \wedge \dom(x) \cdot a(x) = 0) \Rightarrow a(x) \cdot x=0$ n/a
ISD45 antidomain locality $(\dom(x)+a(x) = 1 \wedge \dom(x) \dot a(x) = 0) \Rightarrow a(x \cdot y)+a(x \cdot \dom(y)) = a(x \cdot \dom(y))$ n/a
ISD46 left invariant $x = \dom(x) \cdot x$ n/a
ISD47 domain locality $\dom(x \cdot y) = \dom(x \cdot \dom(y))$ n/a
ISD48 subidentity $\dom(x)+1 = 1$ n/a
ISD49 strictness $\dom(0) = 0$ n/a
ISD50 additivity $\dom(x+y) = \dom(x)+\dom(y)$ n/a
ISD51 greatest left annihilation $\dom(y) \cdot x = 0 \Leftrightarrow \dom(y)+a(x)=a(x)$ n/a
ISD52 antitonicity $x+y = y \Rightarrow a(y)+a(x) = a(x)$ n/a
ISD53 codomain closure $\dom(cd(x)) = cd(x)$ n/a
ISD54 coantidomain closure $\dom(ca(x)) = ca(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