The type property must form a partial order, and must be equipped with a least element bottom and with an equality test equal. The partial order must satisfy the ascending chain condition: every monotone sequence must eventually stabilize.
We do not require an ordering test leq or a join operation join.
equal p q determines whether the properties p and q are equal. In the implementation of this test, it is permitted to assume that p <= q holds.
val is_maximal : property -> boolis_maximal p determines whether the property p is maximal with respect to the partial order. A conservative check suffices: it is always permitted for is_maximal p to be false. If is_maximal p is true, then p must have no strict upper bound. In particular, if properties form a lattice, then is_maximal p = true implies that p is the top element of the lattice.