:: Boolean Properties of Lattices :: by Agnieszka Julia Marasik :: :: Received March 28, 1994 :: Copyright (c) 1994-2018 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; theorems LATTICES, FILTER_0, LATTICE4; 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 X "/\" Y`; coherence; end; definition let L,X,Y; func X \+\ Y -> Element of L equals (X \ Y) "\/" (Y \ X); coherence; end; definition let L,X,Y; redefine pred X = Y means X [= Y & Y [= X; compatibility by LATTICES:8; end; definition let L,X,Y; pred X meets Y means X "/\" Y <> Bottom L; end; notation let L,X,Y; antonym X misses Y for X meets Y; end; theorem X "\/" Y [= Z implies X [= Z proof assume X "\/" Y [= Z; then X "/\" (X "\/" Y) [= X "/\" Z by LATTICES:9; then A1: X [= X "/\" Z by LATTICES:def 9; X "/\" Z [= Z by LATTICES:6; hence thesis by A1,LATTICES:7; end; theorem X "/\" Y [= X "\/" Z proof X "/\" Y [= X & X [= X "\/" Z by LATTICES:5,6; hence thesis by LATTICES:7; end; theorem X [= Z implies X \ Y [= Z proof assume X [= Z; then A1: X "/\" Y` [= Z "/\" Y` by LATTICES:9; Z "/\" Y` [= Z by LATTICES:6; hence thesis by A1,LATTICES:7; end; theorem X \ Y [= Z & Y \ X [= Z implies X \+\ Y [= Z by FILTER_0:6; theorem X = Y "\/" Z iff Y [= X & Z [= X & for V st Y [= V & Z [= V holds X [= V proof thus X = Y "\/" Z implies Y [= X & Z [= X & for V st Y [= V & Z [= V holds X [= V by FILTER_0:6,LATTICES:5; assume that A1: Y [= X & Z [= X and A2: for V st Y [= V & Z [= V holds X [= V; A3: Y "\/" Z [= X by A1,FILTER_0:6; Y [= Y "\/" Z & Z [= Y "\/" Z by LATTICES:5; then X [= Y "\/" Z by A2; hence thesis by A3; end; theorem X = Y "/\" Z iff X [= Y & X [= Z & for V st V [= Y & V [= Z holds V [= X proof thus X = Y "/\" Z implies X [= Y & X [= Z & for V st V [= Y & V [= Z holds V [= X by FILTER_0:7,LATTICES:6; assume that A1: X [= Y & X [= Z and A2: for V st V [= Y & V [= Z holds V [= X; A3: X [= Y "/\" Z by A1,FILTER_0:7; Y "/\" Z [= Y & Y "/\" Z [= Z by LATTICES:6; then Y "/\" Z [= X by A2; hence thesis by A3; end; theorem 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 (X "/\" Y) "\/" (X "/\" Z) = X implies X [= Y "\/" Z proof assume (X "/\" Y) "\/" (X "/\" Z) = X; then X "/\" (Y "\/" Z) = X by LATTICES:def 11; hence thesis by LATTICES:4; end; begin :: Distributive Bounded Lattices reserve L for 0_Lattice; reserve X,Y,Z for Element of L; theorem Th9: X [= Bottom L implies X = Bottom L by LATTICES:16; theorem X [= Y & X [= Z & Y "/\" Z = Bottom L implies X = Bottom L by Th9,FILTER_0:7; theorem Th11: X "\/" Y = Bottom L iff X = Bottom L & Y = Bottom L by LATTICES:5,LATTICES:16; theorem X [= Y & Y "/\" Z = Bottom L implies X "/\" Z = Bottom L by Th9,LATTICES:9; theorem Th13: X meets Y & Y [= Z implies X meets Z by Th9,LATTICES:9; theorem Th14: X meets Y "/\" Z implies X meets Y & X meets Z proof assume X meets Y "/\" Z; then A1: X "/\" (Y "/\" Z) <> Bottom L; then X "/\" Z "/\" Y <> Bottom L by LATTICES:def 7; then A2: X "/\" Z <> Bottom L; X "/\" Y "/\" Z <> Bottom L by A1,LATTICES:def 7; then X "/\" Y <> Bottom L; hence thesis by A2; end; theorem X meets Y \ Z implies X meets Y proof assume X meets Y \ Z; then X "/\" (Y \ Z) <> Bottom L; then X "/\" Y "/\" Z` <> Bottom L by LATTICES:def 7; then X "/\" Y <> Bottom L; hence thesis; end; theorem X misses Bottom L; theorem X misses Z & Y [= Z implies X misses Y by Th13; theorem X misses Y or X misses Z implies X misses Y "/\" Z by Th14; theorem X [= Y & X [= Z & Y misses Z implies X = Bottom L by Th9,FILTER_0:7; theorem X misses Y implies (Z "/\" X) misses (Z "/\" Y) proof assume A1: X misses Y; (Z "/\" X) "/\" (Z "/\" Y) = Z "/\" (X "/\" (Y "/\" Z)) by LATTICES:def 7 .= Z "/\" ((X "/\" Y) "/\" Z) by LATTICES:def 7 .= Z "/\" Bottom L by A1 .= Bottom L; hence thesis; end; begin :: Boolean Lattices reserve L for B_Lattice; reserve X,Y,Z,V for Element of L; theorem X \ Y [= Z implies X [= Y "\/" Z proof assume X \ Y [= Z; then Y "\/" (X "/\" Y`) [= Y "\/" Z by FILTER_0:1; then (Y "\/" X) "/\" (Y "\/" Y`) [= Y "\/" Z by LATTICES:11; then A1: (Y "\/" X) "/\" Top L [= Y "\/" Z by LATTICES:21; X [= X "\/" Y by LATTICES:5; hence thesis by A1,LATTICES:7; end; theorem Th22: X [= Y implies Z \ Y [= Z \ X proof assume X [= Y; then Y` [= X` by LATTICES:26; hence thesis by LATTICES:9; end; theorem X [= Y & Z [= V implies X \ V [= Y \ Z proof assume X [= Y & Z [= V; then X \ V [= Y \ V & Y \ V [= Y \ Z by Th22,LATTICES:9; hence thesis by LATTICES:7; end; theorem X [= Y "\/" Z implies X \ Y [= Z proof assume X [= Y "\/" Z; then X "/\" Y` [= (Y "\/" Z) "/\" Y` by LATTICES:9; then X "/\" Y` [= (Y "/\" Y`) "\/" (Z "/\" Y`) by LATTICES:def 11; then A1: X \ Y [= Bottom L "\/" (Z "/\" Y`) by LATTICES:20; Z "/\" Y` [= Z by LATTICES:6; hence thesis by A1,LATTICES:7; end; theorem X` [= (X "/\" Y)` proof X` [= X` "\/" Y` by LATTICES:5; hence thesis by LATTICES:23; end; theorem (X "\/" Y)` [= X` proof (X "\/" Y)` = X` "/\" Y` by LATTICES:24; hence thesis by LATTICES:6; end; theorem X [= Y \ X implies X = Bottom L proof A1: X "/\" (Y "/\" X`) = Y "/\" (X` "/\" X) by LATTICES:def 7 .= Y "/\" Bottom L by LATTICES:20 .= Bottom L; assume X [= Y \ X; hence thesis by A1,LATTICES:4; end; theorem X [= Y implies Y = X "\/" (Y \ X) proof assume A1: X [= Y; Y = Y "/\" Top L .= Y "/\" ( X "\/" X`) by LATTICES:21 .= (Y "/\" X) "\/" ( Y "/\" X`) by LATTICES:def 11 .= X "\/" (Y \ X) by A1,LATTICES:4; hence thesis; end; theorem Th29: X \ Y = Bottom L iff X [= Y proof thus X \ Y = Bottom L implies X [= Y proof A1: X "/\" Y` = Bottom L implies X [= Y`` by LATTICES:25; assume X \ Y = Bottom L; hence thesis by A1; end; assume X [= Y; then X "/\" Y` [= Y` "/\" Y by LATTICES:9; then A2: X "/\" Y` [= Bottom L by LATTICES:20; Bottom L [= X \ Y by LATTICES:16; hence thesis by A2; end; theorem X [= (Y "\/" Z) & X "/\" Z = Bottom L implies X [= Y proof assume that A1: X [= (Y "\/" Z) and A2: X "/\" Z = Bottom L; X "/\" (Y "\/" Z) = X by A1,LATTICES:4; then (X "/\" Y) "\/" Bottom L = X by A2,LATTICES:def 11; hence thesis by LATTICES:4; end; theorem X "\/" Y = (X \ Y) "\/" Y proof thus X "\/" Y = (X "\/" Y) "/\" Top L .= (X "\/" Y) "/\" (Y` "\/" Y) by LATTICES:21 .= (X \ Y) "\/" Y by LATTICES:11; end; theorem X \ (X "\/" Y) = Bottom L by Th29,LATTICES:5; theorem Th33: X \ X "/\" Y = X \ Y proof X \ X "/\" Y = X "/\" (X` "\/" Y`) by LATTICES:23 .= (X "/\" X`) "\/" (X "/\" Y`) by LATTICES:def 11 .= Bottom L "\/" (X "/\" Y`) by LATTICES:20 .= X "/\" Y`; hence thesis; end; theorem (X \ Y) "/\" Y = Bottom L proof (X \ Y) "/\" Y = X "/\" (Y`"/\" Y) by LATTICES:def 7 .= X "/\" Bottom L by LATTICES:20; hence thesis; end; theorem Th35: X "\/" (Y \ X) = X "\/" Y proof X "\/" (Y \ X) = (X "\/" Y) "/\" (X "\/" X`) by LATTICES:11 .= (X "\/" Y) "/\" Top L by LATTICES:21; hence thesis; end; theorem Th36: (X "/\" Y) "\/" (X \ Y) = X proof (X "/\" Y) "\/" (X \ Y) =((X "/\" Y) "\/" X) "/\" ((X "/\" Y) "\/" Y`) by LATTICES:11 .= X "/\" ((X "/\" Y) "\/" Y`) by LATTICES:def 8 .= X "/\" ((X "\/" Y`) "/\" (Y "\/" Y`)) by LATTICES:11 .= X "/\" ((X "\/" Y`) "/\" Top L) by LATTICES:21 .= X by LATTICES:def 9; hence thesis; end; theorem Th37: X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z) proof X \ (Y \ Z) = X "/\" (Y`"\/" Z``) by LATTICES:23 .= X "/\" (Y`"\/" Z) .= (X "/\" Y`) "\/" (X "/\" Z) by LATTICES:def 11; hence thesis; end; theorem X \ (X \ Y) = X "/\" Y proof X \ (X \ Y) = X "/\" (X` "\/" Y``) by LATTICES:23 .= X "/\" (X` "\/" Y) .= (X "/\" X`) "\/" (X "/\" Y) by LATTICES:def 11 .= Bottom L "\/" (X "/\" Y) by LATTICES:20; hence thesis; end; theorem (X "\/" Y) \ Y = X \ Y proof (X "\/" Y) \ Y = (X "/\" Y`) "\/" (Y "/\" Y`) by LATTICES:def 11 .= (X "/\" Y`) "\/" Bottom L by LATTICES:20 .= X "/\" Y`; hence thesis; end; theorem X "/\" Y = Bottom L iff X \ Y = X proof thus X "/\" Y = Bottom L implies X \ Y = X proof assume X "/\" Y = Bottom L; then A1: X "/\" X [= X "/\" Y` by LATTICES:9,25; X \ Y [= X by LATTICES:6; hence thesis by A1; end; assume X \ Y = X; then X` "\/" Y`` = X` by LATTICES:23; then X "/\" (X` "\/" Y) [= X "/\" X`; then (X "/\" X`) "\/" (X "/\" Y) [= X "/\" X` by LATTICES:def 11; then Bottom L "\/" (X "/\" Y) [= X "/\" X` by LATTICES:20; then A2: X "/\" Y [= Bottom L by LATTICES:20; Bottom L [= X "/\" Y by LATTICES:16; hence thesis by A2; end; theorem X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z) proof thus X \ (Y "\/" Z) = X "/\" (Y` "/\" Z`) by LATTICES:24 .= (X "/\" X "/\" Y`) "/\" Z` by LATTICES:def 7 .= (X "/\" (X "/\" Y`)) "/\" Z` by LATTICES:def 7 .= (X \ Y) "/\" (X \ Z) by LATTICES:def 7; end; theorem Th42: X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z) proof thus X \ (Y "/\" Z) = X "/\" (Y` "\/" Z`) by LATTICES:23 .= (X \ Y) "\/" (X \ Z) by LATTICES:def 11; end; theorem X "/\" (Y \ Z) = X "/\" Y \ X "/\" Z proof X "/\" Y \ X "/\" Z = ((X "/\" Y) \ X) "\/" ((X "/\" Y) \ Z) by Th42 .= Bottom L "\/" ((X "/\" Y) \ Z) by Th29,LATTICES:6 .= (X "/\" Y) \ Z; hence thesis by LATTICES:def 7; end; theorem Th44: (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X) proof (X "\/" Y) \ (X "/\" Y) = (X "\/" Y) "/\" (X` "\/" Y`) by LATTICES:23 .= ((X "\/" Y) "/\" X`) "\/" ((X "\/" Y) "/\" Y`) by LATTICES:def 11 .= ((X "/\" X`) "\/" (Y "/\" X`)) "\/" ((X "\/" Y) "/\" Y`) by LATTICES:def 11 .= ((X "/\" X`) "\/" (Y "/\" X`)) "\/" ((X "/\" Y`) "\/" (Y "/\" Y`)) by LATTICES:def 11 .= (Bottom L "\/" (Y "/\" X`)) "\/" ((X "/\" Y`) "\/" (Y "/\" Y`)) by LATTICES:20 .= (Y "/\" X`) "\/" ((X "/\" Y`) "\/" Bottom L) by LATTICES:20 .= (X \ Y) "\/" (Y \ X); hence thesis; end; theorem Th45: (X \ Y) \ Z = X \ (Y "\/" Z) proof thus (X \ Y) \ Z = X "/\" (Y` "/\" Z`) by LATTICES:def 7 .= X \ (Y "\/" Z) by LATTICES:24; end; theorem X \ Y = Y \ X implies X = Y proof assume A1: X \ Y = Y \ X; then (X "/\" Y`) "/\" X = Y "/\" (X` "/\" X) by LATTICES:def 7 .= Y "/\" Bottom L by LATTICES:20 .= Bottom L; then (X "/\" X) "/\" Y` = Bottom L by LATTICES:def 7; then (X "/\" Y`) "\/" X`= (X "/\" X`) "\/" X` by LATTICES:20 .= X` by LATTICES:def 8; then (X "\/" X`) "/\" (Y` "\/" X`) = X` by LATTICES:11; then Top L "/\" (Y` "\/" X`) = X` by LATTICES:21; then Y` "/\" X` = Y` by LATTICES:def 9; then X`` [= Y`` by LATTICES:4,26; then X [= Y``; then A2: X [= Y; X "/\" (Y` "/\" Y) = (Y "/\" X`) "/\" Y by A1,LATTICES:def 7; then X "/\" Bottom L = (Y "/\" X`) "/\" Y by LATTICES:20; then Bottom L = X` "/\" (Y "/\" Y) by LATTICES:def 7 .= X` "/\" Y; then Y [= X`` by LATTICES:25; then Y [= X; hence thesis by A2; end; theorem Th47: X \ Bottom L = X proof X \ Bottom L = X "/\" Top L by LATTICE4:30 .= X; hence thesis; end; theorem (X \ Y)` = X` "\/" Y proof (X \ Y)` = X` "\/" Y`` by LATTICES:23; hence thesis; end; theorem Th49: X meets Y "\/" Z iff X meets Y or X meets Z proof thus X meets Y "\/" Z implies X meets Y or X meets Z proof assume X meets Y "\/" Z; then X "/\" (Y "\/" Z) <> Bottom L; then (X "/\" Y) "\/" (X "/\" Z) <> Bottom L by LATTICES:def 11; then (X "/\" Y) <> Bottom L or (X "/\" Z) <> Bottom L; hence thesis; end; assume A1: X meets Y or X meets Z; per cases by A1; suppose A2: X meets Y; X "/\" Y [= (X "/\" Y) "\/" (X "/\" Z) by LATTICES:5; then A3: X "/\" Y [= X "/\" (Y "\/" Z) by LATTICES:def 11; X "/\" (Y "\/" Z) <> Bottom L by A3,Th9,A2; hence thesis; end; suppose A4: X meets Z; A5: (X "/\" Z) "\/" (X "/\" Y) = X "/\" (Y "\/" Z) by LATTICES:def 11; X "/\" Z <> Bottom L by A4; then X "/\" (Y "\/" Z) <> Bottom L by A5,Th11; hence thesis; end; end; theorem Th50: X "/\" Y misses X \ Y proof (X "/\" Y) "/\" (X \ Y) = (X "/\" Y "/\" Y`) "/\" X by LATTICES:def 7 .= (X "/\" (Y "/\" Y`)) "/\" X by LATTICES:def 7 .= Bottom L "/\" X by LATTICES:20 .= Bottom L; hence thesis; end; theorem X misses Y "\/" Z iff X misses Y & X misses Z by Th49; theorem (X \ Y) misses Y proof (X \ Y) "/\" Y = X "/\" (Y` "/\" Y) by LATTICES:def 7 .= X "/\" Bottom L by LATTICES:20 .= Bottom L; hence thesis; end; theorem X misses Y implies (X "\/" Y) \ Y = X proof assume X "/\" Y = Bottom L; then X` "\/" (X "/\" Y) = X`; then (X` "\/" X) "/\" (X` "\/" Y) = X` by LATTICES:11; then Top L "/\" (X` "\/" Y) = X` by LATTICES:21; then (X` "\/" Y)` = X; then A1: X`` "/\" Y` = X by LATTICES:24; (X "\/" Y) \ Y = (X "/\" Y`) "\/" (Y "/\" Y`) by LATTICES:def 11 .= (X "/\" Y`) "\/" Bottom L by LATTICES:20 .= X "/\" Y`; hence thesis by A1; end; theorem X` "\/" Y` = X "\/" Y & X misses X` & Y misses Y` implies X = Y` & Y = X` proof assume that A1: X` "\/" Y` = X "\/" Y and A2: X misses X` and A3: Y misses Y`; A4: X "/\" X`= Bottom L by A2; A5: Y "/\" Y` = Bottom L by A3; then A6: Y` "/\" (X` "\/" Y`) = (Y` "/\" X) "\/" Bottom L by A1,LATTICES:def 11; (Y "/\" X`) "\/" (Y "/\" Y`) = Y "/\" (X "\/" Y) by A1,LATTICES:def 11; then Y "/\" X` = Y "/\" (X "\/" Y) by A5; then A7: Y "/\" X` = Y by LATTICES:def 9; (X "/\" X`) "\/" (X "/\" Y`) = X "/\" (X "\/" Y) by A1,LATTICES:def 11; then X "/\" Y` = X "/\" (X "\/" Y) by A4 .= X by LATTICES:def 9; hence X = Y` by A6,LATTICES:def 9; X` "/\" (X` "\/" Y`) = Bottom L "\/" (X` "/\" Y) by A1,A4,LATTICES:def 11; hence thesis by A7,LATTICES:def 9; end; theorem X` "\/" Y` = X "\/" Y & Y misses X` & X misses Y` implies X = X` & Y = Y` proof assume that A1: X` "\/" Y` = X "\/" Y and A2: Y misses X` and A3: X misses Y`; A4: Y "/\" X` = Bottom L by A2; then (X "\/" Y) "/\" (X "\/" X`) = X "\/" Bottom L by LATTICES:11; then (X "\/" Y) "/\" Top L = X by LATTICES:21; then (Y "/\" X)` [= Y` by LATTICES:def 9; then A5: X "\/" Y [= Y` by A1,LATTICES:23; A6: X "/\" Y` = Bottom L by A3; then (Y "\/" X) "/\" (Y "\/" Y`) = Y "\/" Bottom L by LATTICES:11; then (Y "\/" X) "/\" Top L = Y by LATTICES:21; then (X "/\" Y)` [= X` by LATTICES:def 9; then A7: X "\/" Y [= X` by A1,LATTICES:23; (Y` "\/" Y) "/\" (Y` "\/" X`) = Y` "\/" Bottom L by A4,LATTICES:11; then Top L "/\" (Y` "\/" X`) = Y` by LATTICES:21; then (X` "/\" Y`)` [= X`` by LATTICES:def 9; then (X` "/\" Y`)` [= X; then X`` "\/" Y`` [= X by LATTICES:23; then X "\/" Y`` [= X; then A8: X` "\/" Y` [= X by A1; X` [= X` "\/" Y` by LATTICES:5; then A9: X` [= X by A8,LATTICES:7; (X` "\/" X) "/\" (X` "\/" Y`) = X` "\/" Bottom L by A6,LATTICES:11; then Top L "/\" (X` "\/" Y`)= X` by LATTICES:21; then (Y` "/\" X`)` [= Y`` by LATTICES:def 9; then Y`` "\/" X`` [= Y`` by LATTICES:23; then Y`` "\/" X`` [= Y; then Y`` "\/" X [= Y; then A10: X` "\/" Y` [= Y by A1; Y` [= X` "\/" Y` by LATTICES:5; then A11: Y` [= Y by A10,LATTICES:7; X [= X "\/" Y by LATTICES:5; then A12: X [= X` by A7,LATTICES:7; Y [= X "\/" Y by LATTICES:5; then Y [= Y` by A5,LATTICES:7; hence thesis by A11,A9,A12; end; theorem X \+\ Bottom L = X by Th47; theorem X \+\ X = Bottom L by LATTICES:20; theorem X "/\" Y misses X \+\ Y proof X "/\" Y misses X \ Y & X "/\" Y misses Y \ X by Th50; hence thesis by Th49; end; theorem X "\/" Y = X \+\ (Y \ X) proof X "\/" Y = (X "\/" Y) "/\" Top L .= (X "\/" Y) "/\" (X "\/" X`) by LATTICES:21 .= X "\/" (Y "/\" X`) by LATTICES:11 .= ((X "/\" Y`) "\/" (X "/\" X)) "\/" (Y "/\" X`) by LATTICES:def 8 .= ((X "/\" Y`) "\/" (X "/\" X``)) "\/" (Y "/\" (X` "/\" X`)) .= (X "/\" (Y` "\/" X``)) "\/" (Y "/\" (X` "/\" X`)) by LATTICES:def 11 .= (X "/\" (Y "/\" X`)`) "\/" (Y "/\" (X` "/\" X`)) by LATTICES:23 .= X \+\ (Y \ X) by LATTICES:def 7; hence thesis; end; theorem X \+\ (X "/\" Y) = X \ Y proof X \+\ (X "/\" Y) = (X "/\" (X "/\" Y)`) "\/" (Y "/\" (X "/\" X`)) by LATTICES:def 7 .= (X "/\" (X "/\" Y)`) "\/" (Y "/\" Bottom L) by LATTICES:20 .= X "/\" (X` "\/" Y`) by LATTICES:23 .= (X "/\" X`) "\/" (X "/\" Y`) by LATTICES:def 11 .= Bottom L "\/" (X "/\" Y`) by LATTICES:20 .= X "/\" Y`; hence thesis; end; theorem X "\/" Y = (X \+\ Y) "\/" (X "/\" Y) proof thus X "\/" Y = (Y \ X) "\/" X by Th35 .= (Y \ X) "\/" ((X \ Y) "\/" (X "/\" Y)) by Th36 .= (X \+\ Y) "\/" (X "/\" Y) by LATTICES:def 5; end; Lm1: (X "\/" Y) \ (X \+\ Y) = X "/\" Y proof set XY = X "\/" Y; thus XY \ (X \+\ Y) = XY "/\" ((X "/\" Y`)` "/\" (Y "/\" X`)`) by LATTICES:24 .= XY "/\" ((X "/\" Y`)` "/\" (Y` "\/" X``)) by LATTICES:23 .= XY "/\" ((X` "\/" Y``) "/\" (Y` "\/" X``)) by LATTICES:23 .= XY "/\" ((X` "\/" Y``) "/\" (Y` "\/" X)) .= XY "/\" ((X` "\/" Y) "/\" (Y` "\/" X)) .= (XY "/\" (X` "\/" Y)) "/\" (Y` "\/" X) by LATTICES:def 7 .= ( (XY "/\" X`) "\/" ((X "\/" Y) "/\" Y) ) "/\" (Y` "\/" X) by LATTICES:def 11 .= ( (XY "/\" X`) "\/" Y ) "/\" (Y` "\/" X) by LATTICES:def 9 .= ( ((X "/\" X`) "\/" (Y "/\" X`)) "\/" Y ) "/\" (Y` "\/" X) by LATTICES:def 11 .= ( (Bottom L "\/" (Y "/\" X`)) "\/" Y ) "/\" (Y` "\/" X) by LATTICES:20 .= Y "/\" (Y` "\/" X) by LATTICES:def 8 .= (Y "/\" Y`) "\/" (Y "/\" X) by LATTICES:def 11 .= Bottom L "\/" (Y "/\" X) by LATTICES:20 .= X "/\" Y; end; theorem (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y proof set XY = X \+\ Y, A = Y "/\" X`; XY \+\ (X "/\" Y) = (XY "/\" (X` "\/" Y`)) "\/" ((X "/\" Y) "/\" XY`) by LATTICES:23 .= ( (XY "/\" X`) "\/" (XY "/\" Y`) ) "\/" ((X "/\" Y) "/\" XY`) by LATTICES:def 11 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Y) "/\" ((X "/\" Y`)` "/\" A `) ) by LATTICES:24 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Y) "/\" ((X` "\/" Y``) "/\" A`) ) by LATTICES:23 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Y) "/\" ((X` "\/" Y``) "/\" (Y` "\/" X``)) ) by LATTICES:23 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Y) "/\" ((X` "\/" Y) "/\" (Y ` "\/" X``)) ) .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Y) "/\" ((X` "\/" Y) "/\" (Y ` "\/" X)) ) .= ( (XY \ X) "\/" (XY \ Y) ) "\/" (((X "/\" Y) "/\" (X` "\/" Y)) "/\" ( Y` "\/" X)) by LATTICES:def 7 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ( (((X "/\" Y) "/\" X`) "\/" ((X "/\" Y) "/\" Y)) "/\" (Y` "\/" X)) by LATTICES:def 11 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ( ((Y "/\" (X "/\" X`)) "\/" ((X "/\" Y) "/\" Y)) "/\" (Y` "\/" X)) by LATTICES:def 7 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ( ((Y "/\" Bottom L) "\/" ((X "/\" Y) "/\" Y)) "/\" (Y` "\/" X)) by LATTICES:20 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" (Y "/\" Y)) "/\" (Y` "\/" X) ) by LATTICES:def 7 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" (((X "/\" Y) "/\" Y`) "\/" ((X "/\" Y ) "/\" X)) by LATTICES:def 11 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" (Y "/\" Y`)) "\/" ((X "/\" Y ) "/\" X)) by LATTICES:def 7 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Bottom L) "\/" ((X "/\" Y) "/\" X)) by LATTICES:20 .= ( (XY \ X) "\/" (XY \ Y) ) "\/" (Y "/\" (X "/\" X)) by LATTICES:def 7 .= ( (((X "/\" Y`) "/\" X`) "\/" (A "/\" X`)) "\/" (((X \ Y) "\/" (Y \ X )) "/\" Y`) ) "\/" (Y "/\" X) by LATTICES:def 11 .= ( ((Y` "/\" (X "/\" X`)) "\/" (A "/\" X`)) "\/" (((X \ Y) "\/" (Y \ X )) "/\" Y`) ) "\/" (Y "/\" X) by LATTICES:def 7 .= ( ((Y` "/\" (X "/\" X`)) "\/" (Y "/\" (X` "/\" X`))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" Y`) ) "\/" (Y "/\" X) by LATTICES:def 7 .= ( ((Y` "/\" Bottom L) "\/" (Y "/\" (X` "/\" X`))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" Y`) ) "\/" (Y "/\" X) by LATTICES:20 .= ( A "\/" (((X "/\" Y`) "/\" Y`) "\/" (A "/\" Y`)) ) "\/" (Y "/\" X) by LATTICES:def 11 .= ( A "\/" ( (X "/\" (Y` "/\" Y`)) "\/" (A "/\" Y`)) ) "\/" (Y "/\" X) by LATTICES:def 7 .= ( A "\/" ( (X "/\" Y`) "\/" (X` "/\" (Y "/\" Y`))) ) "\/" (Y "/\" X) by LATTICES:def 7 .= ( A "\/" ((X "/\" Y`) "\/" (X` "/\" Bottom L) )) "\/" (Y "/\" X) by LATTICES:20 .= A "\/" ( (X "/\" Y`) "\/" (Y "/\" X) ) by LATTICES:def 5 .= A "\/" (X "/\" (Y` "\/" Y) ) by LATTICES:def 11 .= A "\/" (X "/\" Top L) by LATTICES:21 .= (Y "\/" X) "/\" (X` "\/" X ) by LATTICES:11 .= (Y "\/" X) "/\" Top L by LATTICES:21 .= Y "\/" X; hence thesis; end; theorem (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y proof (X \+\ Y) \+\ (X "\/" Y) = ((X \+\ Y) "/\" (X` "/\" Y`)) "\/" ((X "\/" Y ) \ (X \+\ Y)) by LATTICES:24 .= ( ((X "/\" Y`) "/\" (X` "/\" Y`)) "\/" ((Y "/\" X`) "/\" (X` "/\" Y`) ) ) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 11 .= ( (X "/\" (Y` "/\" (Y` "/\" X`))) "\/" ((Y "/\" X`) "/\" (X` "/\" Y`) ) ) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7 .= ( (X "/\" ((Y` "/\" Y`) "/\" X`)) "\/" ((Y "/\" X`) "/\" (X` "/\" Y`) ) ) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7 .= ( ((X "/\" X`) "/\" Y`) "\/" ((Y "/\" X`) "/\" (X` "/\" Y`)) ) "\/" ( (X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7 .= ( (Bottom L "/\" Y`) "\/" ((Y "/\" X`) "/\" (X` "/\" Y`)) ) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:20 .= (Y "/\" (X` "/\" (X` "/\" Y`))) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7 .= (Y "/\" ((X` "/\" X`) "/\" Y`)) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7 .= ((Y "/\" Y`) "/\" X`) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7 .= (Bottom L "/\" X`) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:20 .= Y "/\" X by Lm1; hence thesis; end; theorem Th64: X \+\ Y = (X "\/" Y) \ (X "/\" Y) proof thus X \+\ Y = (X \ X "/\" Y) "\/" (Y \ X) by Th33 .= (X \ X "/\" Y) "\/" (Y \ X "/\" Y) by Th33 .= (X "\/" Y) \ (X "/\" Y) by LATTICES:def 11; end; theorem (X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z)) proof thus (X \+\ Y) \ Z = (X \ Y \ Z) "\/" (Y \ X \ Z) by LATTICES:def 11 .= (X \ (Y "\/" Z)) "\/" (Y \ X \ Z) by Th45 .= (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z)) by Th45; end; theorem X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" (X "/\" Y "/\" Z) proof X \ (Y \+\ Z) = X \ ((Y "\/" Z) \ (Y "/\" Z)) by Th64 .= (X \ (Y "\/" Z)) "\/" (X "/\" (Y "/\" Z)) by Th37 .= (X \ (Y "\/" Z)) "\/" (X "/\" Y "/\" Z) by LATTICES:def 7; hence thesis; end; theorem (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z) proof set S1 = X \ (Y "\/" Z), S2 = Y \ (X "\/" Z), S3 = Z \ (X "\/" Y), S4 = X "/\" Y "/\" Z; thus (X \+\ Y) \+\ Z = (((X \ Y) \ Z) "\/" ((Y \ X) \ Z)) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by LATTICES:def 11 .= ( S1 "\/" ((Y \ X) \ Z)) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by Th45 .= ( S1 "\/" S2) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by Th45 .= ( S1 "\/" S2) "\/" (Z \ ((X "\/" Y) \ (X "/\" Y))) by Th44 .= ( S1 "\/" S2) "\/" (S3 "\/" (X "/\" Y "/\" Z )) by Th37 .= (S1 "\/" S2 "\/" S4) "\/" S3 by LATTICES:def 5 .= (S1 "\/" S4 "\/" S2) "\/" S3 by LATTICES:def 5 .= (S1 "\/" S4) "\/" (S2 "\/" S3) by LATTICES:def 5 .= (S1 "\/" (X "/\" (Y "/\" Z))) "\/" (S2 "\/" S3) by LATTICES:def 7 .= (X \ ((Y "\/" Z) \ (Y "/\" Z))) "\/" (S2 "\/" S3) by Th37 .= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" (S2 "\/" S3) by Th44 .= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" (S2 "\/" (Z \ Y \ X)) by Th45 .= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" ((Y \ Z \ X) "\/" (Z \ Y \ X)) by Th45 .= X \+\ (Y \+\ Z) by LATTICES:def 11; end; theorem (X \+\ Y)` = (X "/\" Y) "\/" (X` "/\" Y`) proof thus (X \+\ Y)` = (X \ Y)` "/\" (Y \ X)` by LATTICES:24 .=(X` "\/" Y``) "/\" (Y "/\" X`)` by LATTICES:23 .=(X` "\/" Y``) "/\" (Y` "\/" X``) by LATTICES:23 .=(X` "\/" Y) "/\" (Y` "\/" X``) .=(X` "\/" Y) "/\" (Y` "\/" X) .=(X` "/\" (Y` "\/" X)) "\/" (Y "/\" (Y` "\/" X)) by LATTICES:def 11 .=((X` "/\" Y`) "\/" (X` "/\" X)) "\/" (Y "/\" (Y` "\/" X)) by LATTICES:def 11 .=((X` "/\" Y`) "\/" (X` "/\" X)) "\/" ((Y "/\" Y`) "\/" (Y "/\" X)) by LATTICES:def 11 .=((X` "/\" Y`) "\/" Bottom L) "\/" ((Y "/\" Y`) "\/" (Y "/\" X)) by LATTICES:20 .=(X` "/\" Y`) "\/" (Bottom L "\/" (Y "/\" X)) by LATTICES:20 .=(X "/\" Y) "\/" (X` "/\" Y`); end;