Boolean version of well-formed invariant.

Had to add finiteness of lattice as an axiom.