:: BVFUNC25 semantic presentation

theorem Th1: :: BVFUNC25:1

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

proof end;

theorem Th2: :: BVFUNC25:2

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 Th3: :: BVFUNC25:3

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

proof end;

theorem Th4: :: BVFUNC25:4

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

proof end;

theorem Th5: :: BVFUNC25:5

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

proof end;

theorem Th6: :: BVFUNC25:6

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

proof end;

theorem Th7: :: BVFUNC25:7

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

proof end;

theorem Th8: :: BVFUNC25:8

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

proof end;

theorem Th9: :: BVFUNC25:9

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

proof end;

theorem Th10: :: BVFUNC25:10

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

proof end;

theorem Th11: :: BVFUNC25:11

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

proof end;

theorem Th12: :: BVFUNC25:12

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

proof end;

theorem Th13: :: BVFUNC25:13

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

proof end;

theorem Th14: :: BVFUNC25:14

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

proof end;

theorem Th15: :: BVFUNC25:15

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

proof end;

theorem Th16: :: BVFUNC25:16

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

proof end;

theorem Th17: :: BVFUNC25:17

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

proof end;

theorem Th18: :: BVFUNC25:18

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

proof end;

theorem Th19: :: BVFUNC25:19

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

proof end;

theorem Th20: :: BVFUNC25:20

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

proof end;

theorem Th21: :: BVFUNC25:21

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

proof end;

theorem Th22: :: BVFUNC25:22

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

proof end;

theorem Th23: :: BVFUNC25:23

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

proof end;

theorem Th24: :: BVFUNC25:24

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

proof end;

theorem Th25: :: BVFUNC25:25

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

proof end;

theorem Th26: :: BVFUNC25:26

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

proof end;

theorem Th27: :: BVFUNC25:27

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

proof end;

theorem Th28: :: BVFUNC25:28

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

proof end;

theorem Th29: :: BVFUNC25:29

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 Th30: :: BVFUNC25:30

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

proof end;

theorem Th31: :: BVFUNC25:31

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

proof end;

theorem Th32: :: BVFUNC25:32

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

proof end;

theorem Th33: :: BVFUNC25:33

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 Th34: :: BVFUNC25:34

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

proof end;

theorem Th35: :: BVFUNC25:35

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

proof end;

theorem Th36: :: BVFUNC25:36

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

proof end;

theorem Th37: :: BVFUNC25:37

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

proof end;

theorem Th38: :: BVFUNC25:38

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

proof end;

theorem Th39: :: BVFUNC25:39

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 Th40: :: BVFUNC25:40

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

proof end;

theorem Th41: :: BVFUNC25:41

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

proof end;

theorem Th42: :: BVFUNC25:42

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

proof end;

theorem Th43: :: BVFUNC25:43

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

proof end;

theorem Th44: :: BVFUNC25:44

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

proof end;

theorem Th45: :: BVFUNC25:45

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

proof end;

theorem Th46: :: BVFUNC25:46

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

proof end;

theorem Th47: :: BVFUNC25:47

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

proof end;