assign(new_constants, 1).

assign(eq_defs, fold).

formulas(sos).

% Veroff's 2-basis for BA in terms of the Sheffer stroke.

f(x,y) = f(y,x).
f(f(x,y),f(x,f(y,z))) = x.

% f(f(x, f(f(y, x), x)), f(y, f(z, x))) = y.  % Sh_1

% Denial of the Sheffer basis.

f(f(a, a), f(a, a)) != a
	| f(a, f(b, f(b, b))) != f(a, a)
	| f(f(f(b, b), a), f(f(c, c), a)) != f(f(a, f(b, c)), f(a, f(b, c)))
	# answer("Sheffer").

% Define a new operation (which turns out to be complement).
% The "assign(eq_defs, fold)" above causes this definition to be
% oriented as a rewrite rule so that the operation is introduced
% whenever possible.

x' = f(x,x).

end_of_list.