%
% 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**.
%
x => ((x => y) => y) = 1                               #label("(A1)[= 1]").
(x => y) => ((y => z) => (x => z)) = 1                 #label("(A2)[= 1]").
(x ^ y) => x = 1                                       #label("(A3)[= 1]").
(x ^ y) => y = 1                                       #label("(A4)[= 1]").
((x => y) ^ (x => z)) => (x => (y ^ z)) = 1            #label("(A5)[= 1]").
x => (x v y) = 1                                       #label("(A6)[= 1]").
y => (x v y) = 1                                       #label("(A7)[= 1]").
((x => z) ^ (y => z)) => ((x v y) => z) = 1            #label("(A8)[= 1]").
(x ^ (y v z)) => ((x ^ y) v z) = 1                     #label("(A9)[= 1]").
~~x => x = 1                                           #label("(A10)[= 1]").
(x => ~y) => (y => ~x) = 1                             #label("(A11)[= 1]").
x => (y => x) = 1                                      #label("(A12)[= 1]").
((x => (x => y)) ^ (~y => (x => y))) => (x => y) = 1   #label("(A13)[= 1]").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

x => ((x => y) => y) = 1.
(x => y) => ((y => z) => (x => z)) = 1.
(x ^ y) => x = 1.
(x ^ y) => y = 1.
((x => y) ^ (x => z)) => (x => (y ^ z)) = 1.
x => (x v y) = 1.
y => (x v y) = 1.
((x => z) ^ (y => z)) => ((x v y) => z) = 1.
(x ^ (y v z)) => ((x ^ y) v z) = 1.
~~x => x = 1.
(x => ~y) => (y => ~x) = 1.
x => (y => x) = 1.
((x => (x => y)) ^ (~y => (x => y))) => (x => y) = 1.

