assign(report_stderr, 2).
set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
  assign(max_seconds, 6000).
end_if.

if(Mace4).   % Options for Mace4
  assign(max_seconds, 6000).
end_if.

formulas(assumptions).

% lattice theory

%L2v
x v y = y v x.
%L3v
(x v y) v z = x v (y v z).
%L2^
x ^ y = y ^ x.
%L3^
(x ^ y) ^ z = x^ (y ^ z).
%L4^
x ^ (x v y) = x.
%L4v
x v (x ^ y) = x.

%Boundedness
%L5v
0 v x = x.
%L5^
0 ^ x = 0.
%L6v
1 v x = 1.
%L6^
x ^ 1 = x.

% Lemma of Uni: Distributivity
x ^ (y v z) = (x ^ y) v (x ^ z).
% Lemma of Uni: Dual distributivity
x v (y ^ z) = (x v y) ^ (x v z).

%C0
-C(0,x).
%-C(x,0).
%C1
x!= 0 -> C(x,x).
%C2
C(x,y) <-> C(y,x).
%C3
(C(x,y) & y ^ z = y) -> C(x,z).

%x!=0 & P(x,y) -> C(x,y).

%Ext"
%(all z (C(x,z) <-> C(y,z))) <-> x=y.
%Ext'
%(all z (C(x,z) -> C(y,z))) <-> P(x,y).
%Dis (Disconnection axiom, it is implied by Ext" or Ext', therefore the proof we get is sufficient to show that (Ext") instead also proves (C4).
(all x (x != 1 -> (exists y (y != 0 & -C(x,y) ) ) ) ).

% Lemma
x != 0 -> C(x,1).

% Lemma: define (Boolean) complementation
x ^ x' = 0.
x v x' = 1.
% Lemma: require complementation
x' ' = x.
0' = 1.
1' = 0.

%enforce that C4 does not hold:
(exists x exists y exists z (C(x, y v z) & -C(x,y) & -C(x,z))).

end_of_list.

formulas(goals).

% -Con is inconsistent in non-trivial lattices, i.e. exists an x!=0,1 s.t. C(x,x')
(exists y (exists z (y!=1 & z!=1 & C(y,z)))) -> (exists x (x!=0 & x!=1 & C(x,x'))).

end_of_list.

