%
% Prover9 commands
%

clear(auto).

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

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

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

set(paramodulation).
set(para_units_only).
clear(back_demod).
set(hyper_resolution).

set(auto_denials).
set(restrict_denials).

% **************************************************************************
% Clauses for Section 4
% **************************************************************************

formulas(assumptions).

%
% Identities axiomatising lattices
%

(x v y) v z = x v (y v z)                 # label("(D1)").
(x ^ y) ^ z = x ^ (y ^ z)                 # label("(D2)").

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

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

%
% Identities and quasi-identities axiomatising BCK-algebras
%

(x => y) => ((y => z) => (x => z)) = 1    # label("(BCK1)").
1 => x = x                                # label("(BCK2)").
x => 1 = 1                                # label("(BCK3)").
x => y != 1 | y => x != 1 | x = y         # label("(BCK4)").

%
% Identities axiomatising partially ordered, commutative integral 
% residuated monoids (pocrims)
%
%    Note: These identities axiomatise pocrims when taken in
%    conjunction with the identities and quasi-identities axiomatising  
%    BCK-algebras given above.
%
x * 1 = x                                 # label("(M1)").
x * y = y * x                             # label("(M2)").
(x * y) * z = x * (y * z)                 # label("(M3)").
(x * y) => z = x => (y => z)              # label("(P)").

%
% Identities axiomatising commutative, integral residuated lattices
%
%    Note: These identities axiomatise commutative, integral residuated
%    lattices when taken in conjunction with the identities and 
%    quasi-identities axiomatising pocrims given above.
%
%    Note: This quasi-equational basis for commutative, integral 
%    residuated lattices axiomatises them as structures
%    <A; ^, v, *, =>, 1> with a lattice reduct <A; ^, v>,
%    a pocrim reduct <A; *, =>, 1>, such that (i) 1 is the greatest 
%    element with respect to the lattice partial ordering; and 
%    (ii) the lattice partial order and BCK-algebra partial orders 
%    coincide.
%

x ^ 1 = x                                 # label("(D10)").
x ^ ((x => y) => y) = x                   # label("(3.7)").
(x ^ y) => y = 1                          # label("(3.11)").

%
% Identities axiomatising FL_ew-algebras
%
%    Note: These identities axiomatise FL_ew-algebras
%    when taken in conjunction with the identities and 
%    quasi-identities axiomatising commutative, integral
%    residuated lattices given above.
%

x v 0 = x                                 # label("(D9)").

%
% Definitions mapping Nelson FL_ew-algebras to Nelson algebras
%

% Definition of -> (weak implication) in Nelson FL_ew-algebras
x -> y = x => (x => y)                    # label("(-> def)").

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

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

%
% Identities axiomatising Nelson FL_ew-algebras. 
%
%    Note: Nelson FL_algebras are 3-potent, distributive classical 
%    FL_ew-algebras satisfying the Nelson identity (N). 
%
%    Note: The identities expressing classicality and the Nelson identity
%    are expressed in terms of the definitions mapping Nelson FL_ew-algebras
%    into Nelson algebras.
%

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

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

~(~x) = x                                 # label("(DN)").  % Classicality

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

%
% Identities which are known consequences of the theory of FL_ew-algebras
%
%    Note: The following identities are known to hold for BCK-algebras, and
%    hence hold for Nelson FL_ew-algebras.
%

(x => y) => ((z => x) => (z => y)) = 1    # label("(BCK1')").
x => ((x => y) => y) = 1                  # label("(BCK5)").
x => x = 1                                # label("(3.16)").
x => (y => x) = 1                         # label("(3.17)").
x => (y => z) = y => (x => z)             # label("(3.18)").

%
%    Note: The following identities are known to hold for commutative,
%    integral residuated lattices, and hence hold for Nelson FL_ew-algebras.
%

(x * y) v (x * z) = x * (y v z)           # label("(4.1)").
(x => y) ^ (x => z) = x => (y ^ z)        # label("(4.2)").
(x * (x => y)) v y = y                    # label("(4.3)").
(x => y) ^ (z => y) = (x v z) => y        # label("(4.4)").
((x => y) * z) => (x => (y * z)) = 1      # label("(4.5)").

end_of_list.

%
% Previous results
%

formulas(assumptions).

% Lemma 4.3

(x => y) ^ y = y                       # label("(3.13)"). % Lemma 4.3 (1)
(x v y) => y = x => y                  # label("(4.6)"). % Lemma 4.3 (2)
x -> (y => z) = y => (x -> z)          # label("(4.7)"). % Lemma 4.3 (3)
x ^ (~x => y) = x                      # label("(4.8)"). % Lemma 4.3 (4)

% Lemma 4.4

x -> ((y v x) -> z) = x -> z           # label("(4.9)"). % Lemma 4.4 (1)
x -> (~x v y) = x -> y                 # label("(4.10)"). % Lemma 4.4 (2)

x -> x = 1                             # label("(N2)"). % Lemma 4.5
(x -> y) ^ (x -> z) = x -> (y ^ z)     # label("(N5)"). % Lemma 4.6
(x -> y) ^ (~x v y) = ~x v y           # label("(N3)"). % Lemma 4.7
(x ^ y) -> z = x -> (y -> z)           # label("(N6)"). % Lemma 4.8

end_of_list.

%
% Current problem (Lemma 4.9)
%

formulas(goals).

x ^ (~x v y) = x ^ (x -> y)            # label("(N4)"). % Lemma 4.9

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

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

end_of_list.