The abstract of the Mizar article:

Propositional Calculus for Boolean Valued Functions. Part VII

by

Shunichi Kobayashi

Received February 6, 2003

MML identifier: BVFUNC25

[ Mizar article, MML identifier index ]

environ

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


begin

 reserve Y for non empty set,
         a,b,c,d for Element of Funcs(Y,BOOLEAN);

theorem :: BVFUNC25:1
  'not' (a 'imp' b) = a '&' 'not' b;

theorem :: BVFUNC25:2
('not' b 'imp' 'not' a) 'imp' (a 'imp' b)=I_el(Y);

theorem :: BVFUNC25:3
a 'imp' b = 'not' b 'imp' 'not' a;

theorem :: BVFUNC25:4
  a 'eqv' b = 'not' a 'eqv' 'not' b;

theorem :: BVFUNC25:5
a 'imp' b = a 'imp' (a '&' b);

theorem :: BVFUNC25:6
  a 'eqv' b = (a 'or' b) 'imp' (a '&' b);

theorem :: BVFUNC25:7
  a 'eqv' 'not' a = O_el(Y);

theorem :: BVFUNC25:8
  a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c);

theorem :: BVFUNC25:9
  a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c);

theorem :: BVFUNC25:10
  a 'eqv' b = a 'xor' 'not' b;

theorem :: BVFUNC25:11
  a '&' (b 'xor' c) = a '&' b 'xor' a '&' c;

theorem :: BVFUNC25:12
  a 'eqv' b = 'not' (a 'xor' b);

theorem :: BVFUNC25:13
  a 'xor' a = O_el(Y);

theorem :: BVFUNC25:14
  a 'xor' 'not' a = I_el(Y);

theorem :: BVFUNC25:15
  (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a;

theorem :: BVFUNC25:16
(a 'or' b) '&' ('not' a 'or' 'not' b) = ('not' a '&' b) 'or' (a '&' 'not' b);

theorem :: BVFUNC25:17
(a '&' b) 'or' ('not' a '&' 'not' b) = ('not' a 'or' b) '&' (a 'or' 'not' b);

theorem :: BVFUNC25:18
  a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c;

theorem :: BVFUNC25:19
  a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c;

theorem :: BVFUNC25:20
  'not' 'not' a 'imp' a = I_el(Y);

theorem :: BVFUNC25:21
  ((a 'imp' b) '&' a) 'imp' b = I_el(Y);

theorem :: BVFUNC25:22
a 'imp' ('not' a 'imp' a) = I_el(Y);

theorem :: BVFUNC25:23
  ('not' a 'imp' a) 'eqv' a = I_el(Y);

theorem :: BVFUNC25:24
  a 'or' (a 'imp' b) = I_el(Y);

theorem :: BVFUNC25:25
  (a 'imp' b) 'or' (c 'imp' a) = I_el(Y);

theorem :: BVFUNC25:26
  (a 'imp' b) 'or' ('not' a 'imp' b) = I_el(Y);

theorem :: BVFUNC25:27
  (a 'imp' b) 'or' (a 'imp' 'not' b) = I_el(Y);

theorem :: BVFUNC25:28
  'not' a 'imp' ('not' b 'eqv' (b 'imp' a)) = I_el(Y);

theorem :: BVFUNC25:29
  (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el(Y);

theorem :: BVFUNC25:30
  a 'imp' b = a 'eqv' (a '&' b);

theorem :: BVFUNC25:31
  a 'imp' b=I_el(Y) & b 'imp' a=I_el(Y) iff a=b;

theorem :: BVFUNC25:32
  a = 'not' a 'imp' a;

theorem :: BVFUNC25:33
a 'imp' ((a 'imp' b) 'imp' a) = I_el(Y);

theorem :: BVFUNC25:34
  a = (a 'imp' b) 'imp' a;

theorem :: BVFUNC25:35
  a = (b 'imp' a) '&' ('not' b 'imp' a);

theorem :: BVFUNC25:36
  a '&' b = 'not' (a 'imp' 'not' b);

theorem :: BVFUNC25:37
  a 'or' b = 'not' a 'imp' b;

theorem :: BVFUNC25:38
  a 'or' b = (a 'imp' b) 'imp' b;

theorem :: BVFUNC25:39
  (a 'imp' b) 'imp' (a 'imp' a) = I_el(Y);

theorem :: BVFUNC25:40
  (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el(
Y
);

theorem :: BVFUNC25:41
  (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el(Y);

theorem :: BVFUNC25:42
  (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el(Y);

theorem :: BVFUNC25:43
  ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el(Y);

theorem :: BVFUNC25:44
  (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el(Y);

theorem :: BVFUNC25:45
  (a 'imp' b) '&' (a '&' c) 'imp' (b '&' c) = I_el(Y);

theorem :: BVFUNC25:46
  a '&' (a 'imp' b) '&' (b 'imp' c) '<' c;

theorem :: BVFUNC25:47
  (a 'or' b) '&' (a 'imp' c) '&' (b 'imp' c) '<' ('not' a 'imp' (b 'or' c));