:: BOOLEALG semantic presentation

definition

let L be Lattice;
let X, Y be Element of L;
func X \ Y -> Element of L equals :: BOOLEALG:def 1
X "/\" (Y ` );
correctness ;

end;

:: deftheorem defines \ BOOLEALG:def 1 :

definition

let L be Lattice;
let X, Y be Element of L;
func X \+\ Y -> Element of L equals :: BOOLEALG:def 2
(X \ Y) "\/" (Y \ X);
correctness ;

end;

:: deftheorem defines \+\ BOOLEALG:def 2 :

definition

let L be Lattice;
let X, Y be Element of L;
:: original: =
redefine pred X = Y means :Def3: :: BOOLEALG:def 3
( X [= Y & Y [= X );
compatibility by LATTICES:26;

end;

:: deftheorem Def3 defines = BOOLEALG:def 3 :

definition

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

end;

:: deftheorem Def4 defines meets BOOLEALG:def 4 :

notation

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

end;

Lm1: for L being Lattice
for X, Z, Y being Element of L st X [= Z & Y [= Z holds
X "\/" Y [= Z

proof end;

theorem :: BOOLEALG:1

canceled;

theorem :: BOOLEALG:2

canceled;

theorem :: BOOLEALG:3

for L being Lattice
for X, Y, Z being Element of L st X "\/" Y [= Z holds
( X [= Z & Y [= Z )

proof end;

theorem :: BOOLEALG:4

for L being Lattice
for X, Y, Z being Element of L holds X "/\" Y [= X "\/" Z

proof end;

theorem :: BOOLEALG:5

canceled;

theorem :: BOOLEALG:6

for L being Lattice
for X, Z, Y being Element of L st X [= Z holds
X \ Y [= Z

proof end;

theorem Th7: :: BOOLEALG:7

for L being Lattice
for X, Y, Z being Element of L st X [= Y holds
X \ Z [= Y \ Z by LATTICES:27;

theorem Th8: :: BOOLEALG:8

for L being Lattice
for X, Y being Element of L holds X \ Y [= X by LATTICES:23;

theorem :: BOOLEALG:9

for L being Lattice
for X, Y being Element of L holds X \ Y [= X \+\ Y by LATTICES:22;

theorem :: BOOLEALG:10

for L being Lattice
for X, Y, Z being Element of L st X \ Y [= Z & Y \ X [= Z holds
X \+\ Y [= Z by Lm1;

theorem :: BOOLEALG:11

for L being Lattice
for X, Y, Z being Element of L holds
( X = Y "\/" Z iff ( Y [= X & Z [= X & ( for V being Element of L st Y [= V & Z [= V holds
X [= V ) ) )

proof end;

theorem :: BOOLEALG:12

for L being Lattice
for X, Y, Z being Element of L holds
( X = Y "/\" Z iff ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) ) )

proof end;

theorem :: BOOLEALG:13

canceled;

theorem Th14: :: BOOLEALG:14

for L being Lattice
for X, Y, Z being Element of L holds X "/\" (Y \ Z) = (X "/\" Y) \ Z by LATTICES:def 7;

theorem Th15: :: BOOLEALG:15

for L being Lattice
for X, Y being Element of L st X meets Y holds
Y meets X

proof end;

theorem :: BOOLEALG:16

for L being Lattice
for X being Element of L holds
( X meets X iff X <> Bottom L )

proof end;

theorem :: BOOLEALG:17

for L being Lattice
for X, Y being Element of L holds X \+\ Y = Y \+\ X ;

definition

let L be Lattice;
let X, Y be Element of L;
:: original: meets
redefine pred X meets Y;
symmetry by Th15;
:: original: \+\
redefine func X \+\ Y -> Element of L;
commutativity ;

end;

theorem :: BOOLEALG:18

canceled;

theorem :: BOOLEALG:19

canceled;

theorem :: BOOLEALG:20

canceled;

theorem :: BOOLEALG:21

for L being M_Lattice
for X, Y being Element of L st X misses Y holds
Y misses X

proof end;

theorem :: BOOLEALG:22

for L being D_Lattice
for X, Y, Z being Element of L st (X "/\" Y) "\/" (X "/\" Z) = X holds
X [= Y "\/" Z

proof end;

theorem :: BOOLEALG:23

canceled;

theorem Th24: :: BOOLEALG:24

for L being D_Lattice
for X, Y, Z being Element of L holds (X "\/" Y) \ Z = (X \ Z) "\/" (Y \ Z) by LATTICES:def 11;

theorem Th25: :: BOOLEALG:25

for L being 0_Lattice
for X being Element of L st X [= Bottom L holds
X = Bottom L

proof end;

theorem :: BOOLEALG:26

for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y & X [= Z & Y "/\" Z = Bottom L holds
X = Bottom L

proof end;

theorem Th27: :: BOOLEALG:27

for L being 0_Lattice
for X, Y being Element of L holds
( X "\/" Y = Bottom L iff ( X = Bottom L & Y = Bottom L ) )

proof end;

theorem :: BOOLEALG:28

for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y & Y "/\" Z = Bottom L holds
X "/\" Z = Bottom L

proof end;

theorem Th29: :: BOOLEALG:29

for L being 0_Lattice
for X being Element of L holds (Bottom L) \ X = Bottom L by LATTICES:40;

theorem Th30: :: BOOLEALG:30

for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y & Y [= Z holds
X meets Z

proof end;

theorem Th31: :: BOOLEALG:31

for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y "/\" Z holds
( X meets Y & X meets Z )

proof end;

theorem :: BOOLEALG:32

for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y \ Z holds
X meets Y

proof end;

theorem :: BOOLEALG:33

for L being 0_Lattice
for X being Element of L holds X misses Bottom L

proof end;

theorem :: BOOLEALG:34

for L being 0_Lattice
for X, Z, Y being Element of L st X misses Z & Y [= Z holds
X misses Y by Th30;

theorem :: BOOLEALG:35

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

theorem :: BOOLEALG:36

for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y & X [= Z & Y misses Z holds
X = Bottom L

proof end;

theorem :: BOOLEALG:37

for L being 0_Lattice
for X, Y, Z being Element of L st X misses Y holds
( Z "/\" X misses Z "/\" Y & X "/\" Z misses Y "/\" Z )

proof end;

theorem :: BOOLEALG:38

for L being B_Lattice
for X, Y, Z being Element of L st X \ Y [= Z holds
X [= Y "\/" Z

proof end;

theorem Th39: :: BOOLEALG:39

for L being B_Lattice
for X, Y, Z being Element of L st X [= Y holds
Z \ Y [= Z \ X

proof end;

theorem :: BOOLEALG:40

for L being B_Lattice
for X, Y, Z, V being Element of L st X [= Y & Z [= V holds
X \ V [= Y \ Z

proof end;

theorem :: BOOLEALG:41

for L being B_Lattice
for X, Y, Z being Element of L st X [= Y "\/" Z holds
( X \ Y [= Z & X \ Z [= Y )

proof end;

theorem :: BOOLEALG:42

for L being B_Lattice
for X, Y being Element of L holds
( X ` [= (X "/\" Y) ` & Y ` [= (X "/\" Y) ` )

proof end;

theorem :: BOOLEALG:43

for L being B_Lattice
for X, Y being Element of L holds
( (X "\/" Y) ` [= X ` & (X "\/" Y) ` [= Y ` )

proof end;

theorem :: BOOLEALG:44

for L being B_Lattice
for X, Y being Element of L st X [= Y \ X holds
X = Bottom L

proof end;

theorem :: BOOLEALG:45

for L being B_Lattice
for X, Y being Element of L st X [= Y holds
Y = X "\/" (Y \ X)

proof end;

theorem Th46: :: BOOLEALG:46

for L being B_Lattice
for X, Y being Element of L holds
( X \ Y = Bottom L iff X [= Y )

proof end;

theorem :: BOOLEALG:47

for L being B_Lattice
for X, Y, Z being Element of L st X [= Y "\/" Z & X "/\" Z = Bottom L holds
X [= Y

proof end;

theorem :: BOOLEALG:48

for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = (X \ Y) "\/" Y

proof end;

theorem :: BOOLEALG:49

for L being B_Lattice
for X, Y being Element of L holds X \ (X "\/" Y) = Bottom L

proof end;

theorem Th50: :: BOOLEALG:50

for L being B_Lattice
for X, Y being Element of L holds
( X \ (X "/\" Y) = X \ Y & X \ (Y "/\" X) = X \ Y )

proof end;

theorem :: BOOLEALG:51

for L being B_Lattice
for X, Y being Element of L holds (X \ Y) "/\" Y = Bottom L

proof end;

theorem Th52: :: BOOLEALG:52

for L being B_Lattice
for X, Y being Element of L holds
( X "\/" (Y \ X) = X "\/" Y & (Y \ X) "\/" X = Y "\/" X )

proof end;

theorem Th53: :: BOOLEALG:53

for L being B_Lattice
for X, Y being Element of L holds (X "/\" Y) "\/" (X \ Y) = X

proof end;

theorem Th54: :: BOOLEALG:54

for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z)

proof end;

theorem :: BOOLEALG:55

for L being B_Lattice
for X, Y being Element of L holds X \ (X \ Y) = X "/\" Y

proof end;

theorem :: BOOLEALG:56

for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ Y = X \ Y

proof end;

theorem :: BOOLEALG:57

for L being B_Lattice
for X, Y being Element of L holds
( X "/\" Y = Bottom L iff X \ Y = X )

proof end;

theorem :: BOOLEALG:58

for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z)

proof end;

theorem Th59: :: BOOLEALG:59

for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z)

proof end;

theorem :: BOOLEALG:60

for L being B_Lattice
for X, Y, Z being Element of L holds
( X "/\" (Y \ Z) = (X "/\" Y) \ (X "/\" Z) & (Y \ Z) "/\" X = (Y "/\" X) \ (Z "/\" X) )

proof end;

theorem Th61: :: BOOLEALG:61

for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X)

proof end;

theorem Th62: :: BOOLEALG:62

for L being B_Lattice
for X, Y, Z being Element of L holds (X \ Y) \ Z = X \ (Y "\/" Z)

proof end;

theorem :: BOOLEALG:63

for L being B_Lattice
for X, Y being Element of L st X \ Y = Y \ X holds
X = Y

proof end;

theorem :: BOOLEALG:64

canceled;

theorem :: BOOLEALG:65

canceled;

theorem Th66: :: BOOLEALG:66

for L being B_Lattice
for X being Element of L holds X \ X = Bottom L by LATTICES:47;

theorem Th67: :: BOOLEALG:67

for L being B_Lattice
for X being Element of L holds X \ (Bottom L) = X

proof end;

theorem :: BOOLEALG:68

for L being B_Lattice
for X, Y being Element of L holds (X \ Y) ` = (X ` ) "\/" Y

proof end;

theorem Th69: :: BOOLEALG:69

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 ) )

proof end;

theorem Th70: :: BOOLEALG:70

for L being B_Lattice
for X, Y being Element of L holds X "/\" Y misses X \ Y

proof end;

theorem :: BOOLEALG:71

for L being B_Lattice
for X, Y, Z being Element of L holds
( X misses Y "\/" Z iff ( X misses Y & X misses Z ) ) by Th69;

theorem :: BOOLEALG:72

for L being B_Lattice
for X, Y being Element of L holds X \ Y misses Y

proof end;

theorem :: BOOLEALG:73

for L being B_Lattice
for X, Y being Element of L st X misses Y holds
( (X "\/" Y) \ Y = X & (X "\/" Y) \ X = Y )

proof end;

theorem :: BOOLEALG:74

for L being B_Lattice
for X, Y being Element of L st (X ` ) "\/" (Y ` ) = X "\/" Y & X misses X ` & Y misses Y ` holds
( X = Y ` & Y = X ` )

proof end;

theorem :: BOOLEALG:75

for L being B_Lattice
for X, Y being Element of L st (X ` ) "\/" (Y ` ) = X "\/" Y & Y misses X ` & X misses Y ` holds
( X = X ` & Y = Y ` )

proof end;

theorem :: BOOLEALG:76

for L being B_Lattice
for X being Element of L holds X \+\ (Bottom L) = X

proof end;

theorem :: BOOLEALG:77

for L being B_Lattice
for X being Element of L holds X \+\ X = Bottom L

proof end;

theorem :: BOOLEALG:78

for L being B_Lattice
for X, Y being Element of L holds X "/\" Y misses X \+\ Y

proof end;

theorem :: BOOLEALG:79

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

proof end;

theorem :: BOOLEALG:80

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

proof end;

theorem :: BOOLEALG:81

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

proof end;

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

proof end;

theorem :: BOOLEALG:82

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

proof end;

theorem :: BOOLEALG:83

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

proof end;

theorem Th84: :: BOOLEALG:84

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

proof end;

theorem :: BOOLEALG:85

for L being B_Lattice
for X, Y, Z being Element of L holds (X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))

proof end;

theorem :: BOOLEALG:86

for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)

proof end;

theorem :: BOOLEALG:87

for L being B_Lattice
for X, Y, Z being Element of L holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)

proof end;

theorem :: BOOLEALG:88

for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) ` = (X "/\" Y) "\/" ((X ` ) "/\" (Y ` ))

proof end;