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

end_of_list.

formulas(goals).

x => x = y => y       # label("(7)").
~x = x => ~(y => y)   # label("(8)").
x => y = ~y => ~x     # label("(9)").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

x => 1 = 1.
1 = (1 => x) => x.
(1 => x) => x = 1.
x => ~ y = y => ~ x.
1 = ((x => 1) => y) => y.
((x => 1) => y) => y = 1.
1 => x = x.
x => x = 1.
1 = x => (y => y).
x => (y => y) = 1.
x => x = y => y.
(x => 1) => y = y.
(x => x) => y = y.
~ x = x => ~ (y => y).
x => ~ (y => y) = ~ x.

end_of_list.
