:: BVFUNC_8 semantic presentation

theorem Th1: :: BVFUNC_8:1

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

proof end;

theorem Th2: :: BVFUNC_8:2

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

proof end;

theorem Th3: :: BVFUNC_8:3

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

proof end;

theorem Th4: :: BVFUNC_8:4

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

proof end;

theorem Th5: :: BVFUNC_8:5

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

proof end;

theorem Th6: :: BVFUNC_8:6

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

proof end;

theorem Th7: :: BVFUNC_8:7

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

proof end;

theorem Th8: :: BVFUNC_8:8

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

proof end;

theorem Th9: :: BVFUNC_8:9

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

proof end;

theorem Th10: :: BVFUNC_8:10

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

proof end;

theorem Th11: :: BVFUNC_8:11

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

proof end;

theorem Th12: :: BVFUNC_8:12

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

proof end;

theorem Th13: :: BVFUNC_8:13

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

proof end;

theorem Th14: :: BVFUNC_8:14

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

proof end;

theorem Th15: :: BVFUNC_8:15

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

proof end;

theorem Th16: :: BVFUNC_8:16

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

proof end;

theorem Th17: :: BVFUNC_8:17

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

proof end;

theorem Th18: :: BVFUNC_8:18

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

proof end;

theorem Th19: :: BVFUNC_8:19

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

proof end;

theorem Th20: :: BVFUNC_8:20

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

proof end;

theorem Th21: :: BVFUNC_8:21

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

proof end;

theorem Th22: :: BVFUNC_8:22

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

proof end;

theorem Th23: :: BVFUNC_8:23

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

proof end;

theorem Th24: :: BVFUNC_8:24

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

proof end;

theorem Th25: :: BVFUNC_8:25

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

proof end;

theorem Th26: :: BVFUNC_8:26

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

proof end;

theorem Th27: :: BVFUNC_8:27

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 Th28: :: BVFUNC_8:28

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

proof end;

theorem Th29: :: BVFUNC_8: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₂ 'imp' b₄)) = I_el b₁

proof end;