(VAR x y z)
(RULES
join(x,meet(x,y)) -> x
meet(x,joint(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].
Remark that a typo has been reported. In rule 2 "joint" should
have been "join". See "108.trs".
)