% This is a problem, from Norm Megill, on weak orthomodular lattices.

assign(increment, 2).

formulas(assumptions).

% Lattice Axioms

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

% Idempotence (follows from the lattice axioms)

x ^ x = x.
x v x = x.

% The following gives us ortholattices.

c(x) ^ x = 0.
c(x) v x = 1.
c(c(x)) = x.
x ^ y = c(c(x) v c(y)).

% Ortholattice lemmas.

1 v x = 1.
1 ^ x = x.

0 ^ x = 0.
0 v x = x.

% Weak orthomodular law (*1 of mail 68).

(c(x) ^ (x v y)) v (c(y) v (x ^ y)) = 1.

% Denial of equation in question (*3 of mail 68).

A ^ (B v (A ^ (c(A) v (A ^ B)))) != A ^ (c(A) v (A ^ B)).

end_of_list.
