Modular Ortholattices in Terms of the Sheffer Stroke

Back to the Main Page

A 4-basis for modular ortholattices 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,x)) = f(y,f(y,y)).                      % ONE_SS
    f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))).  % MOD_SS
These two Otter jobs show that this basis is definitionally equivalent to the (join/meet/complement) MOL basis { AJ, B1, DM, CC, ONE, MOD }. 
    otter < MOL-SS.in > MOL-SS.out
    otter < MOL-SS-2.in > MOL-SS-2.out
These four Mace2 jobs show that { A_SS, B_SS, ONE_SS, MOD_SS } is independent. 
    mace2 -N6 -p < MOL-SS-a.in > MOL-SS-a.out
    mace2 -N6 -p < MOL-SS-b.in > MOL-SS-b.out
    mace2 -N6 -p < MOL-SS-c.in > MOL-SS-c.out
    mace2 -N6 -p < MOL-SS-d.in > MOL-SS-d.out