x ^ 1 = x.
x * 1 = x.
x => (y ^ z) = (x => y) ^ (x => z).
(x => y) ^ (x => z) = x => (y ^ z).
(x => (x * y)) ^ y = y.
1 = x => (x * 1).
x => (x * 1) = 1.
x => x = 1.
~ ~ x = x.
x ^ y = y ^ x.
(x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y.
(x => (x => ~ y)) ^ (y => (~ ~ y => ~ x)) = x => ~ y.
(x => (x => ~ y)) ^ (y => (y => ~ x)) = x => ~ y.
x => ~ y = (y => (y => ~ x)) ^ (x => (x => ~ y)).
(x => (x => ~ y)) ^ (y => (y => ~ x)) = y => ~ x.
x => ~ y = y => ~ x.
x => y = ~ y => ~ x.
~ x => ~ y = y => x.
(x => (x => y)) ^ (~ y => (x => y)) = x => y.
x ^ (x v y) = x.
x = 1 ^ x.
1 ^ x = x.
x => (x ^ (x v y)) = 1.
1 ^ (x => y) = x => (x ^ y).
x => (x ^ y) = 1 ^ (x => y).
x => (x ^ y) = x => y.
x v y = y v x.
x v (x ^ y) = x.
x v (y ^ x) = x.
x = (y ^ x) v x.
(x ^ y) v y = y.
x = (x ^ y) v x.
(x ^ y) v x = x.
(x v y) ^ (x v z) = x v (y ^ z).
(x ^ y) v (x ^ z) = x ^ (y v z).
(x v (y ^ z)) => (x v z) = 1.
x ^ 0 = 0.
x * y = y * x.
x * (y v z) = (x * y) v (x * z).
(x * y) v (x * z) = x * (y v z).
(x * (x => y)) v y = y.
~ x = x => 0.
x => 0 = ~ x.
x ^ (y v x) = x.
x v 0 = x.
1 * x = x.
x = x v (y * (y => x)).
x v (y * (y => x)) = x.
x = x ^ (y => (y * x)).
x ^ (y => (y * x)) = x.
(x => (y * x)) ^ y = y.
~ x => 0 = x.
x * (x => 0) = 0.
x = (y v x) ^ x.
(x v y) ^ y = y.
x * ~ x = 0.
0 = ~ x * x.
~ x * x = 0.
x v (y * ~ y) = x.
0 = ~ 1.
~ 1 = 0.
x * y = x * (y v ~ x).
x * (y v ~ x) = x * y.
x * (y v ~ x) = y * x.
~ x * (y v x) = y * ~ x.
~ x * (x v y) = y * ~ x.
~ x * x = (x ^ y) * ~ x.
(x ^ y) * ~ x = ~ x * x.
(x ^ y) * ~ x = 0.
~ x ^ ((x ^ y) => 0) = ~ x.
~ x ^ ~ (x ^ y) = ~ x.
~ (x v y) ^ ~ y = ~ (x v y).
~ x => y = ~ y => x.
~ 0 = 1.
x = ~ 0 => x.
~ 0 => x = x.
1 => x = x.
(x => (y ^ z)) => (x => z) = 1.
(x => y) => (x => (y v z)) = 1.
(x => ~ (y v z)) => (x => ~ z) = 1.
((x v y) => z) => (~ z => ~ y) = 1.
((x v y) => z) => (y => z) = 1.
(x => y) => ((x ^ z) => y) = 1.
((x => (y * x)) => z) => (y => z) = 1.
1 => (x => (y => ((x * y) v z))) = 1.
1 => (x => (y => (z v (x * y)))) = 1.
1 = x => (y => (z v (x * y))).
x => (y => (z v (x * y))) = 1.
x v (x * y) = x * (1 v y).
1 v x = 1.
x v (x * y) = x * 1.
x v (x * y) = x.
(x * y) * z = x * (y * z).
x = (x v y) ^ x.
(x v y) ^ x = x.
x * (y * z) = z * (x * y).
x ^ (y => (x * y)) = x.
x * (y * z) = y * (x * z).
0 = ~ x * (x ^ y).
~ x * (x ^ y) = 0.
x * ~ (x v y) = 0.
~ (x v y) * y = 0.
(x * (x => y)) * ~ y = 0.
~ x * (y * (y => x)) = 0.
0 = x * ((x => y) * ~ y).
x * ((x => y) * ~ y) = 0.
x * (y * (y => ~ x)) = 0.
0 = x * (y * (x => ~ y)).
x * (y * (x => ~ y)) = 0.
(x * y) * (x => ~ y) = 0.
x v (~ y * (~ x => y)) = x.
x => (y => (x * y)) = 1.
(x * y) => ((x => ~ y) => 0) = 1.
(x * y) => ~ (x => ~ y) = 1.
(x * ~ y) => ~ (x => y) = 1.
1 = (x => y) => ~ (x * ~ y).
(x => y) => ~ (x * ~ y) = 1.
1 => (x => ~ (y * ~ (x * y))) = 1.
1 = x => ~ (y * ~ (x * y)).
x => ~ (y * ~ (x * y)) = 1.
x v (~ ~ (y * ~ (~ x * y)) * 1) = x.
x * (1 * ~ ((x => y) => y)) = 0.
x * ~ ((x => y) => y) = 0.
x ^ (~ ((x => y) => y) => 0) = x.
x ^ ((x => y) => y) = x.
(x => y) => (x => ((y => z) => z)) = 1.
(x => y) ^ (1 => ~ (x * ~ y)) = x => y.
x ^ (1 => (y => (z v (x * y)))) = x.
x ^ (y => (z v (x * y))) = x.
x = (y => (z v (x * y))) ^ x.
(x => (y v (z * x))) ^ z = z.
(x => (y v (x * z))) ^ z = z.
x v (~ ~ (y * ~ (y * ~ x)) * 1) = x.
(x => y) ^ ~ (x * ~ y) = x => y.
x v ((y * ~ (y * ~ x)) * 1) = x.
x v (y * ~ (y * ~ x)) = x.
(x => y) ^ ~ (x * ~ y) = ~ (x * ~ y).
~ (x * ~ y) = x => y.
~ (x * y) = x => ~ y.
~ (x * (y * z)) = (x * y) => ~ z.
~ (x * (y * z)) = z => ~ (x * y).
x => ~ (y * z) = y => ~ (z * x).
x => ~ (y * z) = z => ~ (x * y).
x => (y => ~ z) = z => ~ (x * y).
x => ~ (y * z) = y => (z => ~ x).
x => (y => z) = y => (~ z => ~ x).
x => (~ y => ~ z) = z => (x => y).
x => (y => z) = y => (x => z).
(x v y) v z = x v (y v z).
x v (y v z) = y v (z v x).
x v (y v z) = z v (x v y).
x v ((x ^ y) v z) = z v x.
x v (y v (x ^ z)) = y v x.
x v (y v (x ^ z)) = x v y.
x => (y => (y * x)) = 1.
(x v y) => (~ y => (x * ~ y)) = 1.
((x v y) => z) => (x => z) = 1.
(x => y) v (((x v z) => y) * 1) = x => y.
((x => y) => y) v x = (x => y) => y.
(((x => y) => y) => z) => (x => z) = 1.
1 => (x => (((x => y) ^ z) => y)) = 1.
1 = x => (((x => y) ^ z) => y).
x => (((x => y) ^ z) => y) = 1.
x => ((y ^ (x => z)) => z) = 1.
x ^ (1 => ((y ^ (x => z)) => z)) = x.
x ^ ((y ^ (x => z)) => z) = x.
(x => y) v ((x v z) => y) = x => y.
(x => y) => z = ~ z => (x * ~ y).
~ x => (y * ~ z) = (y => z) => x.
(x v y) => ((x => y) => y) = 1.
(x => y) => ((x v y) => y) = 1.
((x v y) => y) v ((x => y) * 1) = (x v y) => y.
((x v y) => y) v (x => y) = (x v y) => y.
(x v y) => y = (x => y) v ((x v y) => y).
(x => y) v ((x v y) => y) = (x v y) => y.
(x v y) => y = x => y.
(x v y) => x = y => x.
(x v y) => x = (y v (x ^ z)) => x.
(x v (y ^ z)) => y = (y v x) => y.
(x v (y ^ z)) => y = x => y.
(x v (y ^ z)) => z = x => z.
(x v y) => ((z ^ (y => u)) => u) = x => ((z ^ (y => u)) => u).
(x v y) => (((x => z) ^ (y => z)) => z) = 1.
1 = ((x => y) ^ (z => y)) => ((x v z) => y).

end_of_list.
