:: Propositional Calculus For Boolean Valued Functions, IV
:: by Shunichi Kobayashi
::
:: Received April 23, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users

begin

theorem :: BVFUNC_8:1

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

proof end;

theorem :: BVFUNC_8:2

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

proof end;

theorem :: BVFUNC_8:3

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

proof end;

theorem :: BVFUNC_8:4

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

proof end;

theorem :: BVFUNC_8:5

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

proof end;

theorem :: BVFUNC_8:6

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

proof end;

theorem :: BVFUNC_8:7

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

proof end;

theorem :: BVFUNC_8:8

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

proof end;

theorem :: BVFUNC_8:9

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

proof end;

theorem :: BVFUNC_8:10

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

proof end;

theorem :: BVFUNC_8:11

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

proof end;

theorem :: BVFUNC_8:12

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

proof end;

theorem :: BVFUNC_8:13

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

proof end;

theorem :: BVFUNC_8:14

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

proof end;

theorem :: BVFUNC_8:15

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds a 'xor' (O_el Y) = a

proof end;

theorem :: BVFUNC_8:16

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

proof end;

theorem :: BVFUNC_8:17

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

proof end;

theorem Th18: :: BVFUNC_8:18

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

proof end;

theorem :: BVFUNC_8:19

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

proof end;

theorem :: BVFUNC_8:20

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

proof end;

theorem :: BVFUNC_8:21

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

proof end;

theorem :: BVFUNC_8:22

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

proof end;

theorem :: BVFUNC_8:23

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

proof end;

theorem :: BVFUNC_8:24

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

proof end;

theorem :: BVFUNC_8:25

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

proof end;

theorem :: BVFUNC_8:26

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

proof end;

theorem :: BVFUNC_8:27

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

proof end;

theorem :: BVFUNC_8:28

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

proof end;

theorem :: BVFUNC_8:29

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

proof end;