:: Propositional Calculus for Boolean Valued Functions, { V } :: by Shunichi Kobayashi :: :: Received May 5, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin Lm1: for Y being non empty set for a, b being Function of Y,BOOLEAN holds a '&' b '<' a proofend; Lm2: for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b ) proofend; Lm3: for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds ( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b ) proofend; Lm4: for Y being non empty set for a, b, c, d, e being Function of Y,BOOLEAN holds ( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b ) proofend; Lm5: for Y being non empty set for a, b, c, d, e, f being Function of Y,BOOLEAN holds ( ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' a & ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b ) proofend; Lm6: for Y being non empty set for a, b, c, d, e, f, g being Function of Y,BOOLEAN holds ( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b ) proofend; theorem Th1: :: BVFUNC_9:1 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (b 'imp' c) '<' a 'or' c proofend; theorem Th2: :: BVFUNC_9:2 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a '&' (a 'imp' b) '<' b proofend; theorem :: BVFUNC_9:3 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' ('not' b) '<' 'not' a proofend; theorem :: BVFUNC_9:4 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' ('not' a) '<' b proofend; theorem :: BVFUNC_9:5 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' b) '<' b proofend; theorem :: BVFUNC_9:6 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' ('not' b)) '<' 'not' a proofend; theorem :: BVFUNC_9:7 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b '&' c) '<' a 'imp' b proofend; theorem :: BVFUNC_9:8 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'imp' c '<' a 'imp' c proofend; theorem :: BVFUNC_9:9 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a '&' c) 'imp' b proofend; theorem :: BVFUNC_9:10 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a '&' c) 'imp' (b '&' c) proofend; theorem :: BVFUNC_9:11 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' a 'imp' (b 'or' c) proofend; theorem :: BVFUNC_9:12 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a 'or' c) 'imp' (b 'or' c) proofend; theorem :: BVFUNC_9:13 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'or' c '<' a 'or' c proofend; theorem :: BVFUNC_9:14 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds (a '&' b) 'or' (c '&' d) '<' a 'or' c proofend; theorem :: BVFUNC_9:15 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (b 'imp' c) '<' a 'or' c by Th1; theorem :: BVFUNC_9:16 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' c) '<' b 'or' c proofend; theorem :: BVFUNC_9:17 for Y being non empty set for a, c, b being Function of Y,BOOLEAN holds (a 'imp' c) '&' (b 'imp' ('not' c)) '<' ('not' a) 'or' ('not' b) proofend; theorem :: BVFUNC_9:18 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' c) '<' b 'or' c proofend; theorem Th19: :: BVFUNC_9:19 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' b) '&' (c 'imp' d) '<' (a '&' c) 'imp' (b '&' d) proofend; theorem :: BVFUNC_9:20 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b '&' c) proofend; theorem Th21: :: BVFUNC_9:21 for Y being non empty set for a, c, b being Function of Y,BOOLEAN holds (a 'imp' c) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c proofend; theorem Th22: :: BVFUNC_9:22 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' b) '&' (c 'imp' d) '<' (a 'or' c) 'imp' (b 'or' d) proofend; theorem :: BVFUNC_9:23 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b 'or' c) proofend; theorem Th24: :: BVFUNC_9:24 for Y being non empty set for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds ((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' a2 'imp' a1 proofend; Lm8: for Y being non empty set for a1, b1, c1, a2, b2, c2 being Function of 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))) 'imp' (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) = I_el Y proofend; Lm9: for Y being non empty set for a1, b1, c1, a2, b2, c2 being Function of 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))) 'imp' (((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (b2 '&' a2))) '&' ('not' (b2 '&' c2))) = I_el Y proofend; Lm10: for Y being non empty set for a1, b1, c1, a2, b2, c2 being Function of 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))) 'imp' (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) = I_el Y proofend; theorem :: BVFUNC_9:25 for Y being non empty set for a1, b1, c1, a2, b2, c2 being Function of 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) proofend; theorem Th26: :: BVFUNC_9:26 for Y being non empty set for a1, b1, a2, b2 being Function of Y,BOOLEAN holds (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) 'imp' ('not' (a1 '&' b1)) = I_el Y proofend; theorem :: BVFUNC_9:27 for Y being non empty set for a1, b1, c1, a2, b2, c2 being Function of 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)) proofend; theorem :: BVFUNC_9:28 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a '&' b '<' a by Lm1; theorem :: BVFUNC_9:29 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b ) by Lm2; theorem :: BVFUNC_9:30 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds ( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b ) by Lm3; theorem :: BVFUNC_9:31 for Y being non empty set for a, b, c, d, e being Function of Y,BOOLEAN holds ( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b ) by Lm4; theorem :: BVFUNC_9:32 for Y being non empty set for a, b, c, d, e, f being Function of Y,BOOLEAN holds ( ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' a & ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b ) by Lm5; theorem :: BVFUNC_9:33 for Y being non empty set for a, b, c, d, e, f, g being Function of Y,BOOLEAN holds ( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b ) by Lm6; theorem Th34: :: BVFUNC_9:34 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds a '&' c '<' b '&' d proofend; theorem :: BVFUNC_9:35 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds a '&' ('not' c) '<' 'not' b proofend; theorem :: BVFUNC_9:36 for Y being non empty set for a, c, b being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c proofend; theorem :: BVFUNC_9:37 for Y being non empty set for a, c, b being Function of Y,BOOLEAN holds ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c proofend; theorem :: BVFUNC_9:38 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds a 'or' c '<' b 'or' d proofend; theorem Th39: :: BVFUNC_9:39 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a '<' a 'or' b proofend; theorem :: BVFUNC_9:40 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a '&' b '<' a 'or' b proofend;