:: Boolean Properties of Lattices
:: by Agnieszka Julia Marasik
::
:: Received March 28, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

definition
let L be Lattice;
let X, Y be Element of L;
funcX \ Y ->  Element of L equals :: BOOLEALG:def 1
X "/\" (Y `);
coherence
 X "/\" (Y `) is Element of L ;
end;

:: deftheorem  defines \ BOOLEALG:def_1_:_
 for L being Lattice
for X, Y being Element of L holds X \ Y = X "/\" (Y `);

definition
let L be Lattice;
let X, Y be Element of L;
funcX \+\ Y ->  Element of L equals :: BOOLEALG:def 2
(X \ Y) "\/" (Y \ X);
coherence
 (X \ Y) "\/" (Y \ X) is Element of L ;
end;

:: deftheorem  defines \+\ BOOLEALG:def_2_:_
 for L being Lattice
for X, Y being Element of L holds X \+\ Y = (X \ Y) "\/" (Y \ X);

definition
let L be Lattice;
let X, Y be Element of L;
:: original:=
redefine predX = Y means :Def3: :: BOOLEALG:def 3
( X [= Y & Y [= X );
compatibility
 ( X = Y iff ( X [= Y & Y [= X ) ) by LATTICES:8;
end;

:: deftheorem Def3 defines = BOOLEALG:def_3_:_
 for L being Lattice
for X, Y being Element of L holds
( X = Y iff ( X [= Y & Y [= X ) );

definition
let L be Lattice;
let X, Y be Element of L;
predX meets Y means :Def4: :: BOOLEALG:def 4
X "/\" Y <> Bottom L;
end;

:: deftheorem Def4 defines meets BOOLEALG:def_4_:_
 for L being Lattice
for X, Y being Element of L holds
( X meets Y iff X "/\" Y <> Bottom L );

notation
let L be Lattice;
let X, Y be Element of L;
antonym X misses Y for X meets Y;
end;

theorem :: BOOLEALG:1
for L being Lattice
for X, Y, Z being Element of L st X "\/" Y [= Z holds
X [= Z
proofend;

theorem :: BOOLEALG:2
for L being Lattice
for X, Y, Z being Element of L holds X "/\" Y [= X "\/" Z
proofend;

theorem :: BOOLEALG:3
for L being Lattice
for X, Z, Y being Element of L st X [= Z holds
X \ Y [= Z
proofend;

theorem :: BOOLEALG:4
for L being Lattice
for X, Y, Z being Element of L st X \ Y [= Z &amp; Y \ X [= Z holds
X \+\ Y [= Z by FILTER_0:6;

theorem :: BOOLEALG:5
for L being Lattice
for X, Y, Z being Element of L holds
( X = Y "\/" Z iff ( Y [= X &amp; Z [= X &amp; ( for V being Element of L st Y [= V &amp; Z [= V holds
X [= V ) ) )
proofend;

theorem :: BOOLEALG:6
for L being Lattice
for X, Y, Z being Element of L holds
( X = Y "/\" Z iff ( X [= Y &amp; X [= Z &amp; ( for V being Element of L st V [= Y &amp; V [= Z holds
V [= X ) ) )
proofend;

Lm1:  for L being Lattice
for X, Y being Element of L st X meets Y holds
Y meets X
proofend;

theorem :: BOOLEALG:7
for L being Lattice
for X being Element of L holds
( X meets X iff X <> Bottom L )
proofend;

definition
let L be Lattice;
let X, Y be Element of L;
:: original:meets
redefine predX meets Y;
symmetry
 for X, Y being Element of L st (L,b1,b2) holds
(L,b2,b1) by Lm1;
:: original:\+\
redefine funcX \+\ Y ->  Element of L;
commutativity
 for X, Y being Element of L holds X \+\ Y = Y \+\ X ;
:: original:meets
redefine predX misses Y;
symmetry
 for X, Y being Element of L st (L,b1,b2) holds
not (L,b2,b1) by Lm1;
end;

begin

begin

theorem :: BOOLEALG:8
for L being D_Lattice
for X, Y, Z being Element of L st (X "/\" Y) "\/" (X "/\" Z) = X holds
X [= Y "\/" Z
proofend;

begin

theorem Th9: :: BOOLEALG:9
for L being 0_Lattice
for X being Element of L st X [= Bottom L holds
X = Bottom L
proofend;

theorem :: BOOLEALG:10
for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y &amp; X [= Z &amp; Y "/\" Z = Bottom L holds
X = Bottom L by Th9, FILTER_0:7;

theorem Th11: :: BOOLEALG:11
for L being 0_Lattice
for X, Y being Element of L holds
( X "\/" Y = Bottom L iff ( X = Bottom L &amp; Y = Bottom L ) )
proofend;

theorem :: BOOLEALG:12
for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y &amp; Y "/\" Z = Bottom L holds
X "/\" Z = Bottom L by LATTICES:9, Th9;

theorem Th13: :: BOOLEALG:13
for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y &amp; Y [= Z holds
X meets Z
proofend;

theorem Th14: :: BOOLEALG:14
for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y "/\" Z holds
( X meets Y &amp; X meets Z )
proofend;

theorem :: BOOLEALG:15
for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y \ Z holds
X meets Y
proofend;

theorem :: BOOLEALG:16
for L being 0_Lattice
for X being Element of L holds X misses Bottom L
proofend;

theorem :: BOOLEALG:17
for L being 0_Lattice
for X, Z, Y being Element of L st X misses Z &amp; Y [= Z holds
X misses Y by Th13;

theorem :: BOOLEALG:18
for L being 0_Lattice
for X, Y, Z being Element of L st ( X misses Y or X misses Z ) holds
X misses Y "/\" Z by Th14;

theorem :: BOOLEALG:19
for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y &amp; X [= Z &amp; Y misses Z holds
X = Bottom L
proofend;

theorem :: BOOLEALG:20
for L being 0_Lattice
for X, Y, Z being Element of L st X misses Y holds
Z "/\" X misses Z "/\" Y
proofend;

begin

theorem :: BOOLEALG:21
for L being B_Lattice
for X, Y, Z being Element of L st X \ Y [= Z holds
X [= Y "\/" Z
proofend;

theorem Th22: :: BOOLEALG:22
for L being B_Lattice
for X, Y, Z being Element of L st X [= Y holds
Z \ Y [= Z \ X
proofend;

theorem :: BOOLEALG:23
for L being B_Lattice
for X, Y, Z, V being Element of L st X [= Y &amp; Z [= V holds
X \ V [= Y \ Z
proofend;

theorem :: BOOLEALG:24
for L being B_Lattice
for X, Y, Z being Element of L st X [= Y "\/" Z holds
X \ Y [= Z
proofend;

theorem :: BOOLEALG:25
for L being B_Lattice
for X, Y being Element of L holds X ` [= (X "/\" Y) `
proofend;

theorem :: BOOLEALG:26
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) ` [= X `
proofend;

theorem :: BOOLEALG:27
for L being B_Lattice
for X, Y being Element of L st X [= Y \ X holds
X = Bottom L
proofend;

theorem :: BOOLEALG:28
for L being B_Lattice
for X, Y being Element of L st X [= Y holds
Y = X "\/" (Y \ X)
proofend;

theorem Th29: :: BOOLEALG:29
for L being B_Lattice
for X, Y being Element of L holds
( X \ Y = Bottom L iff X [= Y )
proofend;

theorem :: BOOLEALG:30
for L being B_Lattice
for X, Y, Z being Element of L st X [= Y "\/" Z &amp; X "/\" Z = Bottom L holds
X [= Y
proofend;

theorem :: BOOLEALG:31
for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = (X \ Y) "\/" Y
proofend;

theorem :: BOOLEALG:32
for L being B_Lattice
for X, Y being Element of L holds X \ (X "\/" Y) = Bottom L by Th29, LATTICES:5;

theorem Th33: :: BOOLEALG:33
for L being B_Lattice
for X, Y being Element of L holds X \ (X "/\" Y) = X \ Y
proofend;

theorem :: BOOLEALG:34
for L being B_Lattice
for X, Y being Element of L holds (X \ Y) "/\" Y = Bottom L
proofend;

theorem Th35: :: BOOLEALG:35
for L being B_Lattice
for X, Y being Element of L holds X "\/" (Y \ X) = X "\/" Y
proofend;

theorem Th36: :: BOOLEALG:36
for L being B_Lattice
for X, Y being Element of L holds (X "/\" Y) "\/" (X \ Y) = X
proofend;

theorem Th37: :: BOOLEALG:37
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z)
proofend;

theorem :: BOOLEALG:38
for L being B_Lattice
for X, Y being Element of L holds X \ (X \ Y) = X "/\" Y
proofend;

theorem :: BOOLEALG:39
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ Y = X \ Y
proofend;

theorem :: BOOLEALG:40
for L being B_Lattice
for X, Y being Element of L holds
( X "/\" Y = Bottom L iff X \ Y = X )
proofend;

theorem :: BOOLEALG:41
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z)
proofend;

theorem Th42: :: BOOLEALG:42
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z)
proofend;

theorem :: BOOLEALG:43
for L being B_Lattice
for X, Y, Z being Element of L holds X "/\" (Y \ Z) = (X "/\" Y) \ (X "/\" Z)
proofend;

theorem Th44: :: BOOLEALG:44
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X)
proofend;

theorem Th45: :: BOOLEALG:45
for L being B_Lattice
for X, Y, Z being Element of L holds (X \ Y) \ Z = X \ (Y "\/" Z)
proofend;

theorem :: BOOLEALG:46
for L being B_Lattice
for X, Y being Element of L st X \ Y = Y \ X holds
X = Y
proofend;

theorem Th47: :: BOOLEALG:47
for L being B_Lattice
for X being Element of L holds X \ (Bottom L) = X
proofend;

theorem :: BOOLEALG:48
for L being B_Lattice
for X, Y being Element of L holds (X \ Y) ` = (X `) "\/" Y
proofend;

theorem Th49: :: BOOLEALG:49
for L being B_Lattice
for X, Y, Z being Element of L holds
( X meets Y "\/" Z iff ( X meets Y or X meets Z ) )
proofend;

theorem Th50: :: BOOLEALG:50
for L being B_Lattice
for X, Y being Element of L holds X "/\" Y misses X \ Y
proofend;

theorem :: BOOLEALG:51
for L being B_Lattice
for X, Y, Z being Element of L holds
( X misses Y "\/" Z iff ( X misses Y &amp; X misses Z ) ) by Th49;

theorem :: BOOLEALG:52
for L being B_Lattice
for X, Y being Element of L holds X \ Y misses Y
proofend;

theorem :: BOOLEALG:53
for L being B_Lattice
for X, Y being Element of L st X misses Y holds
(X "\/" Y) \ Y = X
proofend;

theorem :: BOOLEALG:54
for L being B_Lattice
for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y &amp; X misses X ` &amp; Y misses Y ` holds
( X = Y ` &amp; Y = X ` )
proofend;

theorem :: BOOLEALG:55
for L being B_Lattice
for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y &amp; Y misses X ` &amp; X misses Y ` holds
( X = X ` &amp; Y = Y ` )
proofend;

theorem :: BOOLEALG:56
for L being B_Lattice
for X being Element of L holds X \+\ (Bottom L) = X
proofend;

theorem :: BOOLEALG:57
for L being B_Lattice
for X being Element of L holds X \+\ X = Bottom L by LATTICES:20;

theorem :: BOOLEALG:58
for L being B_Lattice
for X, Y being Element of L holds X "/\" Y misses X \+\ Y
proofend;

theorem :: BOOLEALG:59
for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = X \+\ (Y \ X)
proofend;

theorem :: BOOLEALG:60
for L being B_Lattice
for X, Y being Element of L holds X \+\ (X "/\" Y) = X \ Y
proofend;

theorem :: BOOLEALG:61
for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = (X \+\ Y) "\/" (X "/\" Y)
proofend;

Lm2:  for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ (X \+\ Y) = X "/\" Y
proofend;

theorem :: BOOLEALG:62
for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y
proofend;

theorem :: BOOLEALG:63
for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y
proofend;

theorem Th64: :: BOOLEALG:64
for L being B_Lattice
for X, Y being Element of L holds X \+\ Y = (X "\/" Y) \ (X "/\" Y)
proofend;

theorem :: BOOLEALG:65
for L being B_Lattice
for X, Y, Z being Element of L holds (X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))
proofend;

theorem :: BOOLEALG:66
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)
proofend;

theorem :: BOOLEALG:67
for L being B_Lattice
for X, Y, Z being Element of L holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proofend;

theorem :: BOOLEALG:68
for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) ` = (X "/\" Y) "\/" ((X `) "/\" (Y `))
proofend;