% Problem: Lattice-ordered Pregroups
% Status:  Open Problem
%
% A lattice-ordered pregroup is a residuated lattice with additional
% operations l(x) and r(x) which are, roughly speaking, left and right
% inverses. The structure generalizes lattice-ordered groups and are
% used to model grammars.
%
% Problem: Is every lattice-ordered pregroup distributive?
%
% Galatos & Jipsen showed that the answer is affirmative in case
% l(l(...(x)...)) = r(r(...(x)...)) where there are the same number
% l's and r's on both sides.
%
% N. Galatos & P. Jipsen, Periodic lattice-ordered pregroups are
% distributive, Algebra Universalis, 2012.
%
% Using Waldmeister, I managed to show that lattice-ordered pregroups
% are semidistributive. I have never managed to get this using Prover9.
% I did not include this result as a lemma below.
%
% Thus to answer the question affirmatively, it
% is enough to show that lattice-ordered pregroups are modular.
%
% The Galatos/Jipsen paper has many lemmas which might be useful.
% I have not included them in this bare bones file.
% Also, there are many possible signatures in which to formulate the
% problem; this is just one of the easier ones.

formulas(assumptions).

% lattice
x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z).
x v y = y v x. (x v y) v z = x v (y v z).
x v (x ^ y) = x. x ^ (x v y) = x.

% monoid
1 * x = x. x * 1 = x.
(x * y) * z = x * (y * z).

% compatibility
(x * y) ^ (x * z) = x * (y ^ z).
(y * x) ^ (z * x) = (y ^ z) * x.
(x * y) v (x * z) = x * (y v z).
(y * x) v (z * x) = (y v z) * x.

% l and r
l(r(x)) = x. r(l(x)) = x.
x * (l(x) * x) = x. x * (r(x) * x) = x.
l(x) * (x * l(x)) = l(x). r(x) * (x * r(x)) = r(x).
l(x * y) = l(y) * l(x). r(x * y) = r(y) * r(x).
l(x ^ y) = l(x) v l(y). l(x v y) = l(x) ^ l(y).
r(x ^ y) = r(x) v r(y). r(x v y) = r(x) ^ r(y).

% pregroup conditions
(l(x) * x) v 1 = 1.  (x * l(x)) ^ 1 = 1.
(x * r(x)) v 1 = 1.  (r(x) * x) ^ 1 = 1.

% modular?
b v c = c.  a v b = a v c.  a ^ b = a ^ c.  b != c.

end_of_list.
