Discard Subalgebras with top/bottom elements

[Brandon-Rozek]

When checking pairs of subalgebras, discard the pair if either subalgebra contains either a top or bottom element.

By definition:

• Bottom: Any element x where x && x = x
• Top: Any element x where x || x = x

[Brandon-Rozek]

I'm missing something here since this optimization discards the subalgebras {a3} and {a2} which show VSP for R using Model 5.2.1.1.3

[Brandon-Rozek]

I misinterpreted this. First, I need to figure out what T and F are in this model. This means that for all elements of the carrier set.

Find T such that T || a = T, T && a = a for all a in the carrier set Find F such that F || a = a, F && a = F

Then it becomes a simple check if either T or F are in either subalgebra