%
% 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(restrict_denials).

%
% Input formulas
%

formulas(assumptions).

%
% 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]").

all x all y (((x = 1) & (x => y = 1)) -> (y = 1))      #label("(3)").
all x all y (((x = 1) & (y = 1)) -> (x ^ y = 1))       #label("(4)").
all x all y (((x => y = 1) & (y => x = 1)) -> (x = y)) #label("(5)").

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

% Definition of * (monoid operation) in Alg Mod* F**-algebras
x * y = ~(x => ~y)                                     #label("(* def)").

% Definition of 0 in Alg Mod* F**-algebras
0 = ~(x => x)                                          #label("(0 def)").

% Definition of 1 in Alg Mod* F**-algebras
1 = x => x                                             #label("(1 def)").

end_of_list.

formulas(goals).

%
% Identities axiomatising Nelson FL_ew-algebras. Prove all these.
%

% 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

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

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

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

end_of_list.
