The abstract of the Mizar article:

Propositional Calculus for Boolean Valued Functions. Part VI

by

Shunichi Kobayashi

Received July 14, 1999

MML identifier: BVFUNC10

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, ZF_LANG, BVFUNC_1, PARTIT1;
 notation XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, FRAENKEL, BINARITH, BVFUNC_1;
 constructors BINARITH, BVFUNC_1;
 clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL;


begin

::Chap. 1  Propositional Calculus

reserve Y for non empty set;

theorem :: BVFUNC10:1
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'or' (b '&' c) 'or' (c '&' a)=
(a 'or' b) '&' (b 'or' c) '&' (c 'or' a);

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

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

theorem :: BVFUNC10:4
  for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(c 'imp' a)=I_el(Y) & (c 'imp' b)=I_el(Y) implies
c 'imp' (a 'or' b)=I_el(Y);

theorem :: BVFUNC10:5
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' c)=I_el(Y) & (b 'imp' c)=I_el(Y) implies
(a '&' b) 'imp' c = I_el(Y);

theorem :: BVFUNC10:6
for a1,a2,b1,b2,c1,c2 being Element of Funcs(Y,BOOLEAN) holds
(a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1)
'<'
(a2 'or' b2 'or' c2);

theorem :: BVFUNC10:7
for a1,a2,b1,b2 being Element of Funcs(Y,BOOLEAN) holds
(a1 'imp' b1) '&' (a2 'imp' b2) '&' (a1 'or' a2) '&' 'not'( b1 '&' b2)=
(b1 'imp' a1) '&' (b2 'imp' a2) '&' (b1 'or' b2) '&' 'not'( a1 '&' a2);

theorem :: BVFUNC10:8
for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
(a 'or' b) '&' (c 'or' d) =
(a '&' c) 'or' (a '&' d) 'or' (b '&' c) 'or' (b '&' d);

theorem :: BVFUNC10:9
for a1,a2,b1,b2,b3 being Element of Funcs(Y,BOOLEAN) holds
(a1 '&' a2) 'or' (b1 '&' b2 '&' b3)=
(a1 'or' b1) '&' (a1 'or' b2) '&' (a1 'or' b3) '&'
(a2 'or' b1) '&' (a2 'or' b2) '&' (a2 'or' b3);

theorem :: BVFUNC10:10
for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' d)=
(a 'imp' (b '&' c '&' d)) '&' (b 'imp' (c '&' d)) '&' (c 'imp' d);

theorem :: BVFUNC10:11
for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' c) '&' (b 'imp' d) '&' (a 'or' b) '<' (c 'or' d);

theorem :: BVFUNC10:12
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a '&' b) 'imp' 'not' c) '&' a '&' c '<' 'not' b;

theorem :: BVFUNC10:13
for a1,a2,a3,b1,b2,b3 being Element of Funcs(Y,BOOLEAN) holds
(a1 '&' a2 '&' a3) 'imp' (b1 'or' b2 'or' b3)=
('not' b1 '&' 'not' b2 '&' a3) 'imp' ('not' a1 'or' 'not' a2 'or' b3);

theorem :: BVFUNC10:14
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) =
(a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' 'not' c);

theorem :: BVFUNC10:15
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) '&' (a 'or' b 'or' c)=
(a '&' b '&' c);

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

theorem :: BVFUNC10:17
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b '&' c));

theorem :: BVFUNC10:18
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' ((a 'or' b) 'imp' c);

theorem :: BVFUNC10:19
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' c));

theorem :: BVFUNC10:20
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' 'not' c));

theorem :: BVFUNC10:21
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (b 'imp' (c 'or' a));

theorem :: BVFUNC10:22
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (b 'imp' (c 'or' 'not' a));

theorem :: BVFUNC10:23
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' b) '&' (b 'imp' (c 'or' a));

theorem :: BVFUNC10:24
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' 'not' c)) '&' (b 'imp' c);

theorem :: BVFUNC10:25
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' c)) '&' (b 'imp' (c 'or' a));

theorem :: BVFUNC10:26
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' 'not'
c)) '&' (b 'imp' (c 'or' a));

theorem :: BVFUNC10:27
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<'
(a 'imp' (b 'or' 'not' c)) '&' (b 'imp' (c 'or' 'not' a));