%
% 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)

end_of_list.

%
% Current problem (Lemma 4.5)
%

formulas(goals).

x -> x = 1                             # label("(N2)"). % Lemma 4.5

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

1 = x -> x.

end_of_list.
