Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Propositional Calculus for Boolean Valued Functions. Part VII

by
Shunichi Kobayashi

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));

```