Laws for Demonic Refinement 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
DRA1 top element $x\leq 1^\infty$ n/a
DRA2 strong iteration of zero $0^\infty=1$ n/a
DRA3 right unfold $x^\infty = x^\infty\cdot x+1$ n/a
DRA4 isotonicity of strong iteration $x\leq y \Rightarrow x^\infty\leq y^\infty$ n/a
DRA5 top is left annihilator $1^\infty\cdot x = 1^\infty$ n/a
DRA6 infinitity of intfinity is magic $(x^\infty)^\infty = 1^\infty$ n/a
DRA7 strong iteration is idempotent w.r.t. multiplication $x^\infty\cdot x^\infty = x^\infty$ n/a
DRA8 strong iteration over iteration is magic $(x^*)^\infty = 1^\infty$ n/a
DRA9 strong iteration dominates iteration $(x^\infty)^* = x^\infty$ n/a
DRA10 strong iteration is a superidentity $1\leq x^\infty$ n/a
DRA11 an unfold law $x^*\cdot x^\infty = x^\infty$ $x^\infty\cdot x^* = x^\infty$
DRA12 an unfold law $(x^*\cdot y)^\infty = y^*\cdot(x^*\cdot y)^\infty$ n/a
DRA13 simple simulation $x\cdot y =0 \Rightarrow x\cdot y^\infty =x$ n/a
DRA14 the simple inequality of Church Rosser $x^\infty\cdot y^\infty \leq (x+y)^\infty$ n/a
DRA15 special unfold $(x+y)^\infty = y^*\cdot x\cdot (x+y)^\infty + y^\infty$ n/a
DRA16 strong iteration of special elements $(x\cdot 0)^\infty = 1+x\cdot 0$ n/a
DRA17 sliding I $x\cdot (y\cdot x)^\infty \leq (x\cdot y)^\infty\cdot x$ n/a
DRA18 sliding II $(x\cdot y)^\infty\cdot x\leq x\cdot (y\cdot x)^\infty$ n/a
DRA19 denest I $(x+y)^\infty = x^\infty\cdot(y\cdot x^\infty)^\infty$ n/a
DRA20 denest II $(x+y)^\infty\leq (x^*\cdot y)^\infty\cdot x^\infty$ n/a
DRA21 denest IIa $(x^*\cdot y)^\infty\cdot x^\infty\leq (x+y)^\infty$ n/a
DRA22 bubble sort w.r.t. star $y\cdot x\leq x\cdot y \Rightarrow (x+y)^*\leq x^*\cdot y^*$ n/a
DRA23 bubble sort w.r.t. strong iteration $y\cdot x\leq x\cdot y \Rightarrow (x+y)^\infty\leq x^\infty\cdot y^\infty$ n/a
DRA24 simulation w.r.t. strong iteration $z\cdot x\leq y\cdot z \Rightarrow z\cdot x^\infty\leq y^\infty\cdot z$ n/a
DRA25 simulation w.r.t. star I $z\cdot x\leq y\cdot z \Rightarrow z\cdot x^*\leq y^*\cdot z$ n/a
DRA26 simulation w.r.t. star II $x\cdot z\leq z\cdot y \Leftarrow x^*\cdot z\leq z\cdot y^*$ n/a
DRA27 a classical refinement law $s'\leq s\cdot z,\; z\cdot e'\leq e,\; z\cdot a'\leq a\cdot z,\; z\cdot b\leq b,\; b^\infty=b^*$
$\Rightarrow s'\cdot(a'+b)^\infty\cdot e'\leq s\cdot a^\infty\cdot e$
DRA28 towards Back's Atomicity Refinement Theory (step I) $s=sq,\; a=qa,\; qb = 0$
$\Rightarrow s(a+b)^\infty q\leq s(a\cdot b^\infty q)^\infty$
DRA29 towards Back's Atomicity Refinement Theory (step II) $s=sq,\; a=qa,\; qb = 0,\; (a+b)l\leq l(a+b),\; ql\leq lq,\; q\leq 1$
$\Rightarrow s(a+b+l)^\infty q\leq s(ab^\inftyq+l)^\infty$
DRA30 Back's Atomicity Refinement Theory (part I) $s\leq sq,\; a\leq qa,\; qb=0,\; (a+b+r)l\leq l(a+b+r),\; ql\leq lq,\; rb\leq br,\; rq\leq qr,\; r^\infty=r^*$
$\Rightarrow s(a+b+r+l)^\infty q\leq sl^\infty qr^\infty q(ab^\infty qr^\infty)^\infty$
DRA31 Back's Atomicity Refinement Theory (part II) $s\leq sq,\; a\leq qa,\; qb=0,\; (a+b+r)l\leq l(a+b+r),\; ql\leq lq,\; rb\leq br,\; rq\leq qr,\; r^\infty=r^*,\; q\leq 1$
$\Rightarrow sl^\infty qr^\infty q(ab^\infty qr^\infty)^\infty \leq s(ab^\infty q+r+l)^\infty$
DRA32 a refinement law $y\cdot x \leq x\cdot (x+y)^\infty \Rightarrow (x+y)^\infty= x^\infty\cdot y^\infty$ n/a
DRA33 TBD $ (x+y)^\infty\cdot 0 =0 \Rightarrow x^\infty\cdot 0+y^\infty\cdot 0=0$ n/a
DRA34 TBD $ y\cdot x \leq x\cdot (x+y)^\infty \Rightarrow ((x+y)^\infty\cdot 0 =0 \Leftarrow x^\infty\cdot 0+y^\infty\cdot 0=0)$ n/a
DRA35 star sliding $(x \cdot y)^* \cdot x = x \cdot (y \cdot x)^*$ n/a
DRA36 decomposition $(x+y)^* = x^* \cdot (y \cdot x^*)^*$ n/a
DRA37 TBD $(x+y)^\omega = (x^* \cdot y)^\omega \cdot x^\omega$ n/a
DRA38 special decomposition $(x+y)^* = y^* \cdot (x \cdot (x+y)^*)+y^*$ n/a
DRA39 a simultion theorem $x \cdot y \leq y \cdot x \Rightarrow x^* \cdot y^* \leq y^* \cdot x^*$ n/a
DRA40 a simulation theorem $x \cdot y \leq y \cdot x \Rightarrow x^\omega \cdot y^\omega \leq y^\omega \cdot x^\omega$ n/a
DRA41 simple simulation law w.r.t. star $x \cdot y = 0 \Rightarrow x \cdot y^* = x$ n/a
DRA42 simple simulation law $x \cdot y = 0 \Rightarrow x \cdot y^\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