A 5-basis for ortholattices (OL) in terms of join (v), meet (^), and complement (c).
x v (y v z) = y v (x v z). % AJ
x v (x ^ y) = x. % B1
x ^ y = c(c(x) v c(y)). % DM
c(c(x)) = x. % CC
x v c(x) = y v c(y). % ONE
If we start with the lattice theory 4-basis { AJ, AM, B1, B2 } and
restrict that to the ortholattices by adding { DM, CC, ONE }, then AM and B2 become dependent.
Here are Otter proofs.
otter < OL1.in > OL1.out
otter < OL2.in > OL2.out
Here are Mace2 jobs showing that the OL 5-basis given above is independent.
mace2 -N6 -p < OLa.in > OLa.out
mace2 -N6 -p < OLb.in > OLb.out
mace2 -N6 -p < OLc.in > OLc.out
mace2 -N6 -p < OLd.in > OLd.out
mace2 -N6 -p < OLe.in > OLe.out