imply

Returns the relative pseudocomplement of this relative to that. the relative pseudocomplement is greatest x s.t. this & x <= that.

How does this work? we are dealing with constraints of the form (A1 | ... | Am) & x <= B1 | ... | Bn

which can be rewritten as (A1&x) | ... | (Am&x) <= B1 | ... | Bn

This inequality only holds true if every meet on the left can be "covered" on the right s.t. a meet on the right side is a subset of the meet on the left side. For every meet on the left Ai, we complement it with every meet on the right Bj. because we want the greatest solution, we join these complements together, arriving at an upper bound for x: x <= Ci1 | ... | Cin

where Cij = Bj \ Ai.

But we have to do the same process for all meets on the left, so we get m upper bounds. these have to be all simultaneously satisfied, so we take the meet of the upper bounds: x = (C11 | ... | C1n) & ... & (Cm1 | ... | Cmn)

The algorithm below computes exactly this solution.