:: BVFUNC_9 semantic presentation

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th1: :: BVFUNC_9:1

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

proof end;

theorem Th2: :: BVFUNC_9:2

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

proof end;

theorem Th3: :: BVFUNC_9:3

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

proof end;

theorem Th4: :: BVFUNC_9:4

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

proof end;

theorem Th5: :: BVFUNC_9:5

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

proof end;

theorem Th6: :: BVFUNC_9:6

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

proof end;

theorem Th7: :: BVFUNC_9:7

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

proof end;

theorem Th8: :: BVFUNC_9:8

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

proof end;

theorem Th9: :: BVFUNC_9:9

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

proof end;

theorem Th10: :: BVFUNC_9:10

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

proof end;

theorem Th11: :: BVFUNC_9:11

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

proof end;

theorem Th12: :: BVFUNC_9:12

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

proof end;

theorem Th13: :: BVFUNC_9:13

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

proof end;

theorem Th14: :: BVFUNC_9:14

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

proof end;

theorem Th15: :: BVFUNC_9:15

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

proof end;

theorem Th16: :: BVFUNC_9:16

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

proof end;

theorem Th17: :: BVFUNC_9:17

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

proof end;

theorem Th18: :: BVFUNC_9:18

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

proof end;

theorem Th19: :: BVFUNC_9:19

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₂ '&' b₄) 'imp' (b₃ '&' b₅)

proof end;

theorem Th20: :: BVFUNC_9: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₃ '&' b₄)

proof end;

theorem Th21: :: BVFUNC_9: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₂ 'or' b₄) 'imp' b₃

proof end;

theorem Th22: :: BVFUNC_9:22

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₄) 'imp' (b₃ 'or' b₅)

proof end;

theorem Th23: :: BVFUNC_9: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₃ 'or' b₄)

proof end;

theorem Th24: :: BVFUNC_9:24

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₂ 'or' b₃) 'or' b₄)) '&' ('not' (b₅ '&' b₆))) '&' ('not' (b₅ '&' b₇)) '<' b₅ 'imp' b₂

proof end;

Lemma14: 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₄)) '&' ('not' (b₅ '&' b₆))) '&' ('not' (b₅ '&' b₇))) '&' ('not' (b₆ '&' b₇))) 'imp' (((((b₂ 'imp' b₅) '&' (b₃ 'imp' b₆)) '&' ((b₂ 'or' b₃) 'or' b₄)) '&' ('not' (b₇ '&' b₅))) '&' ('not' (b₇ '&' b₆))) = I_el b₁

proof end;

Lemma15: 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₄)) '&' ('not' (b₅ '&' b₆))) '&' ('not' (b₅ '&' b₇))) '&' ('not' (b₆ '&' b₇))) 'imp' (((((b₂ 'imp' b₅) '&' (b₄ 'imp' b₇)) '&' ((b₂ 'or' b₃) 'or' b₄)) '&' ('not' (b₆ '&' b₅))) '&' ('not' (b₆ '&' b₇))) = I_el b₁

proof end;

Lemma16: 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₄)) '&' ('not' (b₅ '&' b₆))) '&' ('not' (b₅ '&' b₇))) '&' ('not' (b₆ '&' b₇))) 'imp' (((((b₃ 'imp' b₆) '&' (b₄ 'imp' b₇)) '&' ((b₂ 'or' b₃) 'or' b₄)) '&' ('not' (b₅ '&' b₆))) '&' ('not' (b₅ '&' b₇))) = I_el b₁

proof end;

theorem Th25: :: BVFUNC_9:25

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₄)) '&' ('not' (b₅ '&' b₆))) '&' ('not' (b₅ '&' b₇))) '&' ('not' (b₆ '&' b₇)) '<' ((b₅ 'imp' b₂) '&' (b₆ 'imp' b₃)) '&' (b₇ 'imp' b₄)

proof end;

theorem Th26: :: BVFUNC_9:26

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

proof end;

theorem Th27: :: BVFUNC_9:27

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₇)) '&' ('not' (b₅ '&' b₆))) '&' ('not' (b₅ '&' b₇))) '&' ('not' (b₆ '&' b₇)) '<' (('not' (b₂ '&' b₃)) '&' ('not' (b₂ '&' b₄))) '&' ('not' (b₃ '&' b₄))

proof end;

theorem Th28: :: BVFUNC_9:28

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ '&' b₃ '<' b₂ by Lemma1;

theorem Th29: :: BVFUNC_9:29

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

theorem Th30: :: BVFUNC_9:30

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

theorem Th31: :: BVFUNC_9:31

for b₁ being non empty set
for b₂, b₃, b₄, b₅, b₆ being Element of Funcs b₁,BOOLEAN holds
( (((b₂ '&' b₃) '&' b₄) '&' b₅) '&' b₆ '<' b₂ & (((b₂ '&' b₃) '&' b₄) '&' b₅) '&' b₆ '<' b₃ ) by Lemma4;

theorem Th32: :: BVFUNC_9:32

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

theorem Th33: :: BVFUNC_9:33

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

theorem Th34: :: BVFUNC_9:34

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

proof end;

theorem Th35: :: BVFUNC_9:35

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

proof end;

theorem Th36: :: BVFUNC_9:36

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₄) '<' b₃

proof end;

theorem Th37: :: BVFUNC_9:37

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

proof end;

theorem Th38: :: BVFUNC_9:38

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

proof end;

theorem Th39: :: BVFUNC_9:39

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ '<' b₂ 'or' b₃

proof end;

theorem Th40: :: BVFUNC_9:40

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

proof end;