:: Propositional Calculus for Boolean Valued Functions, II
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users

begin

theorem :: BVFUNC_6:1

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

proof end;

theorem :: BVFUNC_6:2

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

proof end;

theorem :: BVFUNC_6:3

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

proof end;

theorem :: BVFUNC_6:4

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

proof end;

theorem :: BVFUNC_6:5

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

proof end;

theorem :: BVFUNC_6:6

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

proof end;

theorem :: BVFUNC_6:7

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

proof end;

theorem :: BVFUNC_6:8

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

proof end;

theorem :: BVFUNC_6:9

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

proof end;

theorem :: BVFUNC_6:10

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

proof end;

theorem :: BVFUNC_6:11

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

proof end;

theorem :: BVFUNC_6:12

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

proof end;

theorem :: BVFUNC_6:13

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

proof end;

theorem :: BVFUNC_6:14

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

proof end;

theorem :: BVFUNC_6:15

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

proof end;

theorem :: BVFUNC_6:16

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

proof end;

theorem :: BVFUNC_6:17

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

proof end;

theorem :: BVFUNC_6:18

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

proof end;

theorem :: BVFUNC_6:19

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

proof end;

theorem :: BVFUNC_6:20

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

proof end;

theorem :: BVFUNC_6:21

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

proof end;

theorem :: BVFUNC_6:22

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

proof end;

theorem :: BVFUNC_6:23

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

proof end;

theorem :: BVFUNC_6:24

canceled;

theorem :: BVFUNC_6:25

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

proof end;

theorem :: BVFUNC_6:26

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

proof end;

theorem :: BVFUNC_6:27

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

proof end;

theorem :: BVFUNC_6:28

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

proof end;

theorem Th29: :: BVFUNC_6:29

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

proof end;

theorem :: BVFUNC_6:30

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

proof end;

theorem :: BVFUNC_6:31

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

proof end;

theorem :: BVFUNC_6:32

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

proof end;

theorem :: BVFUNC_6:33

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

proof end;

theorem :: BVFUNC_6:34

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

proof end;

theorem :: BVFUNC_6:35

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

proof end;

theorem :: BVFUNC_6:36

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

proof end;

theorem Th37: :: BVFUNC_6:37

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

proof end;

theorem :: BVFUNC_6:38

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

proof end;

theorem :: BVFUNC_6:39

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

proof end;

theorem :: BVFUNC_6:40

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

proof end;

theorem :: BVFUNC_6:41

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

proof end;

theorem :: BVFUNC_6:42

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

proof end;

theorem Th43: :: BVFUNC_6:43

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

proof end;

theorem :: BVFUNC_6:44

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

theorem :: BVFUNC_6:45

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

proof end;

theorem :: BVFUNC_6:46

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

proof end;

theorem :: BVFUNC_6:47

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

proof end;