4.4.3 Well-Formedness Clauses

Procedure Clauses creates the well-formedness clauses for the pair of variables x and y, 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


Denys Duchier
Version 1.3.99 (20050412)