:: BVFUNC_5 semantic presentation

theorem :: BVFUNC_5:1

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds
( ( a = I_el Y & b = I_el Y ) iff a '&' b = I_el Y )

proof end;

theorem :: BVFUNC_5:2

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN st a = I_el Y & a 'imp' b = I_el Y holds
b = I_el Y

proof end;

theorem :: BVFUNC_5:3

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN st a = I_el Y holds
a 'or' b = I_el Y

proof end;

theorem :: BVFUNC_5:4

canceled;

theorem :: BVFUNC_5:5

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN st b = I_el Y holds
a 'imp' b = I_el Y

proof end;

theorem :: BVFUNC_5:6

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN st 'not' a = I_el Y holds
a 'imp' b = I_el Y

proof end;

theorem :: BVFUNC_5:7

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds 'not' (a '&' ('not' a)) = I_el Y

proof end;

theorem :: BVFUNC_5:8

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a 'imp' a = I_el Y

proof end;

theorem :: BVFUNC_5:9

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

proof end;

theorem :: BVFUNC_5:10

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN st a 'imp' b = I_el Y & b 'imp' c = I_el Y holds
a 'imp' c = I_el Y

proof end;

theorem :: BVFUNC_5:11

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

proof end;

theorem :: BVFUNC_5:12

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds (('not' a) 'imp' a) 'imp' a = I_el Y

proof end;

theorem :: BVFUNC_5:13

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c))) = I_el Y

proof end;

theorem :: BVFUNC_5:14

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c)) = I_el Y

proof end;

theorem :: BVFUNC_5:15

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN st a 'imp' b = I_el Y holds
(b 'imp' c) 'imp' (a 'imp' c) = I_el Y

proof end;

theorem :: BVFUNC_5:16

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds b 'imp' (a 'imp' b) = I_el Y

proof end;

theorem :: BVFUNC_5:17

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds ((a 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y

proof end;

theorem :: BVFUNC_5:18

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds b 'imp' ((b 'imp' a) 'imp' a) = I_el Y

proof end;

theorem :: BVFUNC_5:19

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a)) = I_el Y

proof end;

theorem :: BVFUNC_5:20

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c)) = I_el Y

proof end;

theorem :: BVFUNC_5:21

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (b 'imp' (b 'imp' c)) 'imp' (b 'imp' c) = I_el Y

proof end;

theorem :: BVFUNC_5:22

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c)) = I_el Y

proof end;

theorem :: BVFUNC_5:23

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN st a = I_el Y holds
(a 'imp' b) 'imp' b = I_el Y

proof end;

theorem :: BVFUNC_5:24

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN st c 'imp' (b 'imp' a) = I_el Y holds
b 'imp' (c 'imp' a) = I_el Y

proof end;

theorem :: BVFUNC_5:25

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN st c 'imp' (b 'imp' a) = I_el Y & b = I_el Y holds
c 'imp' a = I_el Y

proof end;

theorem :: BVFUNC_5:26

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN st c 'imp' (b 'imp' a) = I_el Y & b = I_el Y & c = I_el Y holds
a = I_el Y

proof end;

theorem :: BVFUNC_5:27

for Y being non empty set
for b, c being Element of Funcs Y,BOOLEAN st b 'imp' (b 'imp' c) = I_el Y holds
b 'imp' c = I_el Y

proof end;

theorem :: BVFUNC_5:28

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y holds
(a 'imp' b) 'imp' (a 'imp' c) = I_el Y

proof end;

theorem :: BVFUNC_5:29

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y & a 'imp' b = I_el Y holds
a 'imp' c = I_el Y

proof end;

theorem :: BVFUNC_5:30

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y & a 'imp' b = I_el Y & a = I_el Y holds
c = I_el Y

proof end;

theorem :: BVFUNC_5:31

for Y being non empty set
for a, b, c, d being Element of Funcs Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y & a 'imp' (c 'imp' d) = I_el Y holds
a 'imp' (b 'imp' d) = I_el Y

proof end;

theorem :: BVFUNC_5:32

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

proof end;

theorem :: BVFUNC_5:33

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

proof end;

theorem :: BVFUNC_5:34

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

proof end;

theorem :: BVFUNC_5:35

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

proof end;

theorem :: BVFUNC_5:36

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds (a 'imp' ('not' a)) 'imp' ('not' a) = I_el Y

proof end;

theorem :: BVFUNC_5:37

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

proof end;

theorem :: BVFUNC_5:38

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds 'not' ((a '&' b) '&' c) = (('not' a) 'or' ('not' b)) 'or' ('not' c)

proof end;

theorem :: BVFUNC_5:39

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds 'not' ((a 'or' b) 'or' c) = (('not' a) '&' ('not' b)) '&' ('not' c)

proof end;

theorem :: BVFUNC_5:40

for Y being non empty set
for a, b, c, d being Element of Funcs Y,BOOLEAN holds a 'or' ((b '&' c) '&' d) = ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d)

proof end;

theorem :: BVFUNC_5:41

for Y being non empty set
for a, b, c, d being Element of Funcs Y,BOOLEAN holds a '&' ((b 'or' c) 'or' d) = ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d)

proof end;