Laws for Relation Algebra

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
RA1 isotonicity wrt converse $x\leq y \Leftrightarrow x\conv \leq y\conv$ n/a
RA2 simple properties of converse $0\conv = 0$
$(\overline{x})\conv = \overline{(x\conv)}$
$(x\meet y)\conv = x\conv\meet y\conv$
RA3 TBD $x\conv\meet y=0 \Leftrightarrow x\meet y\conv =0$ n/a
RA4 converse of 1 $1\conv = 1$ n/a
RA5 distributivity of composition over addition $x;(y\join z) = x;y \join x;z$ $(x\join y);z = x;z \join y;z$
RA6 isotonicity wrt. composition $x\leq y \Rightarrow (x;z\leq y;z\; \wedge\; z;x\leq z;y)$ n/a
RA7 Schroeder I $x;y\meet z=0 \Rightarrow y\meet(x\conv;z)=0$ n/a
RA8 Schroeder II $x;y\meet z=0 \Leftarrow y\meet(x\conv;z)=0$ n/a
RA9 TBD $\overline{y;x};x\conv \leq \overline{y}$ n/a
RA10 annihilation $x;0=0$
RA11 properties of identity $x;1=x \;\wedge\;1;x=x$ n/a
RA12 properties for top $x\leq x;\top$
$x\leq \top;x$
RA13 TBD $x;y\meet\overline{x;z} = x;(y\meet\overline{z})\meet \overline{x;z}$ n/a
RA14 TBD $\overline{x;y} \join x;z = \overline{x;(y\meet \overline{z})}+x;z$ n/a
RA15 TBD $x;\top=x \Rightarrow \overline{x};\top=\overline{x}$ n/a
RA16 TBD $x;\top=x\,\wedge\, y;\top=y \Rightarrow (x\meet y);\top=x\meet y$ n/a
RA17 TBD $x;\top=x \Rightarrow (x\meet 1);y = x\meet y$ n/a
RA18 TBD $x;\top=x \Rightarrow (y\meet x\conv);(x\meet z) \leq y;(x\meet z)\,\wedge\, (y\meet x\conv);(x\meet z) \leq (y\meet x\conv);z$ n/a
RA19 TBD $x\leq 1 \Rightarrow x\conv = x$ n/a
RA20 TBD $x\leq 1 \Rightarrow (x;\top)\meet y=x;y$ n/a
RA21 TBD $x\leq 1 \Rightarrow \overline{x;\top}\meet 1 = \overline{x}\meet 1$ n/a
RA22 TBD $x\leq 1\,\wedge\, y\leq1 \Rightarrow x;y=x\meet y$ n/a
RA23 distributivity $x \leq 1\,\wedge\, y \leq 1 \Rightarrow (x;z\meet y;z) = (x\meet y);z$ n/a
RA24 TBD $x\leq 1 \Rightarrow (x;y)\meet\overline{z} = (x;y)\meet\overline{x;z}$ n/a
RA25 functions are preserved under composition $x\conv;x\leq 1\,\wedge\, y\conv;y\leq 1\Rightarrow (x;y)\conv;(x;y)\leq 1$ n/a
RA26 subdistributivity $x;(y\meet z) + (x;y\meet x;z)=(x;y\meet x;z)$ n/a
RA27 TBD $ x;\top=x \Rightarrow (x\meet y);z = x\meet (y;z)$ n/a
RA28 TBD $x;\top=x \Rightarrow (y\meet x\conv);(x\meet z) = y;(x\meet z)$
$x;\top=x \Rightarrow (y\meet x\conv);(x\meet z)=(y\meet x\conv);z$
RA29 modular laws $z;x\meet y \leq z;(x\meet z\conv;y)\meet y$ $x;z\meet y \leq (x\meet y;z\conv);z\meet y$
RA30 Dedekind $z;x\meet y \leq (z\meet y;x\conv);(x\meet z\conv ;y)$ n/a
RA31 distributivity $x\conv ;x\leq 1 \Rightarrow x;(y\meet z) = x;y\meet x;z$ n/a
RA32 TBD $\forall x.\, (\forall y.\, x;y\meet x;\overline{y}=0 \Leftarrow x\conv;x\leq 1)$ n/a
RA33 TBD $\forall x (\forall y x;y\meet x;\overline{y}=0 \Rightarrow x\conv;x\leq 1)$ n/a
RA34 equivalence I of x,y forms rectangle inside z $x;y\conv\leq z \Leftrightarrow \overline{z};y\leq x\conv$ n/a
RA35 equivalence II of x,y forms rectangle inside z $x;y\conv\leq z \Leftrightarrow \overline{z}\conv;x \leq\overline{y}$ n/a
RA36 fringe property I $\mbox{fringe}(x\conv) = \mbox{fringe}(x)\conv$ n/a
RA37 fringe property II If $E$ is an order, then $\mbox{fringe}(E)=1$ n/a
RA38 Exercise 9.1.1 of [Schmidt07] $(x;\top);x =x \Leftrightarrow (x;\overline{x}\conv);x=0$ n/a
RA39 Proposition 9.4.2 of [Schmidt07] $\mbox{fringe}(x) = \mbox{syq}(\overline{(\overline{x};x\conv)},x)$ n/a
RA40 properties of symmetric quotient (Prop. 7.6.1 of [Schmidt07]) $\mbox{syq}(\overline{x},\overline{y}) = \mbox{syq}(x,y)$
$\mbox{syq}(x,y)\conv = \mbox{syq}(y,x)$
RA41 properties of symmetric quotient (Prop. 7.6.2 of [Schmidt07]) $x;\mbox{syq}(x,x)\leq x$ n/a
RA42 $(\overline{x;\overline{x}\conv;x})\conv$ is the greatest subinverse of $x$ (Lemma 9.5.4 of [Schmidt07]) $x;y;x\leq x \Leftrightarrow y\leq\overline{(x;\overline{x}\conv;x)}\conv$ n/a
RA43 Moore-Penrose inverses are uniquely determined provided they exist. (Lemma 9.5.8 of [Schmidt07]) $(x;y;x=x \wedge y;x;y=y \wedge (x;y)\conv =x;y \wedge (y;x)\conv=y;x \wedge x;z;x=x \wedge z;x;z=z \wedge (x;z)\conv=x;z \wedge (z;x)\conv=z;x) \Rightarrow y=z$ n/a
RA44 Properties of Ferrers $\mbox{ferrers}(x) \Rightarrow \mbox{ferrers}(x\conv) \wedge \mbox{ferrers}(\overline{x}) \wedge \mbox{ferrers}(\overline{x}\conv;x)$ n/a
RA45 Properties of Ferrers $\mbox{ferrers}(x) \Rightarrow \mbox{ferrers}(\overline{x};x\conv)$ n/a
RA46 Properties of Ferrers $\mbox{ferrers}(x) \Rightarrow \mbox{ferrers}(x;\overline{x}\conv ;x)$ n/a
RA47 TBD $x;(y \meet z) = x;y \meet x;z \Rightarrow x\conv ;x \leq 1$ n/a
RA48 symmetric quotient is reflexive $1 \leq \mbox{syq}(x,x)$ n/a
RA49 isotonicity of symmentric quotient $\mbox{syq}(x,y) \leq \mbox{syq}(z;x,z;y)$ n/a
RA50 an unfold law $x \leq (x;x\conv);x$ n/a
RA51 an important property for subidentities $x \leq 1 \Rightarrow \overline{x;\top} = (1 \meet \overline{x});\top$ n/a
RA52 a prop of symmentric quotient $x\conv ;x \leq 1 \wedge 1 \leq x;x\conv \Rightarrow x;\mbox{syq}(y,z) = \mbox{syq}(y;x\conv,z)$ n/a
RA53 TBD $x;\overline{\overline{y};z} \leq \overline{\overline{x;y};z}$ n/a
RA54 some strictness property $x \neq 0 \Leftrightarrow x\conv ;x \neq 0$ n/a
RA55 complement of xT is left ideal $\overline{x;\top} = \overline{x;\top};\top$ n/a
RA56 associativity of demonic composition $\demonic(x,\demonic(y,z)) = \demonic(\demonic(x,y),z)$ n/a
RA57 consequense of the Tarski rule $(x;\top);x = x \Rightarrow (x;\overline{x}\conv);x = 0$ n/a
RA58 meet splitting $x \leq y \meet z \Leftrightarrow x \leq y \wedge x \leq z$ n/a
RA59 join splitting $x + y \leq z \Leftrightarrow x \leq z \wedge y \leq z$ n/a
RA60 relational unfold with subidentity and converse $x = (1 \meet x;x^\omega);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