include("ortholattice-header").

% LT basis: { AJ, AM, B1, B2 }

list(usable).

  x v (y v z) = y v (x v z).    % AJ
  x ^ (y ^ z) = y ^ (x ^ z).    % AM
% x v (x ^ y) = x.              % B1
  x ^ (x v y) = x.              % B2

% A v (B v C) != B v (A v C).   % denial of AJ
% A ^ (B ^ C) != B ^ (A ^ C).   % denial of AM
  A v (A ^ B) != A.             % denial of B1
% A ^ (A v B) != A.             % denial of B2

end_of_list.

