:: 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;