Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

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

by
Shunichi Kobayashi

MML identifier: BVFUNC_9
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_2, MARGREL1, ZF_LANG, PARTIT1, BVFUNC_1;
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,
a,b,c,d,e,f,g for Element of Funcs(Y,BOOLEAN);

theorem :: BVFUNC_9:1
(a 'or' b) '&' (b 'imp' c) '<' a 'or' c;

theorem :: BVFUNC_9:2
a '&' (a 'imp' b) '<' b;

theorem :: BVFUNC_9:3
(a 'imp' b) '&' 'not' b '<' 'not' a;

theorem :: BVFUNC_9:4
(a 'or' b) '&' 'not' a '<' b;

theorem :: BVFUNC_9:5
(a 'imp' b) '&' ('not' a 'imp' b) '<' b;

theorem :: BVFUNC_9:6
(a 'imp' b) '&' (a 'imp' 'not' b) '<' 'not' a;

theorem :: BVFUNC_9:7
a 'imp' (b '&' c) '<' a 'imp' b;

theorem :: BVFUNC_9:8
(a 'or' b) 'imp' c '<' a 'imp' c;

theorem :: BVFUNC_9:9
a 'imp' b '<' (a '&' c) 'imp' b;

theorem :: BVFUNC_9:10
a 'imp' b '<' (a '&' c) 'imp' (b '&' c);

theorem :: BVFUNC_9:11
a 'imp' b '<' a 'imp' (b 'or' c);

theorem :: BVFUNC_9:12
a 'imp' b '<' (a 'or' c) 'imp' (b 'or' c);

theorem :: BVFUNC_9:13
a '&' b 'or' c '<' a 'or' c;

theorem :: BVFUNC_9:14
(a '&' b) 'or' (c '&' d) '<' a 'or' c;

theorem :: BVFUNC_9:15
(a 'or' b) '&' (b 'imp' c) '<' a 'or' c;

theorem :: BVFUNC_9:16
(a 'imp' b) '&' ('not' a 'imp' c) '<' b 'or' c;

theorem :: BVFUNC_9:17
(a 'imp' c) '&' (b 'imp' 'not' c) '<' 'not' a 'or' 'not' b;

theorem :: BVFUNC_9:18
(a 'or' b) '&' ('not' a 'or' c) '<' b 'or' c;

theorem :: BVFUNC_9:19
(a 'imp' b) '&' (c 'imp' d) '<' (a '&' c) 'imp' (b '&' d);

theorem :: BVFUNC_9:20
(a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b '&' c);

theorem :: BVFUNC_9:21
((a 'imp' c) '&' (b 'imp' c)) '<' (a 'or' b) 'imp' c;

theorem :: BVFUNC_9:22
(a 'imp' b) '&' (c 'imp' d) '<' (a 'or' c) 'imp' (b 'or' d);

theorem :: BVFUNC_9:23
(a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b 'or' c);

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

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

theorem :: BVFUNC_9:26
for a1,b1,a2,b2 being Element of Funcs(Y,BOOLEAN) holds
((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'(a2 '&' b2))
'imp' 'not' (a1 '&' b1)=I_el(Y);

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

theorem :: BVFUNC_9:28
a '&' b '<' a;

theorem :: BVFUNC_9:29
a '&' b '&' c '<' a &
a '&' b '&' c '<' b;

theorem :: BVFUNC_9:30
a '&' b '&' c '&' d '<' a &
a '&' b '&' c '&' d '<' b;

theorem :: BVFUNC_9:31
a '&' b '&' c '&' d '&' e '<' a &
a '&' b '&' c '&' d '&' e '<' b;

theorem :: BVFUNC_9:32
a '&' b '&' c '&' d '&' e '&' f '<' a &
a '&' b '&' c '&' d '&' e '&' f '<' b;

theorem :: BVFUNC_9:33
a '&' b '&' c '&' d '&' e '&' f '&' g '<' a &
a '&' b '&' c '&' d '&' e '&' f '&' g '<' b;

theorem :: BVFUNC_9:34
a '<' b & c '<' d implies a '&' c '<' b '&' d;

theorem :: BVFUNC_9:35
a '&' b '<' c implies a '&' 'not' c '<' 'not' b;

theorem :: BVFUNC_9:36
(a 'imp' c) '&' (b 'imp' c) '&' (a 'or' b) '<' c;

theorem :: BVFUNC_9:37
((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c;

theorem :: BVFUNC_9:38
a '<' b & c '<' d implies a 'or' c '<' b 'or' d;

theorem :: BVFUNC_9:39
a '<' a 'or' b;

theorem :: BVFUNC_9:40
a '&' b '<' a 'or' b;
```