The abstract of the Mizar article:

Propositional Calculus for Boolean Valued Functions. Part IV

by

Shunichi Kobayashi

Received April 23, 1999

MML identifier: BVFUNC_8

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, BVFUNC_1, ZF_LANG, FUNCT_1, RELAT_1, BINARITH,
      PARTIT1;
 notation TARSKI, XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, RELAT_1, FUNCT_1,
      FRAENKEL, BINARITH, BVFUNC_1;
 constructors BINARITH, BVFUNC_1;
 clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL;
 requirements SUBSET, BOOLE;


begin

::Chap. 1  Propositional Calculus

reserve Y for non empty set;

theorem :: BVFUNC_8:1
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);

theorem :: BVFUNC_8:2
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);

theorem :: BVFUNC_8:3
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);

theorem :: BVFUNC_8:4
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);

theorem :: BVFUNC_8:5
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);

theorem :: BVFUNC_8:6
for a,b being Element of Funcs(Y,BOOLEAN) holds
a = (a '&' b) 'or' (a '&' 'not' b);

theorem :: BVFUNC_8:7
for a,b being Element of Funcs(Y,BOOLEAN) holds
a = (a 'or' b) '&' (a 'or' 'not' b);

theorem :: BVFUNC_8:8
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);

theorem :: BVFUNC_8:9
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);

theorem :: BVFUNC_8:10
for a,b being Element of Funcs(Y,BOOLEAN) holds
a '&' b = a '&' ('not' a 'or' b);

theorem :: BVFUNC_8:11
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'or' b = a 'or' ('not' a '&' b);

theorem :: BVFUNC_8:12
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'xor' b = 'not'( a 'eqv' b);

theorem :: BVFUNC_8:13
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'xor' b = (a 'or' b) '&' ('not' a 'or' 'not' b);

theorem :: BVFUNC_8:14
for a being Element of Funcs(Y,BOOLEAN) holds
a 'xor' I_el(Y) = 'not' a;

theorem :: BVFUNC_8:15
for a being Element of Funcs(Y,BOOLEAN) holds
a 'xor' O_el(Y) = a;

theorem :: BVFUNC_8:16
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'xor' b = 'not' a 'xor' 'not' b;

theorem :: BVFUNC_8:17
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not'( a 'xor' b) = a 'xor' 'not' b;

theorem :: BVFUNC_8:18
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'eqv' b = (a 'or' 'not' b) '&' ('not' a 'or' b);

theorem :: BVFUNC_8:19
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'eqv' b = (a '&' b) 'or' ('not' a '&' 'not' b);

theorem :: BVFUNC_8:20
for a being Element of Funcs(Y,BOOLEAN) holds
a 'eqv' I_el(Y) = a;

theorem :: BVFUNC_8:21
for a being Element of Funcs(Y,BOOLEAN) holds
a 'eqv' O_el(Y) = 'not' a;

theorem :: BVFUNC_8:22
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not'( a 'eqv' b) = (a 'eqv' 'not' b);

theorem :: BVFUNC_8:23
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not' a '<' (a 'imp' b) 'eqv' 'not' a;

theorem :: BVFUNC_8:24
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not' a '<' (b 'imp' a) 'eqv' 'not' b;

theorem :: BVFUNC_8:25
for a,b being Element of Funcs(Y,BOOLEAN) holds
a '<' (a 'or' b) 'eqv' (b 'or' a) 'eqv' a;

theorem :: BVFUNC_8:26
for a being Element of Funcs(Y,BOOLEAN) holds
a 'imp' ('not' a 'eqv' 'not' a) = I_el(Y);

theorem :: BVFUNC_8:27
for a,b being Element of Funcs(Y,BOOLEAN) holds
((a 'imp' b) 'imp' a) 'imp' a = I_el(Y);

theorem :: BVFUNC_8:28
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);

theorem :: BVFUNC_8:29
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);