The abstract of the Mizar article:

Propositional Calculus for Boolean Valued Functions. Part V

by

Shunichi Kobayashi

Received May 5, 1999

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;