(VAR x y z) (RULES join(x,meet(x,y)) -> x meet(x,join(y,z)) -> join(meet(x,y),meet(x,z)) meet(x,x) -> x join(x,x) -> x meet(meet(x,y),z) -> meet(x,meet(y,z)) meet(x,y) -> meet(y,x) join(join(x,y),z) -> join(x,join(y,z)) join(x,y) -> join(y,x) ) (COMMENT Theory of Distributive Lattice from [PS81])