
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Reference
%
%    On Some Ternary Relations in Lattices
%    R. Padmanabhan
%    Colloquium Mathematicum 15:195-198, 1966.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

formulas(assumptions).

% Lattice Theory

x ^ y = y ^ x                # label("commutativity_meet").
x v y = y v x                # label("commutativity_join").
(x ^ y) ^ z = x ^ (y ^ z)    # label("associativity_meet").
(x v y) v z = x v (y v z)    # label("associativity_join").
(x v y) ^ x = x              # label("absorption_1").
(x ^ y) v x = x              # label("absorption_2").

% Assume, for this experiment, 0 and 1.

x ^ 1 = x.
x v 0 = x.

end_of_list.

formulas(assumptions).

% Definition of less-than-or-equal

all x all y ((x <= y) <-> x ^ y = x).

% Definitions of ternary relations

all x all y all z (A(x,y,z)
    <-> ((x <= y & y <= z) | (z <= y & y <= x))).

all x all y all z (B(x,y,z)
    <-> (((x ^ y) v (y ^ z) = y) & ((x v y) ^ (y v z) = y))).
 
% all x all y all z (C(x,y,z)
%    <-> ((((x ^ y) v (y ^ z)) = y) & ((x ^ z) v y = y))).
% 
% all x all y all z (CS(x,y,z)
%    <-> ((((x v y) ^ (y v z)) = y) & ((x v z) ^ y = y))).
%  
% all x all y all z (D(x,y,z)
%    <-> ( ((x ^ z) <= y) & (y <= (x v z)))).

end_of_list.

formulas(goals).

% The following is not a theorem.

all a all x all b (  B(a,x,b) ->  A(a,x,b)).

end_of_list.
