4.4.3 Well-Formedness Clauses

Procedure Clauses creates the well-formedness clauses for the pair of variables and , where N1 denotes $\NODE{x}$ , N2 denotes $\NODE{y}$ , and R denotes $R_{xy}$ . Note that we identify $\EQ$ with 1, $\LT$ with 2, $\GT$ with 3, and $\DJ$ with 4.

<Dominance: well-formedness clauses>=: proc {Clauses N1 N2 C} thread or {Equal N1 N2} C=1 [] C\=:1 {NotEqual N1 N2} end end thread or {Above N1 N2} C=2 [] C\=:2 {NotAbove N1 N2} end end thread or {Above N2 N1} C=3 [] C\=:3 {NotAbove N2 N1} end end thread or {Disjoint N1 N2} C=4 [] C\=:4 {NotDisjoint N1 N2} end end end