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


begin

theorem :: BVFUNC_8:1
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds a 'imp' ((b '&' c) '&' d) = ((a 'imp' b) '&' (a 'imp' c)) '&' (a 'imp' d)
proofend;

theorem :: BVFUNC_8:2
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds a 'imp' ((b 'or' c) 'or' d) = ((a 'imp' b) 'or' (a 'imp' c)) 'or' (a 'imp' d)
proofend;

theorem :: BVFUNC_8:3
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a '&' b) '&' c) 'imp' d = ((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)
proofend;

theorem :: BVFUNC_8:4
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a 'or' b) 'or' c) 'imp' d = ((a 'imp' d) '&' (b 'imp' d)) '&' (c 'imp' d)
proofend;

theorem :: BVFUNC_8:5
for Y being non empty set
for a, b, c being Function of 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)
proofend;

theorem :: BVFUNC_8:6
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a '&' b) 'or' (a '&' ('not' b))
proofend;

theorem :: BVFUNC_8:7
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a 'or' b) '&' (a 'or' ('not' b))
proofend;

theorem :: BVFUNC_8:8
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a = ((((a '&' b) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))
proofend;

theorem :: BVFUNC_8:9
for Y being non empty set
for a, b, c being Function of 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))
proofend;

theorem :: BVFUNC_8:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b = a '&' (('not' a) 'or' b)
proofend;

theorem :: BVFUNC_8:11
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' b = a 'or' (('not' a) '&' b)
proofend;

theorem :: BVFUNC_8:12
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = 'not' (a 'eqv' b)
proofend;

theorem :: BVFUNC_8:13
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = (a 'or' b) '&' (('not' a) 'or' ('not' b))
proofend;

theorem :: BVFUNC_8:14
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' (I_el Y) = 'not' a
proofend;

theorem :: BVFUNC_8:15
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' (O_el Y) = a
proofend;

theorem :: BVFUNC_8:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = ('not' a) 'xor' ('not' b)
proofend;

theorem :: BVFUNC_8:17
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'xor' b) = a 'xor' ('not' b)
proofend;

theorem Th18: :: BVFUNC_8:18
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' ('not' b)) '&' (('not' a) 'or' b)
proofend;

theorem :: BVFUNC_8:19
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a '&' b) 'or' (('not' a) '&' ('not' b))
proofend;

theorem :: BVFUNC_8:20
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' (I_el Y) = a
proofend;

theorem :: BVFUNC_8:21
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' (O_el Y) = 'not' a
proofend;

theorem :: BVFUNC_8:22
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'eqv' b) = a 'eqv' ('not' b)
proofend;

theorem :: BVFUNC_8:23
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' a '<' (a 'imp' b) 'eqv' ('not' a)
proofend;

theorem :: BVFUNC_8:24
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' a '<' (b 'imp' a) 'eqv' ('not' b)
proofend;

theorem :: BVFUNC_8:25
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' ((a 'or' b) 'eqv' (b 'or' a)) 'eqv' a
proofend;

theorem :: BVFUNC_8:26
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'eqv' ('not' a)) = I_el Y
proofend;

theorem :: BVFUNC_8:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' a) 'imp' a = I_el Y
proofend;

theorem :: BVFUNC_8:28
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (((a 'imp' c) '&amp;' (b 'imp' d)) '&amp;' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b)) = I_el Y
proofend;

theorem :: BVFUNC_8:29
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) = I_el Y
proofend;