Lattice TOP ⊤ INT_TOP ⊤ :int TOP->INT_TOP BOT ⊥ INT_HI max < min INT_TOP->INT_HI INT_BOT ⊥ :int INT_BOT->BOT INT_XBOOL 1...0 INT_HI->INT_XBOOL INT_CON constants... INT_HI->INT_CON INT_CON0 0 INT_XBOOL->INT_CON0 INT_CON1 1 INT_XBOOL->INT_CON1 INT_LO max > min INT_CON->INT_LO INT_BOOL 0...1 INT_CON0->INT_BOOL INT_CON1->INT_BOOL INT_BOOL->INT_LO INT_LO->INT_BOT