Below

One point

---

$\textbf{Below} \; A \; R \; \{ x \}\; y \equiv R.y.x$

---

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all x,y: A {
      Below[A,R,x,y]
      iff
      y->x in R
    }
  }
} for 10 expect 0

Range Disjunction

---

$\textbf{Below} \; A \; R \; (S \cup T) \; y \equiv \textbf{Below} \; A \; R \; S \; y \wedge \textbf{Below} \; A \; R \; T \; y$

---

sig A { R: set A }

sig S,T in A {}

check {
  { Preorder[A,R]
  } implies {
    all y: A {
      Below[A,R,S+T,y]
      iff
      Below[A,R,S,y] and Below[A,R,T,y]
    }
  }
} for 10 expect 0

Empty Range

---

$\textbf{Below} \; A \; R \; \empty \; y \equiv \textbf{true}$

---

sig A { R: set A }

check {
  { Preorder[A,R]
  } implies {
    all y: A {
      Below[A,R,none,y]
    }
  }
} for 10 expect 0