assign(max_seconds, 60). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Reference % % On Some Ternary Relations in Lattices % R. Padmanabhan % Colloquium Mathematicum 15:195-198, 1966. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% set(expand_relational_defs). 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"). 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.