:: BOOLEALG semantic presentation

definition

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
func c₂ \ c₃ -> Element of a₁ equals :: BOOLEALG:def 1
a₂ "/\" (a₃ ` );
correctness ;

end;

:: deftheorem Def1 defines \ BOOLEALG:def 1 :

definition

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
func c₂ \+\ c₃ -> Element of a₁ equals :: BOOLEALG:def 2
(a₂ \ a₃) "\/" (a₃ \ a₂);
correctness ;

end;

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

definition

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
redefine pred = as c₂ = c₃ means :Def3: :: BOOLEALG:def 3
( a₂ [= a₃ & a₃ [= a₂ );
compatibility by LATTICES:26;

end;

:: deftheorem Def3 defines = BOOLEALG:def 3 :

definition

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
pred c₂ meets c₃ means :Def4: :: BOOLEALG:def 4
a₂ "/\" a₃ <> Bottom a₁;

end;

:: deftheorem Def4 defines meets BOOLEALG:def 4 :

notation

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
antonym c₂ misses c₃ for c₂ meets c₃;

end;

Lemma3: for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ & b₄ [= b₃ holds
b₂ "\/" b₄ [= b₃

proof end;

theorem Th1: :: BOOLEALG:1

canceled;

theorem Th2: :: BOOLEALG:2

canceled;

theorem Th3: :: BOOLEALG:3

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ "\/" b₃ [= b₄ holds
( b₂ [= b₄ & b₃ [= b₄ )

proof end;

theorem Th4: :: BOOLEALG:4

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ holds b₂ "/\" b₃ [= b₂ "\/" b₄

proof end;

theorem Th5: :: BOOLEALG:5

canceled;

theorem Th6: :: BOOLEALG:6

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ holds
b₂ \ b₄ [= b₃

proof end;

theorem Th7: :: BOOLEALG:7

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ holds
b₂ \ b₄ [= b₃ \ b₄ by LATTICES:27;

theorem Th8: :: BOOLEALG:8

for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds b₂ \ b₃ [= b₂ by LATTICES:23;

theorem Th9: :: BOOLEALG:9

for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds b₂ \ b₃ [= b₂ \+\ b₃ by LATTICES:22;

theorem Th10: :: BOOLEALG:10

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ \ b₃ [= b₄ & b₃ \ b₂ [= b₄ holds
b₂ \+\ b₃ [= b₄ by Lemma3;

theorem Th11: :: BOOLEALG:11

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ = b₃ "\/" b₄ iff ( b₃ [= b₂ & b₄ [= b₂ & ( for b₅ being Element of b₁ st b₃ [= b₅ & b₄ [= b₅ holds
b₂ [= b₅ ) ) )

proof end;

theorem Th12: :: BOOLEALG:12

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ = b₃ "/\" b₄ iff ( b₂ [= b₃ & b₂ [= b₄ & ( for b₅ being Element of b₁ st b₅ [= b₃ & b₅ [= b₄ holds
b₅ [= b₂ ) ) )

proof end;

theorem Th13: :: BOOLEALG:13

canceled;

theorem Th14: :: BOOLEALG:14

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ holds b₂ "/\" (b₃ \ b₄) = (b₂ "/\" b₃) \ b₄ by LATTICES:def 7;

theorem Th15: :: BOOLEALG:15

for b₁ being Lattice
for b₂, b₃ being Element of b₁ st b₂ meets b₃ holds
b₃ meets b₂

proof end;

theorem Th16: :: BOOLEALG:16

for b₁ being Lattice
for b₂ being Element of b₁ holds
( b₂ meets b₂ iff b₂ <> Bottom b₁ )

proof end;

theorem Th17: :: BOOLEALG:17

for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds b₂ \+\ b₃ = b₃ \+\ b₂ ;

definition

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
redefine pred meets as c₂ meets c₃;
symmetry by Th15;
redefine func \+\ as c₂ \+\ c₃ -> Element of a₁;
commutativity ;

end;

theorem Th18: :: BOOLEALG:18

canceled;

theorem Th19: :: BOOLEALG:19

canceled;

theorem Th20: :: BOOLEALG:20

canceled;

theorem Th21: :: BOOLEALG:21

for b₁ being M_Lattice
for b₂, b₃ being Element of b₁ st b₂ misses b₃ holds
b₃ misses b₂

proof end;

theorem Th22: :: BOOLEALG:22

for b₁ being D_Lattice
for b₂, b₃, b₄ being Element of b₁ st (b₂ "/\" b₃) "\/" (b₂ "/\" b₄) = b₂ holds
b₂ [= b₃ "\/" b₄

proof end;

theorem Th23: :: BOOLEALG:23

canceled;

theorem Th24: :: BOOLEALG:24

for b₁ being D_Lattice
for b₂, b₃, b₄ being Element of b₁ holds (b₂ "\/" b₃) \ b₄ = (b₂ \ b₄) "\/" (b₃ \ b₄) by LATTICES:def 11;

theorem Th25: :: BOOLEALG:25

for b₁ being 0_Lattice
for b₂ being Element of b₁ st b₂ [= Bottom b₁ holds
b₂ = Bottom b₁

proof end;

theorem Th26: :: BOOLEALG:26

for b₁ being 0_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ & b₂ [= b₄ & b₃ "/\" b₄ = Bottom b₁ holds
b₂ = Bottom b₁

proof end;

theorem Th27: :: BOOLEALG:27

for b₁ being 0_Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ "\/" b₃ = Bottom b₁ iff ( b₂ = Bottom b₁ & b₃ = Bottom b₁ ) )

proof end;

theorem Th28: :: BOOLEALG:28

for b₁ being 0_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ & b₃ "/\" b₄ = Bottom b₁ holds
b₂ "/\" b₄ = Bottom b₁

proof end;

theorem Th29: :: BOOLEALG:29

for b₁ being 0_Lattice
for b₂ being Element of b₁ holds (Bottom b₁) \ b₂ = Bottom b₁ by LATTICES:40;

theorem Th30: :: BOOLEALG:30

for b₁ being 0_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ meets b₃ & b₃ [= b₄ holds
b₂ meets b₄

proof end;

theorem Th31: :: BOOLEALG:31

for b₁ being 0_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ meets b₃ "/\" b₄ holds
( b₂ meets b₃ & b₂ meets b₄ )

proof end;

theorem Th32: :: BOOLEALG:32

for b₁ being 0_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ meets b₃ \ b₄ holds
b₂ meets b₃

proof end;

theorem Th33: :: BOOLEALG:33

for b₁ being 0_Lattice
for b₂ being Element of b₁ holds b₂ misses Bottom b₁

proof end;

theorem Th34: :: BOOLEALG:34

for b₁ being 0_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ misses b₃ & b₄ [= b₃ holds
b₂ misses b₄ by Th30;

theorem Th35: :: BOOLEALG:35

for b₁ being 0_Lattice
for b₂, b₃, b₄ being Element of b₁ st ( b₂ misses b₃ or b₂ misses b₄ ) holds
b₂ misses b₃ "/\" b₄ by Th31;

theorem Th36: :: BOOLEALG:36

for b₁ being 0_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ & b₂ [= b₄ & b₃ misses b₄ holds
b₂ = Bottom b₁

proof end;

theorem Th37: :: BOOLEALG:37

for b₁ being 0_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ misses b₃ holds
( b₄ "/\" b₂ misses b₄ "/\" b₃ & b₂ "/\" b₄ misses b₃ "/\" b₄ )

proof end;

theorem Th38: :: BOOLEALG:38

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ \ b₃ [= b₄ holds
b₂ [= b₃ "\/" b₄

proof end;

theorem Th39: :: BOOLEALG:39

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ holds
b₄ \ b₃ [= b₄ \ b₂

proof end;

theorem Th40: :: BOOLEALG:40

for b₁ being B_Lattice
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ [= b₃ & b₄ [= b₅ holds
b₂ \ b₅ [= b₃ \ b₄

proof end;

theorem Th41: :: BOOLEALG:41

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ "\/" b₄ holds
( b₂ \ b₃ [= b₄ & b₂ \ b₄ [= b₃ )

proof end;

theorem Th42: :: BOOLEALG:42

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ ` [= (b₂ "/\" b₃) ` & b₃ ` [= (b₂ "/\" b₃) ` )

proof end;

theorem Th43: :: BOOLEALG:43

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds
( (b₂ "\/" b₃) ` [= b₂ ` & (b₂ "\/" b₃) ` [= b₃ ` )

proof end;

theorem Th44: :: BOOLEALG:44

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ st b₂ [= b₃ \ b₂ holds
b₂ = Bottom b₁

proof end;

theorem Th45: :: BOOLEALG:45

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ st b₂ [= b₃ holds
b₃ = b₂ "\/" (b₃ \ b₂)

proof end;

theorem Th46: :: BOOLEALG:46

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ \ b₃ = Bottom b₁ iff b₂ [= b₃ )

proof end;

theorem Th47: :: BOOLEALG:47

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ "\/" b₄ & b₂ "/\" b₄ = Bottom b₁ holds
b₂ [= b₃

proof end;

theorem Th48: :: BOOLEALG:48

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ "\/" b₃ = (b₂ \ b₃) "\/" b₃

proof end;

theorem Th49: :: BOOLEALG:49

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ \ (b₂ "\/" b₃) = Bottom b₁

proof end;

theorem Th50: :: BOOLEALG:50

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ \ (b₂ "/\" b₃) = b₂ \ b₃ & b₂ \ (b₃ "/\" b₂) = b₂ \ b₃ )

proof end;

theorem Th51: :: BOOLEALG:51

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ \ b₃) "/\" b₃ = Bottom b₁

proof end;

theorem Th52: :: BOOLEALG:52

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ "\/" (b₃ \ b₂) = b₂ "\/" b₃ & (b₃ \ b₂) "\/" b₂ = b₃ "\/" b₂ )

proof end;

theorem Th53: :: BOOLEALG:53

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ "/\" b₃) "\/" (b₂ \ b₃) = b₂

proof end;

theorem Th54: :: BOOLEALG:54

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ holds b₂ \ (b₃ \ b₄) = (b₂ \ b₃) "\/" (b₂ "/\" b₄)

proof end;

theorem Th55: :: BOOLEALG:55

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ \ (b₂ \ b₃) = b₂ "/\" b₃

proof end;

theorem Th56: :: BOOLEALG:56

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ "\/" b₃) \ b₃ = b₂ \ b₃

proof end;

theorem Th57: :: BOOLEALG:57

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ "/\" b₃ = Bottom b₁ iff b₂ \ b₃ = b₂ )

proof end;

theorem Th58: :: BOOLEALG:58

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ holds b₂ \ (b₃ "\/" b₄) = (b₂ \ b₃) "/\" (b₂ \ b₄)

proof end;

theorem Th59: :: BOOLEALG:59

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ holds b₂ \ (b₃ "/\" b₄) = (b₂ \ b₃) "\/" (b₂ \ b₄)

proof end;

theorem Th60: :: BOOLEALG:60

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ "/\" (b₃ \ b₄) = (b₂ "/\" b₃) \ (b₂ "/\" b₄) & (b₃ \ b₄) "/\" b₂ = (b₃ "/\" b₂) \ (b₄ "/\" b₂) )

proof end;

theorem Th61: :: BOOLEALG:61

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ "\/" b₃) \ (b₂ "/\" b₃) = (b₂ \ b₃) "\/" (b₃ \ b₂)

proof end;

theorem Th62: :: BOOLEALG:62

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ holds (b₂ \ b₃) \ b₄ = b₂ \ (b₃ "\/" b₄)

proof end;

theorem Th63: :: BOOLEALG:63

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ st b₂ \ b₃ = b₃ \ b₂ holds
b₂ = b₃

proof end;

theorem Th64: :: BOOLEALG:64

canceled;

theorem Th65: :: BOOLEALG:65

canceled;

theorem Th66: :: BOOLEALG:66

for b₁ being B_Lattice
for b₂ being Element of b₁ holds b₂ \ b₂ = Bottom b₁ by LATTICES:47;

theorem Th67: :: BOOLEALG:67

for b₁ being B_Lattice
for b₂ being Element of b₁ holds b₂ \ (Bottom b₁) = b₂

proof end;

theorem Th68: :: BOOLEALG:68

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ \ b₃) ` = (b₂ ` ) "\/" b₃

proof end;

theorem Th69: :: BOOLEALG:69

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ meets b₃ "\/" b₄ iff ( b₂ meets b₃ or b₂ meets b₄ ) )

proof end;

theorem Th70: :: BOOLEALG:70

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ "/\" b₃ misses b₂ \ b₃

proof end;

theorem Th71: :: BOOLEALG:71

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ misses b₃ "\/" b₄ iff ( b₂ misses b₃ & b₂ misses b₄ ) ) by Th69;

theorem Th72: :: BOOLEALG:72

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ \ b₃ misses b₃

proof end;

theorem Th73: :: BOOLEALG:73

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ st b₂ misses b₃ holds
( (b₂ "\/" b₃) \ b₃ = b₂ & (b₂ "\/" b₃) \ b₂ = b₃ )

proof end;

theorem Th74: :: BOOLEALG:74

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ st (b₂ ` ) "\/" (b₃ ` ) = b₂ "\/" b₃ & b₂ misses b₂ ` & b₃ misses b₃ ` holds
( b₂ = b₃ ` & b₃ = b₂ ` )

proof end;

theorem Th75: :: BOOLEALG:75

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ st (b₂ ` ) "\/" (b₃ ` ) = b₂ "\/" b₃ & b₃ misses b₂ ` & b₂ misses b₃ ` holds
( b₂ = b₂ ` & b₃ = b₃ ` )

proof end;

theorem Th76: :: BOOLEALG:76

for b₁ being B_Lattice
for b₂ being Element of b₁ holds b₂ \+\ (Bottom b₁) = b₂

proof end;

theorem Th77: :: BOOLEALG:77

for b₁ being B_Lattice
for b₂ being Element of b₁ holds b₂ \+\ b₂ = Bottom b₁

proof end;

theorem Th78: :: BOOLEALG:78

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ "/\" b₃ misses b₂ \+\ b₃

proof end;

theorem Th79: :: BOOLEALG:79

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ "\/" b₃ = b₂ \+\ (b₃ \ b₂)

proof end;

theorem Th80: :: BOOLEALG:80

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ \+\ (b₂ "/\" b₃) = b₂ \ b₃

proof end;

theorem Th81: :: BOOLEALG:81

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ "\/" b₃ = (b₂ \+\ b₃) "\/" (b₂ "/\" b₃)

proof end;

Lemma27: for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ "\/" b₃) \ (b₂ \+\ b₃) = b₂ "/\" b₃

proof end;

theorem Th82: :: BOOLEALG:82

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ \+\ b₃) \+\ (b₂ "/\" b₃) = b₂ "\/" b₃

proof end;

theorem Th83: :: BOOLEALG:83

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ \+\ b₃) \+\ (b₂ "\/" b₃) = b₂ "/\" b₃

proof end;

theorem Th84: :: BOOLEALG:84

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ \+\ b₃ = (b₂ "\/" b₃) \ (b₂ "/\" b₃)

proof end;

theorem Th85: :: BOOLEALG:85

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ holds (b₂ \+\ b₃) \ b₄ = (b₂ \ (b₃ "\/" b₄)) "\/" (b₃ \ (b₂ "\/" b₄))

proof end;

theorem Th86: :: BOOLEALG:86

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ holds b₂ \ (b₃ \+\ b₄) = (b₂ \ (b₃ "\/" b₄)) "\/" ((b₂ "/\" b₃) "/\" b₄)

proof end;

theorem Th87: :: BOOLEALG:87

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ holds (b₂ \+\ b₃) \+\ b₄ = b₂ \+\ (b₃ \+\ b₄)

proof end;

theorem Th88: :: BOOLEALG:88

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ \+\ b₃) ` = (b₂ "/\" b₃) "\/" ((b₂ ` ) "/\" (b₃ ` ))

proof end;