:: Boolean Properties of Lattices :: by Agnieszka Julia Marasik :: :: Received March 28, 1994 :: Copyright (c) 1994-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies LATTICES, SUBSET_1, XBOOLE_0, EQREL_1, PBOOLE; notations STRUCT_0, LATTICES; constructors LATTICES; registrations LATTICES; begin :: General Lattices reserve L for Lattice; reserve X,Y,Z,V for Element of L; definition let L,X,Y; func X \ Y -> Element of L equals :: BOOLEALG:def 1 X "/\" Y`; end; definition let L,X,Y; func X \+\ Y -> Element of L equals :: BOOLEALG:def 2 (X \ Y) "\/" (Y \ X); end; definition let L,X,Y; redefine pred X = Y means :: BOOLEALG:def 3 X [= Y & Y [= X; end; definition let L,X,Y; pred X meets Y means :: BOOLEALG:def 4 X "/\" Y <> Bottom L; end; notation let L,X,Y; antonym X misses Y for X meets Y; end; theorem :: BOOLEALG:1 X "\/" Y [= Z implies X [= Z; theorem :: BOOLEALG:2 X "/\" Y [= X "\/" Z; theorem :: BOOLEALG:3 X [= Z implies X \ Y [= Z; theorem :: BOOLEALG:4 X \ Y [= Z & Y \ X [= Z implies X \+\ Y [= Z; theorem :: BOOLEALG:5 X = Y "\/" Z iff Y [= X & Z [= X & for V st Y [= V & Z [= V holds X [= V; theorem :: BOOLEALG:6 X = Y "/\" Z iff X [= Y & X [= Z & for V st V [= Y & V [= Z holds V [= X; theorem :: BOOLEALG:7 X meets X iff X <> Bottom L; definition let L, X, Y; redefine pred X meets Y; symmetry; redefine func X \+\ Y; commutativity; redefine pred X misses Y; symmetry; end; begin begin :: Distributive Lattices reserve L for D_Lattice; reserve X,Y,Z for Element of L; theorem :: BOOLEALG:8 (X "/\" Y) "\/" (X "/\" Z) = X implies X [= Y "\/" Z; begin :: Distributive Bounded Lattices reserve L for 0_Lattice; reserve X,Y,Z for Element of L; theorem :: BOOLEALG:9 X [= Bottom L implies X = Bottom L; theorem :: BOOLEALG:10 X [= Y & X [= Z & Y "/\" Z = Bottom L implies X = Bottom L; theorem :: BOOLEALG:11 X "\/" Y = Bottom L iff X = Bottom L & Y = Bottom L; theorem :: BOOLEALG:12 X [= Y & Y "/\" Z = Bottom L implies X "/\" Z = Bottom L; theorem :: BOOLEALG:13 X meets Y & Y [= Z implies X meets Z; theorem :: BOOLEALG:14 X meets Y "/\" Z implies X meets Y & X meets Z; theorem :: BOOLEALG:15 X meets Y \ Z implies X meets Y; theorem :: BOOLEALG:16 X misses Bottom L; theorem :: BOOLEALG:17 X misses Z & Y [= Z implies X misses Y; theorem :: BOOLEALG:18 X misses Y or X misses Z implies X misses Y "/\" Z; theorem :: BOOLEALG:19 X [= Y & X [= Z & Y misses Z implies X = Bottom L; theorem :: BOOLEALG:20 X misses Y implies (Z "/\" X) misses (Z "/\" Y); begin :: Boolean Lattices reserve L for B_Lattice; reserve X,Y,Z,V for Element of L; theorem :: BOOLEALG:21 X \ Y [= Z implies X [= Y "\/" Z; theorem :: BOOLEALG:22 X [= Y implies Z \ Y [= Z \ X; theorem :: BOOLEALG:23 X [= Y & Z [= V implies X \ V [= Y \ Z; theorem :: BOOLEALG:24 X [= Y "\/" Z implies X \ Y [= Z; theorem :: BOOLEALG:25 X` [= (X "/\" Y)`; theorem :: BOOLEALG:26 (X "\/" Y)` [= X`; theorem :: BOOLEALG:27 X [= Y \ X implies X = Bottom L; theorem :: BOOLEALG:28 X [= Y implies Y = X "\/" (Y \ X); theorem :: BOOLEALG:29 X \ Y = Bottom L iff X [= Y; theorem :: BOOLEALG:30 X [= (Y "\/" Z) & X "/\" Z = Bottom L implies X [= Y; theorem :: BOOLEALG:31 X "\/" Y = (X \ Y) "\/" Y; theorem :: BOOLEALG:32 X \ (X "\/" Y) = Bottom L; theorem :: BOOLEALG:33 X \ X "/\" Y = X \ Y; theorem :: BOOLEALG:34 (X \ Y) "/\" Y = Bottom L; theorem :: BOOLEALG:35 X "\/" (Y \ X) = X "\/" Y; theorem :: BOOLEALG:36 (X "/\" Y) "\/" (X \ Y) = X; theorem :: BOOLEALG:37 X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z); theorem :: BOOLEALG:38 X \ (X \ Y) = X "/\" Y; theorem :: BOOLEALG:39 (X "\/" Y) \ Y = X \ Y; theorem :: BOOLEALG:40 X "/\" Y = Bottom L iff X \ Y = X; theorem :: BOOLEALG:41 X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z); theorem :: BOOLEALG:42 X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z); theorem :: BOOLEALG:43 X "/\" (Y \ Z) = X "/\" Y \ X "/\" Z; theorem :: BOOLEALG:44 (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X); theorem :: BOOLEALG:45 (X \ Y) \ Z = X \ (Y "\/" Z); theorem :: BOOLEALG:46 X \ Y = Y \ X implies X = Y; theorem :: BOOLEALG:47 X \ Bottom L = X; theorem :: BOOLEALG:48 (X \ Y)` = X` "\/" Y; theorem :: BOOLEALG:49 X meets Y "\/" Z iff X meets Y or X meets Z; theorem :: BOOLEALG:50 X "/\" Y misses X \ Y; theorem :: BOOLEALG:51 X misses Y "\/" Z iff X misses Y & X misses Z; theorem :: BOOLEALG:52 (X \ Y) misses Y; theorem :: BOOLEALG:53 X misses Y implies (X "\/" Y) \ Y = X; theorem :: BOOLEALG:54 X` "\/" Y` = X "\/" Y & X misses X` & Y misses Y` implies X = Y` & Y = X`; theorem :: BOOLEALG:55 X` "\/" Y` = X "\/" Y & Y misses X` & X misses Y` implies X = X` & Y = Y`; theorem :: BOOLEALG:56 X \+\ Bottom L = X; theorem :: BOOLEALG:57 X \+\ X = Bottom L; theorem :: BOOLEALG:58 X "/\" Y misses X \+\ Y; theorem :: BOOLEALG:59 X "\/" Y = X \+\ (Y \ X); theorem :: BOOLEALG:60 X \+\ (X "/\" Y) = X \ Y; theorem :: BOOLEALG:61 X "\/" Y = (X \+\ Y) "\/" (X "/\" Y); theorem :: BOOLEALG:62 (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y; theorem :: BOOLEALG:63 (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y; theorem :: BOOLEALG:64 X \+\ Y = (X "\/" Y) \ (X "/\" Y); theorem :: BOOLEALG:65 (X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z)); theorem :: BOOLEALG:66 X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" (X "/\" Y "/\" Z); theorem :: BOOLEALG:67 (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z); theorem :: BOOLEALG:68 (X \+\ Y)` = (X "/\" Y) "\/" (X` "/\" Y`);