A 3-basis for orthomodular lattices in terms of the Sheffer stroke.

f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). % A_SS f(f(x,x),f(x,y)) = x. % B_SS f(x,f(x,f(x,y))) = f(x,y). % OM_SSThese two Otter jobs show that this basis is definitionally equivalent to the (join/meet/complement) OML basis

otter < OML-SS.in > OML-SS.out otter < OML-SS-2.in > OML-SS-2.outThese three Mace2 jobs show that

mace2 -N6 -p < OML-SS-a.in > OML-SS-a.out mace2 -N6 -p < OML-SS-b.in > OML-SS-b.out mace2 -N6 -p < OML-SS-c.in > OML-SS-c.out