:: BVFUNC10 semantic presentation

theorem Th1: :: BVFUNC10:1

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ '&' b₃) 'or' (b₃ '&' b₄)) 'or' (b₄ '&' b₂) = ((b₂ 'or' b₃) '&' (b₃ 'or' b₄)) '&' (b₄ 'or' b₂)

proof end;

Lemma1: for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ '&' ('not' b₃)) 'or' (b₃ '&' ('not' b₄))) 'or' (b₄ '&' ('not' b₂)) '<' ((b₃ '&' ('not' b₂)) 'or' (b₄ '&' ('not' b₃))) 'or' (b₂ '&' ('not' b₄))

proof end;

theorem Th2: :: BVFUNC10:2

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ '&' ('not' b₃)) 'or' (b₃ '&' ('not' b₄))) 'or' (b₄ '&' ('not' b₂)) = ((b₃ '&' ('not' b₂)) 'or' (b₄ '&' ('not' b₃))) 'or' (b₂ '&' ('not' b₄))

proof end;

Lemma2: for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'or' ('not' b₃)) '&' (b₃ 'or' ('not' b₄))) '&' (b₄ 'or' ('not' b₂)) '<' ((b₃ 'or' ('not' b₂)) '&' (b₄ 'or' ('not' b₃))) '&' (b₂ 'or' ('not' b₄))

proof end;

theorem Th3: :: BVFUNC10:3

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'or' ('not' b₃)) '&' (b₃ 'or' ('not' b₄))) '&' (b₄ 'or' ('not' b₂)) = ((b₃ 'or' ('not' b₂)) '&' (b₄ 'or' ('not' b₃))) '&' (b₂ 'or' ('not' b₄))

proof end;

theorem Th4: :: BVFUNC10:4

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN st b₄ 'imp' b₂ = I_el b₁ & b₄ 'imp' b₃ = I_el b₁ holds
b₄ 'imp' (b₂ 'or' b₃) = I_el b₁

proof end;

theorem Th5: :: BVFUNC10:5

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN st b₂ 'imp' b₄ = I_el b₁ & b₃ 'imp' b₄ = I_el b₁ holds
(b₂ '&' b₃) 'imp' b₄ = I_el b₁

proof end;

theorem Th6: :: BVFUNC10:6

for b₁ being non empty set
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of Funcs b₁,BOOLEAN holds (((b₂ 'imp' b₃) '&' (b₄ 'imp' b₅)) '&' (b₆ 'imp' b₇)) '&' ((b₂ 'or' b₄) 'or' b₆) '<' (b₃ 'or' b₅) 'or' b₇

proof end;

Lemma3: for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of Funcs b₁,BOOLEAN holds (((b₂ 'imp' b₄) '&' (b₃ 'imp' b₅)) '&' (b₂ 'or' b₃)) '&' ('not' (b₄ '&' b₅)) '<' (((b₄ 'imp' b₂) '&' (b₅ 'imp' b₃)) '&' (b₄ 'or' b₅)) '&' ('not' (b₂ '&' b₃))

proof end;

theorem Th7: :: BVFUNC10:7

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of Funcs b₁,BOOLEAN holds (((b₂ 'imp' b₄) '&' (b₃ 'imp' b₅)) '&' (b₂ 'or' b₃)) '&' ('not' (b₄ '&' b₅)) = (((b₄ 'imp' b₂) '&' (b₅ 'imp' b₃)) '&' (b₄ 'or' b₅)) '&' ('not' (b₂ '&' b₃))

proof end;

theorem Th8: :: BVFUNC10:8

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of Funcs b₁,BOOLEAN holds (b₂ 'or' b₃) '&' (b₄ 'or' b₅) = (((b₂ '&' b₄) 'or' (b₂ '&' b₅)) 'or' (b₃ '&' b₄)) 'or' (b₃ '&' b₅)

proof end;

theorem Th9: :: BVFUNC10:9

for b₁ being non empty set
for b₂, b₃, b₄, b₅, b₆ being Element of Funcs b₁,BOOLEAN holds (b₂ '&' b₃) 'or' ((b₄ '&' b₅) '&' b₆) = (((((b₂ 'or' b₄) '&' (b₂ 'or' b₅)) '&' (b₂ 'or' b₆)) '&' (b₃ 'or' b₄)) '&' (b₃ 'or' b₅)) '&' (b₃ 'or' b₆)

proof end;

