% These are lattice identities

x v y = y v x.

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

x v (x ^ y) = x.

(((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^
    (w v ((v6 v x) ^ (x v v7))) = x.  % A1

% These are not lattice identities

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

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