:: BVFUNC_5 semantic presentation

theorem Th1: :: BVFUNC_5:1

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

proof end;

theorem Th2: :: BVFUNC_5:2

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

proof end;

theorem Th3: :: BVFUNC_5:3

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

proof end;

theorem Th4: :: BVFUNC_5:4

canceled;

theorem Th5: :: BVFUNC_5:5

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

proof end;

theorem Th6: :: BVFUNC_5:6

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

proof end;

theorem Th7: :: BVFUNC_5:7

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

proof end;

theorem Th8: :: BVFUNC_5:8

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds b₂ 'imp' b₂ = I_el b₁

proof end;

theorem Th9: :: BVFUNC_5:9

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

proof end;

theorem Th10: :: BVFUNC_5:10

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₄ = I_el b₁

proof end;

theorem Th11: :: BVFUNC_5:11

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

proof end;

theorem Th12: :: BVFUNC_5:12

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

proof end;

theorem Th13: :: BVFUNC_5:13

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

proof end;

theorem Th14: :: BVFUNC_5:14

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

proof end;

theorem Th15: :: BVFUNC_5:15

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

proof end;

theorem Th16: :: BVFUNC_5:16

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

proof end;

theorem Th17: :: BVFUNC_5:17

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

proof end;

theorem Th18: :: BVFUNC_5:18

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

proof end;

theorem Th19: :: BVFUNC_5:19

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

proof end;

theorem Th20: :: BVFUNC_5:20

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

proof end;

theorem Th21: :: BVFUNC_5:21

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

proof end;

theorem Th22: :: BVFUNC_5:22

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

proof end;

theorem Th23: :: BVFUNC_5:23

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

proof end;

theorem Th24: :: BVFUNC_5:24

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

proof end;

theorem Th25: :: BVFUNC_5:25

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

proof end;

theorem Th26: :: BVFUNC_5:26

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

proof end;

theorem Th27: :: BVFUNC_5:27

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

proof end;

theorem Th28: :: BVFUNC_5:28

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

proof end;

theorem Th29: :: BVFUNC_5:29

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

proof end;

theorem Th30: :: BVFUNC_5:30

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

proof end;

theorem Th31: :: BVFUNC_5:31

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

proof end;

theorem Th32: :: BVFUNC_5:32

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

proof end;

theorem Th33: :: BVFUNC_5:33

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

proof end;

theorem Th34: :: BVFUNC_5:34

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

proof end;

theorem Th35: :: BVFUNC_5:35

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

proof end;

theorem Th36: :: BVFUNC_5:36

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

proof end;

theorem Th37: :: BVFUNC_5:37

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

proof end;

theorem Th38: :: BVFUNC_5:38

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

proof end;

theorem Th39: :: BVFUNC_5:39

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

proof end;

theorem Th40: :: BVFUNC_5:40

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

proof end;

theorem Th41: :: BVFUNC_5:41

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

proof end;