% problem-set/algebra/lattices/SAMslemma.ver1.clauses    
% created : 07/09/86                                        
% revised : 07/08/88                                        

% description:
%
%   Sam's Lemma may be stated as follows:                        
%                                                               
%   Let L be a modular lattice with 0 and 1.  Suppose that      
%   A and B are elements of L such that (A v B) and (A ^ B)     
%   both have not necessarily unique complements.               
%                                                               
%   Then, one can prove                                         
%                                                               
%   ((A v B)' v ((A ^ B)' ^ B)) ^                               
%   ((A v B)' v ((A ^ B)' ^ A))     =    (A v B)'               

% representation:
%
% declare_predicates(3,[MAX,MIN]).
% declare_constants([a,a2,a3,b,b2,b3,c,c2,c3,d,e,d2,e2,a3,b3,c1,c0]).
% declare_variables([x,y,z,x1,y1,z1,xy,yz,xyz]).
%
% Meanings of predicates and functions used in the following clauses :
% MAX(x,y,z) : means z as the union of x and y                   
% MIN(x,y,z) : means z as the intersection of x and y            
% c0         : is the constant used to represent the number '0'  
% c1         : is the constant used to represent the number '1'  


% Union of 1 and x is equal to 1 :  (1 v X) = 1               

MAX(c1,x,c1).

% Union of x with itself is equal to x :  (X v X) = X         

MAX(x,x,x).

% Union of 0 and x is equal to x :  (0 v X) = X               

MAX(c0,x,x).

% Intersection of 0 and x is equal to 0 : (0 ^ X) = 0        

MIN(c0,x,c0).

% Intersection of x and itself is equal to x : (X ^ X) = X  

MIN(x,x,x).

% Intersection of 1 and x is equal to itself : (1 ^ X) = X  

MIN(c1,x,x).

% Intersection of x and y , is the same as intersection of y and x. % 
%   (X ^ Y) = (Y ^ X)                                                

-MIN(x,y,z)   | MIN(y,x,z).

% Union of x and y is the same as union of y and x. (X v Y) = (Y v X) 

-MAX(x,y,z)   | MAX(y,x,z).

% Union of x with the intersection of x and y is the same as x.     
%   X v (X ^ Y) = X                                                 

-MIN(x,y,z)   | MAX(x,z,x).

% Intersection  of x with the union of x and y is the same as x.     
%   X ^ (X v Y) = X                                                 

-MAX(x,y,z)   | MIN(x,z,x).

% The operation '^', intersection ,is associative  X ^ (Y ^ Z) = (X ^ Y) ^ Z 

-MIN(x,y,xy)  | -MIN(y,z,yz) | -MIN(x,yz,xyz)    | MIN(xy,z,xyz).
-MIN(x,y,xy)  | -MIN(y,z,yz) | -MIN(xy,z,xyz)    | MIN(x,yz,xyz).

% The operation 'v' is associative X v (Y v Z) = (X v Y) v Z   

-MAX(x,y,xy)  | -MAX(y,z,yz) | -MAX(x,yz,xyz)    | MAX(xy,z,xyz).
-MAX(x,y,xy)  | -MAX(y,z,yz) | -MAX(xy,z,xyz)    | MAX(x,yz,xyz).

% (X ^ Z) = X implies that (Z ^ (X v Y)) =  (X v (Y ^ Z))        

-MIN(x,z,x)   | -MAX(x,y,x1) | -MIN(y,z,y1) | -MIN(z,x1,z1) | MAX(x,y1,z1).
-MIN(x,z,x)   | -MAX(x,y,x1) | -MIN(y,z,y1) | -MAX(x,y1,z1) | MIN(z,x1,z1).

% (X ^ Z) = Z implies that (X ^ (Y v Z)) = (Z v (X ^ Y))        

-MIN(x,z,z)   | -MAX(y,z,y1) | -MIN(x,y,x1) | -MIN(x,y1,z1) | MAX(z,x1,z1).
-MIN(x,z,z)   | -MAX(y,z,y1) | -MIN(x,y,x1) | -MAX(z,x1,z1) | MIN(x,y1,z1).


% Negation of Sams Lemma :                                       
% The following can be obtained by using the fact that            
% if x v y = 1 and  x ^ y = 0 then x = y'                         

% a intersection b is equal to c : a ^ b = c  

MIN(a,b,c).

% The union of d and c is equal to 1 : d v c = c1

MAX(d,c,c1).

% b union d is equal to e : b v d = e 

MIN(b,d,e).

% a union e is equal to 0 :  a v e = c0 

MIN(a,e,c0).

% b union a2 is equal to b2 : b v a2 = b2 

MAX(b,a2,b2).

% a union b2 is equal to c1 :  (a v b2) = c1 

MAX(a,b2,c1).

% a union b is equal to c2 : (a v b) = c2 

MAX(a,b,c2).

% a2 intersection c2 is equal to c0 :  a2 ^ c2 = c0 

MIN(a2,c2,c0).

% d intersection a is equal to d2 : (d ^ a) = d2 

MIN(d,a,d2).

% a2 union d2 is equal to e2 : (a2 v d2) = e2 

MAX(a2,d2,e2).

% b intersection d is equal to a3 :  (b ^ d) = a3 

MIN(d,b,a3).

% a2 union a3 is equal to b3 : (a2 v a3) = b3 

MAX(a2,a3,b3).

% the intersection of b3 and e2 is not equal to a2 : (b3 ^ e2) <> a2 

-MIN(b3,e2,a2).