% problem-set/algebra/lattices/SAMslemma.ver1.in % 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' set(hyper_res). clear(back_sub). list(axioms). % 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). end_of_list. list(sos). % 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). end_of_list.