theorem Th10: :: BVFUNC10:10

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'imp' b₃) '&' (b₃ 'imp' b₄)) '&' (b₄ 'imp' b₅) = ((b₂ 'imp' ((b₃ '&' b₄) '&' b₅)) '&' (b₃ 'imp' (b₄ '&' b₅))) '&' (b₄ 'imp' b₅)

proof end;

theorem Th11: :: BVFUNC10:11

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'imp' b₄) '&' (b₃ 'imp' b₅)) '&' (b₂ 'or' b₃) '<' b₄ 'or' b₅

proof end;

theorem Th12: :: BVFUNC10:12

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (((b₂ '&' b₃) 'imp' ('not' b₄)) '&' b₂) '&' b₄ '<' 'not' b₃

proof end;

theorem Th13: :: BVFUNC10:13

for b₁ being non empty set
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of Funcs b₁,BOOLEAN holds ((b₂ '&' b₃) '&' b₄) 'imp' ((b₅ 'or' b₆) 'or' b₇) = ((('not' b₅) '&' ('not' b₆)) '&' b₄) 'imp' ((('not' b₂) 'or' ('not' b₃)) 'or' b₇)

proof end;

theorem Th14: :: BVFUNC10:14

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds ((b₂ 'imp' b₃) '&' (b₃ 'imp' b₄)) '&' (b₄ 'imp' b₂) = ((b₂ '&' b₃) '&' b₄) 'or' ((('not' b₂) '&' ('not' b₃)) '&' ('not' b₄))

proof end;

theorem Th15: :: BVFUNC10:15

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (((b₂ 'imp' b₃) '&' (b₃ 'imp' b₄)) '&' (b₄ 'imp' b₂)) '&' ((b₂ 'or' b₃) 'or' b₄) = (b₂ '&' b₃) '&' b₄

proof end;

Lemma4: for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (((('not' b₂) '&' b₃) '&' b₄) 'or' ((b₂ '&' ('not' b₃)) '&' b₄)) 'or' ((b₂ '&' b₃) '&' ('not' b₄)) '<' (b₂ 'or' b₃) '&' ('not' ((b₂ '&' b₃) '&' b₄))

proof end;

theorem Th16: :: BVFUNC10:16

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (((b₂ 'or' b₃) '&' (b₃ 'or' b₄)) '&' (b₄ 'or' b₂)) '&' ('not' ((b₂ '&' b₃) '&' b₄)) = (((('not' b₂) '&' b₃) '&' b₄) 'or' ((b₂ '&' ('not' b₃)) '&' b₄)) 'or' ((b₂ '&' b₃) '&' ('not' b₄))

proof end;

theorem Th17: :: BVFUNC10:17

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' b₂ 'imp' (b₃ '&' b₄)

proof end;

theorem Th18: :: BVFUNC10:18

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' (b₂ 'or' b₃) 'imp' b₄

proof end;

theorem Th19: :: BVFUNC10:19

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' b₂ 'imp' (b₃ 'or' b₄)

proof end;

theorem Th20: :: BVFUNC10:20

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' b₂ 'imp' (b₃ 'or' ('not' b₄))

proof end;

theorem Th21: :: BVFUNC10:21

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' b₃ 'imp' (b₄ 'or' b₂)

proof end;

theorem Th22: :: BVFUNC10:22

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' b₃ 'imp' (b₄ 'or' ('not' b₂))

proof end;

theorem Th23: :: BVFUNC10:23

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' (b₂ 'imp' b₃) '&' (b₃ 'imp' (b₄ 'or' b₂))

proof end;

theorem Th24: :: BVFUNC10:24

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' (b₂ 'imp' (b₃ 'or' ('not' b₄))) '&' (b₃ 'imp' b₄)

proof end;

theorem Th25: :: BVFUNC10:25

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' (b₂ 'imp' (b₃ 'or' b₄)) '&' (b₃ 'imp' (b₄ 'or' b₂))

proof end;

theorem Th26: :: BVFUNC10:26

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' (b₂ 'imp' (b₃ 'or' ('not' b₄))) '&' (b₃ 'imp' (b₄ 'or' b₂))

proof end;

theorem Th27: :: BVFUNC10:27

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'imp' b₃) '&' (b₃ 'imp' b₄) '<' (b₂ 'imp' (b₃ 'or' ('not' b₄))) '&' (b₃ 'imp' (b₄ 'or' ('not' b₂)))

proof end;