op(400, xfx, [*,+,^,v,/,\,#]).  % infix operators
op(300,yf,@).                   % postfix operator

list(usable).

% (v,^) is a transitive near lattice.

x ^ x = x.
x ^ y = y ^ x.
x ^ (x v y) = x.
x ^ (y v (x v z)) = x.

x v x = x.
x v y = y v x.
x v (x ^ y) = x.
x v (y ^ (x ^ z)) = x.

% (v,*) is a transitive near lattice.

x * x = x.
x * y = y * x.
x * (x v y) = x.
x * (y v (x v z)) = x.

x v x = x.
x v y = y v x.
x v (x * y) = x.
x v (y * (x * z)) = x.

0 ^ 1 != 0 * 1.

end_of_list.

