%
% Prover9 commands
%
op(400, infix, [^,v,"=>",*]).
op(200, prefix, ~).

lex([0, 1, *, ^, =>, v, ~]).

assign(order,kbo).
set(lex_order_vars).

set(para_units_only).

clear(back_demod).
set(para_from_small).
set(para_into_vars).
set(restrict_denials).

%
% Input formulas
%

formulas(assumptions).

%
% Identities axiomatising Nelson FL_ew-algebras.
%

% Bounded lattice part
(x v y) v z = x v (y v z)                     #label("(D1)").
(x ^ y) ^ z = x ^ (y ^ z)                     #label("(D2)").

x ^ x = x                                     #label("(D3)").
x v x = x                                     #label("(D4)").

x v y = y v x                                 #label("(D5)").
x ^ y = y ^ x                                 #label("(D6)").

x v (x ^ y) = x                               #label("(D7)").
x ^ (x v y) = x                               #label("(D8)").

x ^ 0 = 0                                     #label("(D9)").
x ^ 1 = x                                     #label("(D10)").

% Monoid part
x * 1 = x                                     #label("(M1)").
x * y = y * x                                 #label("(M2)").
(x * y) * z = x * (y * z)                     #label("(M3)").

% Residuation part
x * (y v z) = (x * y) v (x * z)               #label("(R1)").
x => (y ^ z) = (x => y) ^ (x => z)            #label("(R2)").
(x * (x => y)) v y = y                        #label("(R3)").
(x => (x * y)) ^ y = y                        #label("(R4)").

% Nelson part 
x => (x => (x => y)) = x => (x => y)          #label("(E_2)"). % 3-potency

(x v y) ^ (x v z) = x v (y ^ z)               #label("(D11)"). % Distributivity
(x ^ y) v (x ^ z) = x ^ (y v z)               #label("(D12)").

~(~x) = x                                     #label("(I)").   % Involution

(x => (x => y)) ^ (~y => (~y => ~x)) = x => y #label("(N)").   % Nelson identity

%
% Definitions mapping Nelson FL_ew-algebras to Alg Mod* F**-algebras 
%

% Definition of ~ (negation operation) in Nelson FL_ew-algebras
~x = x => 0                                   #label("(~ def)").

end_of_list.

formulas(goals).

%
% Identities and quasi-identities axiomatising Alg Mod* F**.
%
all x all y (((x => y = 1) & (y => x = 1)) -> (x = y)) #label("(5)").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

x * (c1 => c2) = x.
x * (c2 => c1) = x.
c1 v c2 = c2.
c2 = c2 v c1.
c2 v c1 = c2.
c2 v c1 = c1.
c1 = c2.
c2 = c1.

end_of_list.
