include("ortholattice-header").

% BA basis:    { AJ, DM, ONE, CUT }
% BA_SS basis: { A_SS, CUT_SS }

list(sos).

x v (y v z) = y v (x v z).      % AJ
x ^ y = c(c(x) v c(y)).         % DM
x v c(x) = y v c(y).            % ONE
(x v c(y)) ^ (x v y) = x.       % CUT

f(x,y) = c(x) v c(y).      % DEF_SS

% Lemmas already proved.

x v (x ^ y) = x.                        % B1
c(c(x)) = x.                            % CC

end_of_list.

% The following command orders the relevant operations as f < v < c < ^
% so that everything is rewritten in terms of f whenever possible.

lex([D, C, B, A, 0, 1, f(x,x), x v x, c(x), x ^ x]).

assign(max_proofs, 5).

list(passive).

f(A,f(f(B,C),f(B,C))) != f(B,f(f(A,C),f(A,C)))  | $Ans(A_SS).
f(f(A,f(B,B)),f(A,B)) != A                      | $Ans(CUT_SS).

A v B != f(f(A,A),f(B,B))  | $Ans(DEF_J).
A ^ B != f(f(A,B),f(A,B))  | $Ans(DEF_M).
c(A) != f(A,A)             | $Ans(DEF_C).

end_of_list.