Relation Division

Comparing left and right divisions

Under versus Over

$X \backslash Y = (Y^\circ / X^\circ)^\circ$

---

sig A { X: set B }

sig B {}

sig C { Y: set B }

check {
  Under[A,B,C,X,Y] = ~(Over[A,B,C,~Y,~X])
} for 10

Composition versus Under

$X \circ Z \subseteq Y \equiv Z \subseteq X \backslash Y$

---

sig A { X: set B }

sig B {}

sig C { Y: set B, Z: set A}

check {
  Z.X in Y iff Z in Under[A,B,C,X,Y]
} for 10

Composition versus Over

$Z \circ X \subseteq Y \equiv Z \subseteq Y / X$

---

sig A { Z: set C}

sig B { X: set A, Y: set C}

sig C {}

check {
  X.Z in Y iff Z in Over[A,B,C,Y,X]
} for 10