:: BVFUNC10 semantic presentation begin theorem :: BVFUNC10:1 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a) let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a) for z being Element of Y st (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE holds (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE proof let z be Element of Y; ::_thesis: ( (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE implies (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ) A1: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = (((a '&' b) 'or' (b '&' c)) . z) 'or' ((c '&' a) . z) by BVFUNC_1:def_4 .= (((a '&' b) . z) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by BVFUNC_1:def_4 .= (((a . z) '&' (b . z)) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c '&' a) . z) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c . z) '&' (a . z)) by MARGREL1:def_20 ; assume A2: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE now__::_thesis:_(_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_<>_TRUE_implies_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_=_TRUE_) A3: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = (((a 'or' b) '&' (b 'or' c)) . z) '&' ((c 'or' a) . z) by MARGREL1:def_20 .= (((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by MARGREL1:def_20 .= (((a . z) 'or' (b . z)) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by BVFUNC_1:def_4 .= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c 'or' a) . z) by BVFUNC_1:def_4 .= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z)) by BVFUNC_1:def_4 ; assume Z: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z <> TRUE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE now__::_thesis:_(_(_((a_._z)_'or'_(b_._z))_'&'_((b_._z)_'or'_(c_._z))_=_FALSE_&_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_=_TRUE_)_or_(_(c_._z)_'or'_(a_._z)_=_FALSE_&_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_=_TRUE_)_) percases ( ((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z)) = FALSE or (c . z) 'or' (a . z) = FALSE ) by Z, MARGREL1:12, A3, XBOOLEAN:def_3; caseA5: ((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z)) = FALSE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE now__::_thesis:_(_(_(a_._z)_'or'_(b_._z)_=_FALSE_&_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_=_TRUE_)_or_(_(b_._z)_'or'_(c_._z)_=_FALSE_&_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_=_TRUE_)_) percases ( (a . z) 'or' (b . z) = FALSE or (b . z) 'or' (c . z) = FALSE ) by A5, MARGREL1:12; caseA6: (a . z) 'or' (b . z) = FALSE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3; hence (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE by A2, A1, A6; ::_thesis: verum end; caseA7: (b . z) 'or' (c . z) = FALSE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ( c . z = TRUE or c . z = FALSE ) by XBOOLEAN:def_3; hence (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE by A2, A1, A7; ::_thesis: verum end; end; end; hence (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ; ::_thesis: verum end; caseA8: (c . z) 'or' (a . z) = FALSE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3; hence (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE by A2, A1, A8; ::_thesis: verum end; end; end; hence (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ; ::_thesis: verum end; hence (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ; ::_thesis: verum end; then A9: ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) '<' ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a) by BVFUNC_1:def_12; for z being Element of Y st (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE holds (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE proof let z be Element of Y; ::_thesis: ( (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE implies (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE ) A10: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = (((a 'or' b) '&' (b 'or' c)) . z) '&' ((c 'or' a) . z) by MARGREL1:def_20 .= (((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by MARGREL1:def_20 .= (((a . z) 'or' (b . z)) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by BVFUNC_1:def_4 .= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c 'or' a) . z) by BVFUNC_1:def_4 .= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z)) by BVFUNC_1:def_4 ; assume A11: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ; ::_thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE now__::_thesis:_(_(((a_'&'_b)_'or'_(b_'&'_c))_'or'_(c_'&'_a))_._z_<>_TRUE_implies_(((a_'&'_b)_'or'_(b_'&'_c))_'or'_(c_'&'_a))_._z_=_TRUE_) A12: ( (b . z) '&' (c . z) = TRUE or (b . z) '&' (c . z) = FALSE ) by XBOOLEAN:def_3; A13: ( (c . z) '&' (a . z) = TRUE or (c . z) '&' (a . z) = FALSE ) by XBOOLEAN:def_3; A15: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = (((a '&' b) 'or' (b '&' c)) . z) 'or' ((c '&' a) . z) by BVFUNC_1:def_4 .= (((a '&' b) . z) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by BVFUNC_1:def_4 .= (((a . z) '&' (b . z)) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c '&' a) . z) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c . z) '&' (a . z)) by MARGREL1:def_20 ; assume A16: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z <> TRUE ; ::_thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE now__::_thesis:_(_(_a_._z_=_FALSE_&_b_._z_=_FALSE_&_(((a_'&'_b)_'or'_(b_'&'_c))_'or'_(c_'&'_a))_._z_=_TRUE_)_or_(_b_._z_=_FALSE_&_c_._z_=_FALSE_&_(((a_'&'_b)_'or'_(b_'&'_c))_'or'_(c_'&'_a))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_a_._z_=_FALSE_&_(((a_'&'_b)_'or'_(b_'&'_c))_'or'_(c_'&'_a))_._z_=_TRUE_)_) percases ( ( a . z = FALSE & b . z = FALSE ) or ( b . z = FALSE & c . z = FALSE ) or ( c . z = FALSE & a . z = FALSE ) ) by A16, A15, XBOOLEAN:def_3, A13, A12, MARGREL1:12; case ( a . z = FALSE & b . z = FALSE ) ; ::_thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE hence (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE by A11, A10; ::_thesis: verum end; case ( b . z = FALSE & c . z = FALSE ) ; ::_thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE hence (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE by A11, A10; ::_thesis: verum end; case ( c . z = FALSE & a . z = FALSE ) ; ::_thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE hence (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE by A11, A10; ::_thesis: verum end; end; end; hence (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE ; ::_thesis: verum end; hence (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE ; ::_thesis: verum end; then ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a) '<' ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) by BVFUNC_1:def_12; hence ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a) by A9, BVFUNC_1:15; ::_thesis: verum end; Lm1: for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) '<' ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) '<' ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) '<' ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a))) . z = TRUE or (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE ) A1: (((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a))) . z = (((a '&' ('not' b)) 'or' (b '&' ('not' c))) . z) 'or' ((c '&' ('not' a)) . z) by BVFUNC_1:def_4 .= (((a '&' ('not' b)) . z) 'or' ((b '&' ('not' c)) . z)) 'or' ((c '&' ('not' a)) . z) by BVFUNC_1:def_4 .= (((a . z) '&' (('not' b) . z)) 'or' ((b '&' ('not' c)) . z)) 'or' ((c '&' ('not' a)) . z) by MARGREL1:def_20 .= (((a . z) '&' (('not' b) . z)) 'or' ((b . z) '&' (('not' c) . z))) 'or' ((c '&' ('not' a)) . z) by MARGREL1:def_20 .= (((a . z) '&' (('not' b) . z)) 'or' ((b . z) '&' (('not' c) . z))) 'or' ((c . z) '&' (('not' a) . z)) by MARGREL1:def_20 .= (((a . z) '&' ('not' (b . z))) 'or' ((b . z) '&' (('not' c) . z))) 'or' ((c . z) '&' (('not' a) . z)) by MARGREL1:def_19 .= (((a . z) '&' ('not' (b . z))) 'or' ((b . z) '&' ('not' (c . z)))) 'or' ((c . z) '&' (('not' a) . z)) by MARGREL1:def_19 .= (((a . z) '&' ('not' (b . z))) 'or' ((b . z) '&' ('not' (c . z)))) 'or' ((c . z) '&' ('not' (a . z))) by MARGREL1:def_19 ; assume A2: (((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a))) . z = TRUE ; ::_thesis: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE now__::_thesis:_(_(((b_'&'_('not'_a))_'or'_(c_'&'_('not'_b)))_'or'_(a_'&'_('not'_c)))_._z_<>_TRUE_implies_(((b_'&'_('not'_a))_'or'_(c_'&'_('not'_b)))_'or'_(a_'&'_('not'_c)))_._z_=_TRUE_) A3: ( (a . z) '&' (('not' c) . z) = TRUE or (a . z) '&' (('not' c) . z) = FALSE ) by XBOOLEAN:def_3; assume A4: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z <> TRUE ; ::_thesis: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE A5: ( (c . z) '&' (('not' b) . z) = TRUE or (c . z) '&' (('not' b) . z) = FALSE ) by XBOOLEAN:def_3; A6: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = (((b '&' ('not' a)) 'or' (c '&' ('not' b))) . z) 'or' ((a '&' ('not' c)) . z) by BVFUNC_1:def_4 .= (((b '&' ('not' a)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' ((a '&' ('not' c)) . z) by BVFUNC_1:def_4 .= (((b . z) '&' (('not' a) . z)) 'or' ((c '&' ('not' b)) . z)) 'or' ((a '&' ('not' c)) . z) by MARGREL1:def_20 .= (((b . z) '&' (('not' a) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' ((a '&' ('not' c)) . z) by MARGREL1:def_20 .= (((b . z) '&' (('not' a) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' ((a . z) '&' (('not' c) . z)) by MARGREL1:def_20 ; ( ((b . z) '&' (('not' a) . z)) 'or' ((c . z) '&' (('not' b) . z)) = TRUE or ((b . z) '&' (('not' a) . z)) 'or' ((c . z) '&' (('not' b) . z)) = FALSE ) by XBOOLEAN:def_3; then A7: ( b . z = FALSE or ('not' a) . z = FALSE ) by A4, A6, A5, MARGREL1:12; now__::_thesis:_(_(_a_._z_=_FALSE_&_(((b_'&'_('not'_a))_'or'_(c_'&'_('not'_b)))_'or'_(a_'&'_('not'_c)))_._z_=_TRUE_)_or_(_('not'_c)_._z_=_FALSE_&_(((b_'&'_('not'_a))_'or'_(c_'&'_('not'_b)))_'or'_(a_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( a . z = FALSE or ('not' c) . z = FALSE ) by A4, A6, A3, MARGREL1:12; case a . z = FALSE ; ::_thesis: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE hence (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE by A2, A1, A6, A7, MARGREL1:def_19; ::_thesis: verum end; case ('not' c) . z = FALSE ; ::_thesis: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE then A8: 'not' (c . z) = FALSE by MARGREL1:def_19; then 'not' (b . z) = FALSE by A4, A6, A5, MARGREL1:def_19; hence (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE by A2, A1, A6, A5, A8, MARGREL1:def_19; ::_thesis: verum end; end; end; hence (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; hence (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC10:2 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) = ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) = ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) = ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c)) ( ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) '<' ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c)) & ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c)) '<' ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) ) by Lm1; hence ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) = ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c)) by BVFUNC_1:15; ::_thesis: verum end; Lm2: for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a))) . z = TRUE or (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ) A1: (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a))) . z = (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) . z) '&' ((c 'or' ('not' a)) . z) by MARGREL1:def_20 .= (((a 'or' ('not' b)) . z) '&' ((b 'or' ('not' c)) . z)) '&' ((c 'or' ('not' a)) . z) by MARGREL1:def_20 .= (((a . z) 'or' (('not' b) . z)) '&' ((b 'or' ('not' c)) . z)) '&' ((c 'or' ('not' a)) . z) by BVFUNC_1:def_4 .= (((a . z) 'or' (('not' b) . z)) '&' ((b . z) 'or' (('not' c) . z))) '&' ((c 'or' ('not' a)) . z) by BVFUNC_1:def_4 .= (((a . z) 'or' (('not' b) . z)) '&' ((b . z) 'or' (('not' c) . z))) '&' ((c . z) 'or' (('not' a) . z)) by BVFUNC_1:def_4 .= (((a . z) 'or' ('not' (b . z))) '&' ((b . z) 'or' (('not' c) . z))) '&' ((c . z) 'or' (('not' a) . z)) by MARGREL1:def_19 .= (((a . z) 'or' ('not' (b . z))) '&' ((b . z) 'or' ('not' (c . z)))) '&' ((c . z) 'or' (('not' a) . z)) by MARGREL1:def_19 .= (((a . z) 'or' ('not' (b . z))) '&' ((b . z) 'or' ('not' (c . z)))) '&' ((c . z) 'or' ('not' (a . z))) by MARGREL1:def_19 ; assume A2: (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a))) . z = TRUE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE now__::_thesis:_(_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_<>_TRUE_implies_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_=_TRUE_) A3: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) . z) '&' ((a 'or' ('not' c)) . z) by MARGREL1:def_20 .= (((b 'or' ('not' a)) . z) '&' ((c 'or' ('not' b)) . z)) '&' ((a 'or' ('not' c)) . z) by MARGREL1:def_20 .= (((b . z) 'or' (('not' a) . z)) '&' ((c 'or' ('not' b)) . z)) '&' ((a 'or' ('not' c)) . z) by BVFUNC_1:def_4 .= (((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z))) '&' ((a 'or' ('not' c)) . z) by BVFUNC_1:def_4 .= (((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z))) '&' ((a . z) 'or' (('not' c) . z)) by BVFUNC_1:def_4 ; assume Z: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z <> TRUE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE now__::_thesis:_(_(_((b_._z)_'or'_(('not'_a)_._z))_'&'_((c_._z)_'or'_(('not'_b)_._z))_=_FALSE_&_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_=_TRUE_)_or_(_(a_._z)_'or'_(('not'_c)_._z)_=_FALSE_&_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_=_TRUE_)_) percases ( ((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z)) = FALSE or (a . z) 'or' (('not' c) . z) = FALSE ) by Z, A3, XBOOLEAN:def_3, MARGREL1:12; caseA5: ((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z)) = FALSE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE now__::_thesis:_(_(_(b_._z)_'or'_(('not'_a)_._z)_=_FALSE_&_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_=_TRUE_)_or_(_(c_._z)_'or'_(('not'_b)_._z)_=_FALSE_&_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_=_TRUE_)_) percases ( (b . z) 'or' (('not' a) . z) = FALSE or (c . z) 'or' (('not' b) . z) = FALSE ) by A5, MARGREL1:12; caseA6: (b . z) 'or' (('not' a) . z) = FALSE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE A7: ( ('not' a) . z = TRUE or ('not' a) . z = FALSE ) by XBOOLEAN:def_3; then 'not' (a . z) = FALSE by A6, MARGREL1:def_19; hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE by A2, A1, A6, A7, XBOOLEAN:138; ::_thesis: verum end; caseA8: (c . z) 'or' (('not' b) . z) = FALSE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE A9: ( ('not' b) . z = TRUE or ('not' b) . z = FALSE ) by XBOOLEAN:def_3; then 'not' (b . z) = FALSE by A8, MARGREL1:def_19; hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE by A2, A1, A8, A9, XBOOLEAN:138; ::_thesis: verum end; end; end; hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ; ::_thesis: verum end; caseA10: (a . z) 'or' (('not' c) . z) = FALSE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE A11: ( ('not' c) . z = TRUE or ('not' c) . z = FALSE ) by XBOOLEAN:def_3; then 'not' (c . z) = FALSE by A10, MARGREL1:def_19; hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE by A2, A1, A10, A11, XBOOLEAN:138; ::_thesis: verum end; end; end; hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ; ::_thesis: verum end; hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC10:3 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) ( ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) & ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) '<' ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) ) by Lm2; hence ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) by BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC10:4 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds c 'imp' (a 'or' b) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds c 'imp' (a 'or' b) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( c 'imp' a = I_el Y & c 'imp' b = I_el Y implies c 'imp' (a 'or' b) = I_el Y ) assume A1: ( c 'imp' a = I_el Y & c 'imp' b = I_el Y ) ; ::_thesis: c 'imp' (a 'or' b) = I_el Y c 'imp' (a 'or' b) = (c 'imp' a) 'or' (c 'imp' b) by BVFUNC_7:3 .= I_el Y by A1 ; hence c 'imp' (a 'or' b) = I_el Y ; ::_thesis: verum end; theorem :: BVFUNC10:5 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds (a '&' b) 'imp' c = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds (a '&' b) 'imp' c = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' c = I_el Y & b 'imp' c = I_el Y implies (a '&' b) 'imp' c = I_el Y ) ( a 'imp' c = I_el Y & b 'imp' c = I_el Y implies (a '&' b) 'imp' (c '&' c) = I_el Y ) by BVFUNC_6:21; hence ( a 'imp' c = I_el Y & b 'imp' c = I_el Y implies (a '&' b) 'imp' c = I_el Y ) ; ::_thesis: verum end; theorem :: BVFUNC10:6 for Y being non empty set for a1, a2, b1, b2, c1, c2 being Function of Y,BOOLEAN holds (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1) '<' (a2 'or' b2) 'or' c2 proof let Y be non empty set ; ::_thesis: for a1, a2, b1, b2, c1, c2 being Function of Y,BOOLEAN holds (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1) '<' (a2 'or' b2) 'or' c2 let a1, a2, b1, b2, c1, c2 be Function of Y,BOOLEAN; ::_thesis: (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1) '<' (a2 'or' b2) 'or' c2 let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) . z = TRUE or ((a2 'or' b2) 'or' c2) . z = TRUE ) A1: ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) . z = ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) . z) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def_20 .= ((((a1 'imp' a2) '&' (b1 'imp' b2)) . z) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def_20 .= ((((a1 'imp' a2) . z) '&' ((b1 'imp' b2) . z)) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def_20 .= ((((('not' a1) 'or' a2) . z) '&' ((b1 'imp' b2) . z)) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_4:8 .= ((((('not' a1) 'or' a2) . z) '&' ((('not' b1) 'or' b2) . z)) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_4:8 .= ((((('not' a1) 'or' a2) . z) '&' ((('not' b1) 'or' b2) . z)) '&' ((('not' c1) 'or' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_4:8 .= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) 'or' b2) . z)) '&' ((('not' c1) 'or' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def_4 .= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) 'or' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def_4 .= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def_4 .= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 'or' b1) . z) 'or' (c1 . z)) by BVFUNC_1:def_4 .= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by BVFUNC_1:def_4 .= (((('not' (a1 . z)) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def_19 .= (((('not' (a1 . z)) 'or' (a2 . z)) '&' (('not' (b1 . z)) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def_19 .= (((('not' (a1 . z)) 'or' (a2 . z)) '&' (('not' (b1 . z)) 'or' (b2 . z))) '&' (('not' (c1 . z)) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def_19 ; assume A2: ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) . z = TRUE ; ::_thesis: ((a2 'or' b2) 'or' c2) . z = TRUE now__::_thesis:_not_((a2_'or'_b2)_'or'_c2)_._z_<>_TRUE A3: ( b2 . z = TRUE or b2 . z = FALSE ) by XBOOLEAN:def_3; A4: ( c2 . z = TRUE or c2 . z = FALSE ) by XBOOLEAN:def_3; A5: ((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' ((a1 'or' b1) 'or' c1) = (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' c1) by BVFUNC_1:12 .= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' ((('not' a1) '&' ('not' b1)) '&' (('not' c1) '&' c1)) by BVFUNC_1:4 .= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' ((('not' a1) '&' ('not' b1)) '&' (O_el Y)) by BVFUNC_4:5 .= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' (O_el Y) by BVFUNC_1:5 .= ((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1) by BVFUNC_1:9 .= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' b1) by BVFUNC_1:12 .= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (((('not' a1) '&' ('not' c1)) '&' ('not' b1)) '&' b1) by BVFUNC_1:4 .= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' ((('not' a1) '&' ('not' c1)) '&' (('not' b1) '&' b1)) by BVFUNC_1:4 .= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' ((('not' a1) '&' ('not' c1)) '&' (O_el Y)) by BVFUNC_4:5 .= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (O_el Y) by BVFUNC_1:5 .= ((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1 by BVFUNC_1:9 .= ((('not' b1) '&' ('not' c1)) '&' ('not' a1)) '&' a1 by BVFUNC_1:4 .= (('not' b1) '&' ('not' c1)) '&' (('not' a1) '&' a1) by BVFUNC_1:4 .= (('not' b1) '&' ('not' c1)) '&' (O_el Y) by BVFUNC_4:5 .= O_el Y by BVFUNC_1:5 ; A6: ( (a2 . z) 'or' (b2 . z) = TRUE or (a2 . z) 'or' (b2 . z) = FALSE ) by XBOOLEAN:def_3; A7: ((a2 'or' b2) 'or' c2) . z = ((a2 'or' b2) . z) 'or' (c2 . z) by BVFUNC_1:def_4 .= ((a2 . z) 'or' (b2 . z)) 'or' (c2 . z) by BVFUNC_1:def_4 ; assume ((a2 'or' b2) 'or' c2) . z <> TRUE ; ::_thesis: contradiction then (((('not' (a1 . z)) 'or' (a2 . z)) '&' (('not' (b1 . z)) 'or' (b2 . z))) '&' (('not' (c1 . z)) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) = (((('not' a1) . z) '&' ('not' (b1 . z))) '&' ('not' (c1 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by A7, A6, A4, A3, MARGREL1:def_19 .= (((('not' a1) . z) '&' (('not' b1) . z)) '&' ('not' (c1 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def_19 .= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def_19 .= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 'or' b1) . z) 'or' (c1 . z)) by BVFUNC_1:def_4 .= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def_4 .= (((('not' a1) '&' ('not' b1)) . z) '&' (('not' c1) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def_20 .= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) . z) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def_20 .= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' ((a1 'or' b1) 'or' c1)) . z by MARGREL1:def_20 ; hence contradiction by A2, A1, A5, BVFUNC_1:def_10; ::_thesis: verum end; hence ((a2 'or' b2) 'or' c2) . z = TRUE ; ::_thesis: verum end; Lm3: for Y being non empty set for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) proof let Y be non empty set ; ::_thesis: for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) let a1, a2, b1, b2 be Function of Y,BOOLEAN; ::_thesis: (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z = TRUE or ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ) A1: ((((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z = ((((('not' a1) 'or' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z by BVFUNC_4:8 .= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z by BVFUNC_4:8 .= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) '&' (a1 'or' a2)) . z) '&' (('not' (b1 '&' b2)) . z) by MARGREL1:def_20 .= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) . z) '&' ((a1 'or' a2) . z)) '&' (('not' (b1 '&' b2)) . z) by MARGREL1:def_20 .= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) . z) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:14 .= ((((('not' a1) 'or' b1) . z) '&' ((('not' a2) 'or' b2) . z)) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by MARGREL1:def_20 .= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) 'or' b2) . z)) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:def_4 .= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:def_4 .= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:def_4 .= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) . z) 'or' (('not' b2) . z)) by BVFUNC_1:def_4 .= (((('not' (a1 . z)) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) . z) 'or' (('not' b2) . z)) by MARGREL1:def_19 .= (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) . z) 'or' (('not' b2) . z)) by MARGREL1:def_19 .= (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' (('not' b2) . z)) by MARGREL1:def_19 .= (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) by MARGREL1:def_19 ; assume A2: ((((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z = TRUE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE now__::_thesis:_(_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_<>_TRUE_implies_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_) A3: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = ((((('not' b1) 'or' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z by BVFUNC_4:8 .= ((((('not' b1) 'or' a1) '&' (('not' b2) 'or' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z by BVFUNC_4:8 .= ((((('not' b1) 'or' a1) '&' (('not' b2) 'or' a2)) '&' (b1 'or' b2)) . z) '&' (('not' (a1 '&' a2)) . z) by MARGREL1:def_20 .= ((((('not' b1) 'or' a1) '&' (('not' b2) 'or' a2)) . z) '&' ((b1 'or' b2) . z)) '&' (('not' (a1 '&' a2)) . z) by MARGREL1:def_20 .= ((((('not' b1) 'or' a1) . z) '&' ((('not' b2) 'or' a2) . z)) '&' ((b1 'or' b2) . z)) '&' (('not' (a1 '&' a2)) . z) by MARGREL1:def_20 .= ((((('not' b1) 'or' a1) . z) '&' ((('not' b2) 'or' a2) . z)) '&' ((b1 'or' b2) . z)) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:14 .= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) 'or' a2) . z)) '&' ((b1 'or' b2) . z)) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:def_4 .= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 'or' b2) . z)) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:def_4 .= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z))) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:def_4 .= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z))) '&' ((('not' a1) . z) 'or' (('not' a2) . z)) by BVFUNC_1:def_4 ; assume ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z <> TRUE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE then A4: ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z))) '&' ((('not' a1) . z) 'or' (('not' a2) . z)) = FALSE by A3, XBOOLEAN:def_3; now__::_thesis:_(_(_(((('not'_b1)_._z)_'or'_(a1_._z))_'&'_((('not'_b2)_._z)_'or'_(a2_._z)))_'&'_((b1_._z)_'or'_(b2_._z))_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_or_(_(('not'_a1)_._z)_'or'_(('not'_a2)_._z)_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_) percases ( (((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z)) = FALSE or (('not' a1) . z) 'or' (('not' a2) . z) = FALSE ) by A4, MARGREL1:12; caseA5: (((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z)) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE now__::_thesis:_(_(_((('not'_b1)_._z)_'or'_(a1_._z))_'&'_((('not'_b2)_._z)_'or'_(a2_._z))_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_or_(_(b1_._z)_'or'_(b2_._z)_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_) percases ( ((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z)) = FALSE or (b1 . z) 'or' (b2 . z) = FALSE ) by A5, MARGREL1:12; caseA6: ((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z)) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE now__::_thesis:_(_(_(('not'_b1)_._z)_'or'_(a1_._z)_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_or_(_(('not'_b2)_._z)_'or'_(a2_._z)_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_) percases ( (('not' b1) . z) 'or' (a1 . z) = FALSE or (('not' b2) . z) 'or' (a2 . z) = FALSE ) by A6, MARGREL1:12; caseA7: (('not' b1) . z) 'or' (a1 . z) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE A8: ( a1 . z = TRUE or a1 . z = FALSE ) by XBOOLEAN:def_3; then 'not' (b1 . z) = FALSE by A7, MARGREL1:def_19; then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = (((a2 . z) '&' ('not' (a2 . z))) 'or' ((a2 . z) '&' (b2 . z))) '&' ('not' (b2 . z)) by A7, A8, XBOOLEAN:8 .= (FALSE 'or' ((a2 . z) '&' (b2 . z))) '&' ('not' (b2 . z)) by XBOOLEAN:138 .= ((a2 . z) '&' (b2 . z)) '&' ('not' (b2 . z)) .= (a2 . z) '&' ((b2 . z) '&' ('not' (b2 . z))) .= FALSE '&' (a2 . z) by XBOOLEAN:138 .= FALSE ; hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; ::_thesis: verum end; caseA9: (('not' b2) . z) 'or' (a2 . z) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE A10: ( a2 . z = TRUE or a2 . z = FALSE ) by XBOOLEAN:def_3; then 'not' (b2 . z) = FALSE by A9, MARGREL1:def_19; then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = (((a1 . z) '&' ('not' (a1 . z))) 'or' ((a1 . z) '&' (b1 . z))) '&' ('not' (b1 . z)) by A9, A10, XBOOLEAN:8 .= (FALSE 'or' ((a1 . z) '&' (b1 . z))) '&' ('not' (b1 . z)) by XBOOLEAN:138 .= ((a1 . z) '&' (b1 . z)) '&' ('not' (b1 . z)) .= (a1 . z) '&' ((b1 . z) '&' ('not' (b1 . z))) .= FALSE '&' (a1 . z) by XBOOLEAN:138 .= FALSE ; hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; ::_thesis: verum end; end; end; hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; ::_thesis: verum end; caseA11: (b1 . z) 'or' (b2 . z) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE reconsider a2z = a2 . z as boolean set ; reconsider a1z = a1 . z as boolean set ; ( b1 . z = TRUE or b1 . z = FALSE ) by XBOOLEAN:def_3; then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = ('not' (a1 . z)) '&' (('not' (a2 . z)) '&' ((a1 . z) 'or' (a2 . z))) by A11 .= ('not' (a1 . z)) '&' ((('not' (a2 . z)) '&' (a1 . z)) 'or' (('not' a2z) '&' a2z)) by XBOOLEAN:8 .= ('not' (a1 . z)) '&' ((('not' (a2 . z)) '&' (a1 . z)) 'or' FALSE) by XBOOLEAN:138 .= ('not' (a1 . z)) '&' ((a1 . z) '&' ('not' (a2 . z))) .= (('not' a1z) '&' a1z) '&' ('not' (a2 . z)) .= FALSE '&' ('not' (a2 . z)) by XBOOLEAN:138 .= FALSE ; hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; ::_thesis: verum end; end; end; hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; ::_thesis: verum end; caseA12: (('not' a1) . z) 'or' (('not' a2) . z) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ( ('not' a2) . z = TRUE or ('not' a2) . z = FALSE ) by XBOOLEAN:def_3; then ( 'not' (a1 . z) = FALSE & 'not' (a2 . z) = FALSE ) by A12, MARGREL1:def_19; then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = (b1 . z) '&' ((b2 . z) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z)))) .= (b1 . z) '&' (((b2 . z) '&' ('not' (b1 . z))) 'or' ((b2 . z) '&' ('not' (b2 . z)))) by XBOOLEAN:8 .= (b1 . z) '&' (((b2 . z) '&' ('not' (b1 . z))) 'or' FALSE) by XBOOLEAN:138 .= (b1 . z) '&' (('not' (b1 . z)) '&' (b2 . z)) .= ((b1 . z) '&' ('not' (b1 . z))) '&' (b2 . z) .= FALSE '&' (b2 . z) by XBOOLEAN:138 .= FALSE ; hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; ::_thesis: verum end; end; end; hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; ::_thesis: verum end; hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC10:7 for Y being non empty set for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) = (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) proof let Y be non empty set ; ::_thesis: for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) = (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) let a1, a2, b1, b2 be Function of Y,BOOLEAN; ::_thesis: (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) = (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) ( (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) & (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) '<' (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) ) by Lm3; hence (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) = (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) by BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC10:8 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds (a 'or' b) '&' (c 'or' d) = (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d) proof let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds (a 'or' b) '&' (c 'or' d) = (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d) let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) '&' (c 'or' d) = (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d) (a 'or' b) '&' (c 'or' d) = ((a 'or' b) '&' c) 'or' ((a 'or' b) '&' d) by BVFUNC_1:12 .= ((a '&' c) 'or' (b '&' c)) 'or' ((a 'or' b) '&' d) by BVFUNC_1:12 .= ((a '&' c) 'or' (b '&' c)) 'or' ((a '&' d) 'or' (b '&' d)) by BVFUNC_1:12 .= (((a '&' c) 'or' (b '&' c)) 'or' (a '&' d)) 'or' (b '&' d) by BVFUNC_1:8 .= (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d) by BVFUNC_1:8 ; hence (a 'or' b) '&' (c 'or' d) = (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d) ; ::_thesis: verum end; theorem :: BVFUNC10:9 for Y being non empty set for a1, a2, b1, b2, b3 being Function of Y,BOOLEAN holds (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) proof let Y be non empty set ; ::_thesis: for a1, a2, b1, b2, b3 being Function of Y,BOOLEAN holds (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) let a1, a2, b1, b2, b3 be Function of Y,BOOLEAN; ::_thesis: (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) = ((((a1 'or' (b1 '&' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) by BVFUNC_1:11 .= (((a1 'or' ((b1 '&' b2) '&' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) by BVFUNC_1:11 .= ((a1 'or' ((b1 '&' b2) '&' b3)) '&' ((a2 'or' b1) '&' (a2 'or' b2))) '&' (a2 'or' b3) by BVFUNC_1:4 .= (a1 'or' ((b1 '&' b2) '&' b3)) '&' (((a2 'or' b1) '&' (a2 'or' b2)) '&' (a2 'or' b3)) by BVFUNC_1:4 .= (a1 'or' ((b1 '&' b2) '&' b3)) '&' ((a2 'or' (b1 '&' b2)) '&' (a2 'or' b3)) by BVFUNC_1:11 .= (a1 'or' ((b1 '&' b2) '&' b3)) '&' (a2 'or' ((b1 '&' b2) '&' b3)) by BVFUNC_1:11 .= (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) by BVFUNC_1:11 ; hence (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) ; ::_thesis: verum end; theorem :: BVFUNC10:10 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) proof let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) A1: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) '&' (c 'imp' d) by BVFUNC_7:12 .= ((a 'imp' b) '&' (b 'imp' c)) '&' ((a 'imp' c) '&' (c 'imp' d)) by BVFUNC_1:4 .= ((a 'imp' b) '&' (b 'imp' c)) '&' (((a 'imp' c) '&' (c 'imp' d)) '&' (a 'imp' d)) by BVFUNC_7:12 .= (((a 'imp' b) '&' (b 'imp' c)) '&' ((a 'imp' c) '&' (c 'imp' d))) '&' (a 'imp' d) by BVFUNC_1:4 .= ((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4 .= (((a 'imp' b) '&' ((b 'imp' c) '&' (c 'imp' d))) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4 .= (((a 'imp' b) '&' (((b 'imp' c) '&' (c 'imp' d)) '&' (b 'imp' d))) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_7:12 .= ((((a 'imp' b) '&' ((b 'imp' c) '&' (c 'imp' d))) '&' (b 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4 .= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (b 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4 .= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (b 'imp' d)) '&' (a 'imp' d) by BVFUNC_1:4 .= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d)) '&' (b 'imp' d) by BVFUNC_1:4 ; ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) = ((('not' a) 'or' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) by BVFUNC_4:8 .= ((('not' a) 'or' ((b '&' c) '&' d)) '&' (('not' b) 'or' (c '&' d))) '&' (c 'imp' d) by BVFUNC_4:8 .= ((('not' a) 'or' ((b '&' c) '&' d)) '&' (('not' b) 'or' (c '&' d))) '&' (('not' c) 'or' d) by BVFUNC_4:8 .= ((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' (c '&' d))) '&' (('not' c) 'or' d) by BVFUNC_5:39 .= ((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' ((('not' b) 'or' c) '&' (('not' b) 'or' d))) '&' (('not' c) 'or' d) by BVFUNC_1:11 .= (((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' c)) '&' (('not' b) 'or' d)) '&' (('not' c) 'or' d) by BVFUNC_1:4 .= (((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d)) '&' (('not' c) 'or' d) by BVFUNC_1:4 .= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d)) '&' (('not' c) 'or' d) by BVFUNC_1:4 .= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' c) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_1:4 .= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_1:4 .= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_1:4 .= (((((a 'imp' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8 .= (((((a 'imp' b) '&' (b 'imp' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8 .= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8 .= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8 .= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8 .= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d)) '&' (b 'imp' d) by BVFUNC_4:8 ; hence ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) by A1; ::_thesis: verum end; theorem :: BVFUNC10:11 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b) '<' c 'or' d proof let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b) '<' c 'or' d let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b) '<' c 'or' d let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b)) . z = TRUE or (c 'or' d) . z = TRUE ) A1: (((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b)) . z = (((a 'imp' c) '&' (b 'imp' d)) . z) '&' ((a 'or' b) . z) by MARGREL1:def_20 .= (((a 'imp' c) . z) '&' ((b 'imp' d) . z)) '&' ((a 'or' b) . z) by MARGREL1:def_20 .= (((('not' a) 'or' c) . z) '&' ((b 'imp' d) . z)) '&' ((a 'or' b) . z) by BVFUNC_4:8 .= (((('not' a) 'or' c) . z) '&' ((('not' b) 'or' d) . z)) '&' ((a 'or' b) . z) by BVFUNC_4:8 .= (((('not' a) . z) 'or' (c . z)) '&' ((('not' b) 'or' d) . z)) '&' ((a 'or' b) . z) by BVFUNC_1:def_4 .= (((('not' a) . z) 'or' (c . z)) '&' ((('not' b) . z) 'or' (d . z))) '&' ((a 'or' b) . z) by BVFUNC_1:def_4 .= (((('not' a) . z) 'or' (c . z)) '&' ((('not' b) . z) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) by BVFUNC_1:def_4 .= ((('not' (a . z)) 'or' (c . z)) '&' ((('not' b) . z) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) by MARGREL1:def_19 .= ((('not' (a . z)) 'or' (c . z)) '&' (('not' (b . z)) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) by MARGREL1:def_19 ; reconsider bz = b . z as boolean set ; reconsider az = a . z as boolean set ; assume A2: (((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b)) . z = TRUE ; ::_thesis: (c 'or' d) . z = TRUE now__::_thesis:_(_(c_'or'_d)_._z_<>_TRUE_implies_(c_'or'_d)_._z_=_TRUE_) assume (c 'or' d) . z <> TRUE ; ::_thesis: (c 'or' d) . z = TRUE then (c 'or' d) . z = FALSE by XBOOLEAN:def_3; then A3: (c . z) 'or' (d . z) = FALSE by BVFUNC_1:def_4; ( d . z = TRUE or d . z = FALSE ) by XBOOLEAN:def_3; then ((('not' (a . z)) 'or' (c . z)) '&' (('not' (b . z)) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) = ('not' (a . z)) '&' (('not' (b . z)) '&' ((b . z) 'or' (a . z))) by A3 .= ('not' (a . z)) '&' ((('not' bz) '&' bz) 'or' (('not' (b . z)) '&' (a . z))) by XBOOLEAN:8 .= ('not' (a . z)) '&' (FALSE 'or' (('not' (b . z)) '&' (a . z))) by XBOOLEAN:138 .= ('not' (a . z)) '&' ((a . z) '&' ('not' (b . z))) .= (('not' az) '&' az) '&' ('not' (b . z)) .= FALSE '&' ('not' (b . z)) by XBOOLEAN:138 .= FALSE ; hence (c 'or' d) . z = TRUE by A2, A1; ::_thesis: verum end; hence (c 'or' d) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC10:12 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (((a '&' b) 'imp' ('not' c)) '&' a) '&' c '<' 'not' b proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (((a '&' b) 'imp' ('not' c)) '&' a) '&' c '<' 'not' b let a, b, c be Function of Y,BOOLEAN; ::_thesis: (((a '&' b) 'imp' ('not' c)) '&' a) '&' c '<' 'not' b let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((((a '&' b) 'imp' ('not' c)) '&' a) '&' c) . z = TRUE or ('not' b) . z = TRUE ) A1: ((((a '&' b) 'imp' ('not' c)) '&' a) '&' c) . z = ((((a '&' b) 'imp' ('not' c)) '&' a) . z) '&' (c . z) by MARGREL1:def_20 .= ((((a '&' b) 'imp' ('not' c)) . z) '&' (a . z)) '&' (c . z) by MARGREL1:def_20 .= (((('not' (a '&' b)) 'or' ('not' c)) . z) '&' (a . z)) '&' (c . z) by BVFUNC_4:8 .= ((((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) '&' (a . z)) '&' (c . z) by BVFUNC_1:14 .= ((((('not' a) 'or' ('not' b)) . z) 'or' (('not' c) . z)) '&' (a . z)) '&' (c . z) by BVFUNC_1:def_4 .= ((((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) '&' (a . z)) '&' (c . z) by BVFUNC_1:def_4 ; reconsider cz = c . z as boolean set ; assume A2: ((((a '&' b) 'imp' ('not' c)) '&' a) '&' c) . z = TRUE ; ::_thesis: ('not' b) . z = TRUE now__::_thesis:_(_('not'_b)_._z_<>_TRUE_implies_('not'_b)_._z_=_TRUE_) assume ('not' b) . z <> TRUE ; ::_thesis: ('not' b) . z = TRUE then ('not' b) . z = FALSE by XBOOLEAN:def_3; then ((((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) '&' (a . z)) '&' (c . z) = ((('not' (a . z)) 'or' (('not' c) . z)) '&' (a . z)) '&' (c . z) by MARGREL1:def_19 .= ((a . z) '&' (('not' (a . z)) 'or' ('not' (c . z)))) '&' (c . z) by MARGREL1:def_19 .= (((a . z) '&' ('not' (a . z))) 'or' ((a . z) '&' ('not' (c . z)))) '&' (c . z) by XBOOLEAN:8 .= (FALSE 'or' ((a . z) '&' ('not' (c . z)))) '&' (c . z) by XBOOLEAN:138 .= ((a . z) '&' ('not' (c . z))) '&' (c . z) .= (a . z) '&' (('not' cz) '&' cz) .= FALSE '&' (a . z) by XBOOLEAN:138 .= FALSE ; hence ('not' b) . z = TRUE by A2, A1; ::_thesis: verum end; hence ('not' b) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC10:13 for Y being non empty set for a1, a2, a3, b1, b2, b3 being Function of Y,BOOLEAN holds ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3) proof let Y be non empty set ; ::_thesis: for a1, a2, a3, b1, b2, b3 being Function of Y,BOOLEAN holds ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3) let a1, a2, a3, b1, b2, b3 be Function of Y,BOOLEAN; ::_thesis: ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3) ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3) = ('not' ((('not' b1) '&' ('not' b2)) '&' a3)) 'or' ((('not' a1) 'or' ('not' a2)) 'or' b3) by BVFUNC_4:8 .= ((('not' ('not' b1)) 'or' ('not' ('not' b2))) 'or' ('not' a3)) 'or' ((('not' a1) 'or' ('not' a2)) 'or' b3) by BVFUNC_5:37 .= (((b1 'or' b2) 'or' ('not' a3)) 'or' (('not' a1) 'or' ('not' a2))) 'or' b3 by BVFUNC_1:8 .= ((b1 'or' b2) 'or' ((('not' a1) 'or' ('not' a2)) 'or' ('not' a3))) 'or' b3 by BVFUNC_1:8 .= ((('not' a1) 'or' ('not' a2)) 'or' ('not' a3)) 'or' ((b1 'or' b2) 'or' b3) by BVFUNC_1:8 .= ('not' ((a1 '&' a2) '&' a3)) 'or' ((b1 'or' b2) 'or' b3) by BVFUNC_5:37 .= ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) by BVFUNC_4:8 ; hence ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3) ; ::_thesis: verum end; theorem :: BVFUNC10:14 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) for z being Element of Y st (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE holds (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE proof let z be Element of Y; ::_thesis: ( (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE implies (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) A1: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = (((a 'imp' b) '&' (b 'imp' c)) . z) '&' ((c 'imp' a) . z) by MARGREL1:def_20 .= (((a 'imp' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by MARGREL1:def_20 .= (((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8 .= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8 .= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_4:8 .= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def_4 .= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def_4 .= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by BVFUNC_1:def_4 .= ((('not' (a . z)) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def_19 .= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def_19 .= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' (('not' (c . z)) 'or' (a . z)) by MARGREL1:def_19 ; assume A2: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE now__::_thesis:_(_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_<>_TRUE_implies_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_) A3: ( (('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z)) = TRUE or (('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z)) = FALSE ) by XBOOLEAN:def_3; assume A4: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z <> TRUE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE A5: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = (((a '&' b) '&' c) . z) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by BVFUNC_1:def_4 .= (((a '&' b) . z) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) . z) '&' (('not' c) . z)) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) . z) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def_19 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' (('not' c) . z)) by MARGREL1:def_19 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z))) by MARGREL1:def_19 ; A6: ( ((a . z) '&' (b . z)) '&' (c . z) = TRUE or ((a . z) '&' (b . z)) '&' (c . z) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_(a_._z)_'&'_(b_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( (a . z) '&' (b . z) = FALSE or c . z = FALSE ) by A4, A5, A6, MARGREL1:12; caseA7: (a . z) '&' (b . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE now__::_thesis:_(_(_a_._z_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_or_(_b_._z_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( a . z = FALSE or b . z = FALSE ) by A7, MARGREL1:12; caseA8: a . z = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE now__::_thesis:_(_(_'not'_(b_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_or_(_'not'_(c_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( 'not' (b . z) = FALSE or 'not' (c . z) = FALSE ) by A4, A5, A3, A8, MARGREL1:12; case 'not' (b . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A8, XBOOLEAN:138; ::_thesis: verum end; case 'not' (c . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A8; ::_thesis: verum end; end; end; hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; caseA9: b . z = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE now__::_thesis:_(_(_'not'_(a_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_or_(_'not'_(c_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( 'not' (a . z) = FALSE or 'not' (c . z) = FALSE ) by A4, A5, A3, A9, MARGREL1:12; case 'not' (a . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A9; ::_thesis: verum end; case 'not' (c . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A9, XBOOLEAN:138; ::_thesis: verum end; end; end; hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; end; end; hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; caseA10: c . z = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE now__::_thesis:_(_(_'not'_(a_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_or_(_'not'_(b_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( 'not' (a . z) = FALSE or 'not' (b . z) = FALSE ) by A4, A5, A3, A10, MARGREL1:12; case 'not' (a . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A10, XBOOLEAN:138; ::_thesis: verum end; case 'not' (b . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A10; ::_thesis: verum end; end; end; hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; end; end; hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; then A11: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) '<' ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) by BVFUNC_1:def_12; for z being Element of Y st (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE holds (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE proof let z be Element of Y; ::_thesis: ( (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE implies (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ) A12: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = (((a '&' b) '&' c) . z) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by BVFUNC_1:def_4 .= (((a '&' b) . z) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) . z) '&' (('not' c) . z)) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) . z) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def_19 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' (('not' c) . z)) by MARGREL1:def_19 .= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z))) by MARGREL1:def_19 ; assume A13: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE now__::_thesis:_(_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_<>_TRUE_implies_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_=_TRUE_) A14: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = (((a 'imp' b) '&' (b 'imp' c)) . z) '&' ((c 'imp' a) . z) by MARGREL1:def_20 .= (((a 'imp' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by MARGREL1:def_20 .= (((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8 .= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8 .= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_4:8 .= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def_4 .= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def_4 .= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by BVFUNC_1:def_4 .= ((('not' (a . z)) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def_19 .= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def_19 .= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' (('not' (c . z)) 'or' (a . z)) by MARGREL1:def_19 ; assume (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z <> TRUE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE then A15: ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' (('not' (c . z)) 'or' (a . z)) = FALSE by A14, XBOOLEAN:def_3; now__::_thesis:_(_(_(('not'_(a_._z))_'or'_(b_._z))_'&'_(('not'_(b_._z))_'or'_(c_._z))_=_FALSE_&_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_=_TRUE_)_or_(_('not'_(c_._z))_'or'_(a_._z)_=_FALSE_&_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_=_TRUE_)_) percases ( (('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z)) = FALSE or ('not' (c . z)) 'or' (a . z) = FALSE ) by A15, MARGREL1:12; caseA16: (('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z)) = FALSE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE now__::_thesis:_(_(_('not'_(a_._z))_'or'_(b_._z)_=_FALSE_&_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_=_TRUE_)_or_(_('not'_(b_._z))_'or'_(c_._z)_=_FALSE_&_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_=_TRUE_)_) percases ( ('not' (a . z)) 'or' (b . z) = FALSE or ('not' (b . z)) 'or' (c . z) = FALSE ) by A16, MARGREL1:12; caseA17: ('not' (a . z)) 'or' (b . z) = FALSE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3; hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE by A13, A12, A17; ::_thesis: verum end; caseA18: ('not' (b . z)) 'or' (c . z) = FALSE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ( c . z = TRUE or c . z = FALSE ) by XBOOLEAN:def_3; hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE by A13, A12, A18; ::_thesis: verum end; end; end; hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; ::_thesis: verum end; caseA19: ('not' (c . z)) 'or' (a . z) = FALSE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3; hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE by A13, A12, A19; ::_thesis: verum end; end; end; hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; ::_thesis: verum end; hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; ::_thesis: verum end; then ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) '<' ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) by BVFUNC_1:def_12; hence ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) by A11, BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC10:15 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (a '&' b) '&' c proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (a '&' b) '&' c let a, b, c be Function of Y,BOOLEAN; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (a '&' b) '&' c (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (((('not' a) 'or' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) by BVFUNC_4:8 .= (((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) by BVFUNC_4:8 .= (((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' a)) '&' ((a 'or' b) 'or' c) by BVFUNC_4:8 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((('not' c) 'or' a) '&' ((a 'or' b) 'or' c)) by BVFUNC_1:4 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (((('not' c) 'or' a) '&' (a 'or' b)) 'or' ((('not' c) 'or' a) '&' c)) by BVFUNC_1:12 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (((('not' c) 'or' a) '&' (a 'or' b)) 'or' ((('not' c) '&' c) 'or' (a '&' c))) by BVFUNC_1:12 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (((('not' c) 'or' a) '&' (a 'or' b)) 'or' ((O_el Y) 'or' (a '&' c))) by BVFUNC_4:5 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (((('not' c) 'or' a) '&' (a 'or' b)) 'or' (a '&' c)) by BVFUNC_1:9 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((a 'or' (('not' c) '&' b)) 'or' (a '&' c)) by BVFUNC_1:11 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((a 'or' (a '&' c)) 'or' (('not' c) '&' b)) by BVFUNC_1:8 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (((a '&' (I_el Y)) 'or' (a '&' c)) 'or' (('not' c) '&' b)) by BVFUNC_1:6 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((a '&' ((I_el Y) 'or' c)) 'or' (('not' c) '&' b)) by BVFUNC_1:12 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((a '&' (I_el Y)) 'or' (('not' c) '&' b)) by BVFUNC_1:10 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (a 'or' (('not' c) '&' b)) by BVFUNC_1:6 .= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((a 'or' ('not' c)) '&' (a 'or' b)) by BVFUNC_1:11 .= ((a 'or' b) '&' ((('not' a) 'or' b) '&' (('not' b) 'or' c))) '&' (a 'or' ('not' c)) by BVFUNC_1:4 .= (((a 'or' b) '&' (('not' a) 'or' b)) '&' (('not' b) 'or' c)) '&' (a 'or' ('not' c)) by BVFUNC_1:4 .= (((a '&' ('not' a)) 'or' b) '&' (('not' b) 'or' c)) '&' (a 'or' ('not' c)) by BVFUNC_1:11 .= (((O_el Y) 'or' b) '&' (('not' b) 'or' c)) '&' (a 'or' ('not' c)) by BVFUNC_4:5 .= (b '&' (('not' b) 'or' c)) '&' (a 'or' ('not' c)) by BVFUNC_1:9 .= ((b '&' ('not' b)) 'or' (b '&' c)) '&' (a 'or' ('not' c)) by BVFUNC_1:12 .= ((O_el Y) 'or' (b '&' c)) '&' (a 'or' ('not' c)) by BVFUNC_4:5 .= (b '&' c) '&' (a 'or' ('not' c)) by BVFUNC_1:9 .= ((b '&' c) '&' a) 'or' ((b '&' c) '&' ('not' c)) by BVFUNC_1:12 .= ((b '&' c) '&' a) 'or' (b '&' (c '&' ('not' c))) by BVFUNC_1:4 .= ((b '&' c) '&' a) 'or' (b '&' (O_el Y)) by BVFUNC_4:5 .= ((b '&' c) '&' a) 'or' (O_el Y) by BVFUNC_1:5 .= (b '&' c) '&' a by BVFUNC_1:9 .= (a '&' b) '&' c by BVFUNC_1:4 ; hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (a '&' b) '&' c ; ::_thesis: verum end; Lm4: for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE or ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ) A1: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) . z) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def_4 .= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def_4 .= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) . z) '&' (('not' c) . z)) by MARGREL1:def_20 .= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) . z) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= ((((('not' a) '&' b) '&' c) . z) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= ((((('not' a) '&' b) . z) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= ((((('not' a) . z) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_19 .= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_19 .= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' ('not' (c . z))) by MARGREL1:def_19 ; assume A2: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE now__::_thesis:_(_((a_'or'_b)_'&'_('not'_((a_'&'_b)_'&'_c)))_._z_<>_TRUE_implies_((a_'or'_b)_'&'_('not'_((a_'&'_b)_'&'_c)))_._z_=_TRUE_) A3: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = ((a 'or' b) '&' ((('not' a) 'or' ('not' b)) 'or' ('not' c))) . z by BVFUNC_5:37 .= ((a 'or' b) . z) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by MARGREL1:def_20 .= ((a . z) 'or' (b . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def_4 .= ((a . z) 'or' (b . z)) '&' (((('not' a) 'or' ('not' b)) . z) 'or' (('not' c) . z)) by BVFUNC_1:def_4 .= ((a . z) 'or' (b . z)) '&' (((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by BVFUNC_1:def_4 .= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by MARGREL1:def_19 .= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' (('not' c) . z)) by MARGREL1:def_19 .= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z))) by MARGREL1:def_19 ; assume ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z <> TRUE ; ::_thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE then A4: ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z))) = FALSE by A3, XBOOLEAN:def_3; now__::_thesis:_(_(_(a_._z)_'or'_(b_._z)_=_FALSE_&_((a_'or'_b)_'&'_('not'_((a_'&'_b)_'&'_c)))_._z_=_TRUE_)_or_(_(('not'_(a_._z))_'or'_('not'_(b_._z)))_'or'_('not'_(c_._z))_=_FALSE_&_((a_'or'_b)_'&'_('not'_((a_'&'_b)_'&'_c)))_._z_=_TRUE_)_) percases ( (a . z) 'or' (b . z) = FALSE or (('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z)) = FALSE ) by A4, MARGREL1:12; caseA5: (a . z) 'or' (b . z) = FALSE ; ::_thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3; hence ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE by A2, A1, A5; ::_thesis: verum end; caseA6: (('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z)) = FALSE ; ::_thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE A7: ( 'not' (b . z) = TRUE or 'not' (b . z) = FALSE ) by XBOOLEAN:def_3; ( ('not' (a . z)) 'or' ('not' (b . z)) = TRUE or ('not' (a . z)) 'or' ('not' (b . z)) = FALSE ) by XBOOLEAN:def_3; hence ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE by A2, A1, A6, A7; ::_thesis: verum end; end; end; hence ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ; ::_thesis: verum end; hence ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC10:16 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) A1: (((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' ((c 'or' a) '&' ('not' ((a '&' b) '&' c))) = ((((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4 .= ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4 .= (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' (('not' ((a '&' b) '&' c)) '&' ('not' ((a '&' b) '&' c))) by BVFUNC_1:4 .= (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) ; for z being Element of Y st ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = TRUE holds ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE proof let z be Element of Y; ::_thesis: ( ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = TRUE implies ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ) A2: ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def_20 .= ((((a 'or' b) '&' (b 'or' c)) . z) '&' ((c 'or' a) . z)) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def_20 .= ((((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def_20 .= ((((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_5:37 .= ((((a . z) 'or' (b . z)) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def_4 .= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c 'or' a) . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def_4 .= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def_4 .= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' (((('not' a) 'or' ('not' b)) . z) 'or' (('not' c) . z)) by BVFUNC_1:def_4 .= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' (((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by BVFUNC_1:def_4 .= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' ((('not' (a . z)) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by MARGREL1:def_19 .= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' (('not' c) . z)) by MARGREL1:def_19 .= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z))) by MARGREL1:def_19 ; assume A3: ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE now__::_thesis:_(_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_<>_TRUE_implies_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_) A4: ( ((a . z) '&' (b . z)) '&' ('not' (c . z)) = TRUE or ((a . z) '&' (b . z)) '&' ('not' (c . z)) = FALSE ) by XBOOLEAN:def_3; assume A5: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z <> TRUE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE A6: ( ((a . z) '&' ('not' (b . z))) '&' (c . z) = TRUE or ((a . z) '&' ('not' (b . z))) '&' (c . z) = FALSE ) by XBOOLEAN:def_3; A7: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) . z) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def_4 .= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def_4 .= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) . z) '&' (('not' c) . z)) by MARGREL1:def_20 .= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) . z) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= ((((('not' a) '&' b) '&' c) . z) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= ((((('not' a) '&' b) . z) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= ((((('not' a) . z) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20 .= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_19 .= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_19 .= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' ('not' (c . z))) by MARGREL1:def_19 ; A8: ( ((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z)) = TRUE or ((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z)) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_('not'_(a_._z))_'&'_(b_._z)_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( ('not' (a . z)) '&' (b . z) = FALSE or c . z = FALSE ) by A5, A7, A8, A6, MARGREL1:12; caseA9: ('not' (a . z)) '&' (b . z) = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE now__::_thesis:_(_(_'not'_(a_._z)_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_or_(_b_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( 'not' (a . z) = FALSE or b . z = FALSE ) by A9, MARGREL1:12; caseA10: 'not' (a . z) = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE now__::_thesis:_(_(_'not'_(b_._z)_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( 'not' (b . z) = FALSE or c . z = FALSE ) by A5, A7, A6, A10, MARGREL1:12; case 'not' (b . z) = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A7, A10; ::_thesis: verum end; case c . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A7, A10; ::_thesis: verum end; end; end; hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; caseA11: b . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE now__::_thesis:_(_(_a_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( a . z = FALSE or c . z = FALSE ) by A5, A7, A6, A11, MARGREL1:12; case a . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A11; ::_thesis: verum end; case c . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A11; ::_thesis: verum end; end; end; hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; end; end; hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; caseA12: c . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE now__::_thesis:_(_(_a_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_or_(_b_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_) percases ( a . z = FALSE or b . z = FALSE ) by A5, A7, A4, A12, MARGREL1:12; case a . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A12; ::_thesis: verum end; case b . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A12; ::_thesis: verum end; end; end; hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; end; end; hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; hence ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum end; then A13: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) '<' (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) by BVFUNC_1:def_12; (((('not' c) '&' a) '&' b) 'or' ((c '&' ('not' a)) '&' b)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((c '&' a) '&' b)) by Lm4; then (((('not' c) '&' a) '&' b) 'or' ((c '&' ('not' a)) '&' b)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4; then (((a '&' b) '&' ('not' c)) 'or' ((c '&' ('not' a)) '&' b)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4; then (((a '&' b) '&' ('not' c)) 'or' ((('not' a) '&' b) '&' c)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4; then (((a '&' b) '&' ('not' c)) 'or' ((('not' a) '&' b) '&' c)) 'or' ((a '&' ('not' b)) '&' c) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4; then (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:8; then A14: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((c 'or' a) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:16; (((('not' b) '&' c) '&' a) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((b '&' c) '&' ('not' a)) '<' (b 'or' c) '&' ('not' ((b '&' c) '&' a)) by Lm4; then (((('not' b) '&' c) '&' a) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((b '&' c) '&' ('not' a)) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4; then (((('not' b) '&' c) '&' a) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((('not' a) '&' b) '&' c) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4; then (((a '&' ('not' b)) '&' c) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((('not' a) '&' b) '&' c) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4; then (((a '&' ('not' b)) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((('not' a) '&' b) '&' c) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4; then (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:8; then A15: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((b 'or' c) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:16; (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c)) by Lm4; then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:16; then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' (((a 'or' b) '&' ('not' ((a '&' b) '&' c))) '&' ((b 'or' c) '&' ('not' ((a '&' b) '&' c)))) = I_el Y by A15, BVFUNC_6:18; then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((((a 'or' b) '&' ('not' ((a '&' b) '&' c))) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:4; then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:4; then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' (((a 'or' b) '&' (b 'or' c)) '&' (('not' ((a '&' b) '&' c)) '&' ('not' ((a '&' b) '&' c)))) = I_el Y by BVFUNC_1:4; then ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' ((c 'or' a) '&' ('not' ((a '&' b) '&' c)))) = I_el Y by A14, BVFUNC_6:18; then (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) by A1, BVFUNC_1:16; hence (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) by A13, BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC10:17 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b '&' c) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b '&' c) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b '&' c) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or (a 'imp' (b '&' c)) . z = TRUE ) A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20 .= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8 .= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ; assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: (a 'imp' (b '&' c)) . z = TRUE now__::_thesis:_(_(a_'imp'_(b_'&'_c))_._z_<>_TRUE_implies_(a_'imp'_(b_'&'_c))_._z_=_TRUE_) A3: (a 'imp' (b '&' c)) . z = (('not' a) 'or' (b '&' c)) . z by BVFUNC_4:8 .= (('not' a) . z) 'or' ((b '&' c) . z) by BVFUNC_1:def_4 .= (('not' a) . z) 'or' ((b . z) '&' (c . z)) by MARGREL1:def_20 .= ('not' (a . z)) 'or' ((b . z) '&' (c . z)) by MARGREL1:def_19 ; assume A4: (a 'imp' (b '&' c)) . z <> TRUE ; ::_thesis: (a 'imp' (b '&' c)) . z = TRUE ( 'not' (a . z) = TRUE or 'not' (a . z) = FALSE ) by XBOOLEAN:def_3; then A5: ('not' a) . z = FALSE by A4, A3, MARGREL1:def_19; A6: ( (b . z) '&' (c . z) = TRUE or (b . z) '&' (c . z) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_b_._z_=_FALSE_&_(a_'imp'_(b_'&'_c))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_(a_'imp'_(b_'&'_c))_._z_=_TRUE_)_) percases ( b . z = FALSE or c . z = FALSE ) by A4, A3, A6, MARGREL1:12; case b . z = FALSE ; ::_thesis: (a 'imp' (b '&' c)) . z = TRUE hence (a 'imp' (b '&' c)) . z = TRUE by A2, A1, A5; ::_thesis: verum end; case c . z = FALSE ; ::_thesis: (a 'imp' (b '&' c)) . z = TRUE then ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) = (b . z) '&' ('not' (b . z)) by A5, MARGREL1:def_19 .= FALSE by XBOOLEAN:138 ; hence (a 'imp' (b '&' c)) . z = TRUE by A2, A1; ::_thesis: verum end; end; end; hence (a 'imp' (b '&' c)) . z = TRUE ; ::_thesis: verum end; hence (a 'imp' (b '&' c)) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC10:18 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or ((a 'or' b) 'imp' c) . z = TRUE ) A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20 .= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8 .= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ; assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: ((a 'or' b) 'imp' c) . z = TRUE now__::_thesis:_(_((a_'or'_b)_'imp'_c)_._z_<>_TRUE_implies_((a_'or'_b)_'imp'_c)_._z_=_TRUE_) A3: ( c . z = TRUE or c . z = FALSE ) by XBOOLEAN:def_3; assume A4: ((a 'or' b) 'imp' c) . z <> TRUE ; ::_thesis: ((a 'or' b) 'imp' c) . z = TRUE A5: ((a 'or' b) 'imp' c) . z = (('not' (a 'or' b)) 'or' c) . z by BVFUNC_4:8 .= ((('not' a) '&' ('not' b)) 'or' c) . z by BVFUNC_1:13 .= ((('not' a) '&' ('not' b)) . z) 'or' (c . z) by BVFUNC_1:def_4 .= ((('not' a) . z) '&' (('not' b) . z)) 'or' (c . z) by MARGREL1:def_20 ; A6: ( (('not' a) . z) '&' (('not' b) . z) = TRUE or (('not' a) . z) '&' (('not' b) . z) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_('not'_a)_._z_=_FALSE_&_((a_'or'_b)_'imp'_c)_._z_=_TRUE_)_or_(_('not'_b)_._z_=_FALSE_&_((a_'or'_b)_'imp'_c)_._z_=_TRUE_)_) percases ( ('not' a) . z = FALSE or ('not' b) . z = FALSE ) by A4, A5, A6, MARGREL1:12; case ('not' a) . z = FALSE ; ::_thesis: ((a 'or' b) 'imp' c) . z = TRUE then ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) = (b . z) '&' ('not' (b . z)) by A4, A5, A3, MARGREL1:def_19 .= FALSE by XBOOLEAN:138 ; hence ((a 'or' b) 'imp' c) . z = TRUE by A2, A1; ::_thesis: verum end; case ('not' b) . z = FALSE ; ::_thesis: ((a 'or' b) 'imp' c) . z = TRUE then ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) = ((('not' a) . z) 'or' (b . z)) '&' FALSE by A4, A5, XBOOLEAN:def_3 .= FALSE ; hence ((a 'or' b) 'imp' c) . z = TRUE by A2, A1; ::_thesis: verum end; end; end; hence ((a 'or' b) 'imp' c) . z = TRUE ; ::_thesis: verum end; hence ((a 'or' b) 'imp' c) . z = TRUE ; ::_thesis: verum end; theorem Th19: :: BVFUNC10:19 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' c) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' c) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' c) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or (a 'imp' (b 'or' c)) . z = TRUE ) A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20 .= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8 .= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ; assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: (a 'imp' (b 'or' c)) . z = TRUE now__::_thesis:_(_(a_'imp'_(b_'or'_c))_._z_<>_TRUE_implies_(a_'imp'_(b_'or'_c))_._z_=_TRUE_) assume (a 'imp' (b 'or' c)) . z <> TRUE ; ::_thesis: (a 'imp' (b 'or' c)) . z = TRUE A3: ( ('not' a) . z = TRUE or ('not' a) . z = FALSE ) by XBOOLEAN:def_3; A4: ( (b . z) 'or' (c . z) = TRUE or (b . z) 'or' (c . z) = FALSE ) by XBOOLEAN:def_3; A5: ( c . z = TRUE or c . z = FALSE ) by XBOOLEAN:def_3; (a 'imp' (b 'or' c)) . z = (('not' a) 'or' (b 'or' c)) . z by BVFUNC_4:8 .= (('not' a) . z) 'or' ((b 'or' c) . z) by BVFUNC_1:def_4 .= (('not' a) . z) 'or' ((b . z) 'or' (c . z)) by BVFUNC_1:def_4 ; hence (a 'imp' (b 'or' c)) . z = TRUE by A2, A1, A3, A4, A5; ::_thesis: verum end; hence (a 'imp' (b 'or' c)) . z = TRUE ; ::_thesis: verum end; theorem Th20: :: BVFUNC10:20 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or (a 'imp' (b 'or' ('not' c))) . z = TRUE ) A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20 .= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8 .= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ; assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: (a 'imp' (b 'or' ('not' c))) . z = TRUE now__::_thesis:_(_(a_'imp'_(b_'or'_('not'_c)))_._z_<>_TRUE_implies_(a_'imp'_(b_'or'_('not'_c)))_._z_=_TRUE_) assume (a 'imp' (b 'or' ('not' c))) . z <> TRUE ; ::_thesis: (a 'imp' (b 'or' ('not' c))) . z = TRUE A3: ( ('not' a) . z = TRUE or ('not' a) . z = FALSE ) by XBOOLEAN:def_3; A4: ( (b . z) 'or' (('not' c) . z) = TRUE or (b . z) 'or' (('not' c) . z) = FALSE ) by XBOOLEAN:def_3; A5: ( ('not' c) . z = TRUE or ('not' c) . z = FALSE ) by XBOOLEAN:def_3; (a 'imp' (b 'or' ('not' c))) . z = (('not' a) 'or' (b 'or' ('not' c))) . z by BVFUNC_4:8 .= (('not' a) . z) 'or' ((b 'or' ('not' c)) . z) by BVFUNC_1:def_4 .= (('not' a) . z) 'or' ((b . z) 'or' (('not' c) . z)) by BVFUNC_1:def_4 ; hence (a 'imp' (b 'or' ('not' c))) . z = TRUE by A2, A1, A3, A4, A5; ::_thesis: verum end; hence (a 'imp' (b 'or' ('not' c))) . z = TRUE ; ::_thesis: verum end; theorem Th21: :: BVFUNC10:21 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or (b 'imp' (c 'or' a)) . z = TRUE ) A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20 .= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8 .= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ; assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: (b 'imp' (c 'or' a)) . z = TRUE now__::_thesis:_(_(b_'imp'_(c_'or'_a))_._z_<>_TRUE_implies_(b_'imp'_(c_'or'_a))_._z_=_TRUE_) assume (b 'imp' (c 'or' a)) . z <> TRUE ; ::_thesis: (b 'imp' (c 'or' a)) . z = TRUE A3: ( ('not' b) . z = TRUE or ('not' b) . z = FALSE ) by XBOOLEAN:def_3; A4: ( (c . z) 'or' (a . z) = TRUE or (c . z) 'or' (a . z) = FALSE ) by XBOOLEAN:def_3; A5: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3; (b 'imp' (c 'or' a)) . z = (('not' b) 'or' (c 'or' a)) . z by BVFUNC_4:8 .= (('not' b) . z) 'or' ((c 'or' a) . z) by BVFUNC_1:def_4 .= (('not' b) . z) 'or' ((c . z) 'or' (a . z)) by BVFUNC_1:def_4 ; hence (b 'imp' (c 'or' a)) . z = TRUE by A2, A1, A3, A4, A5; ::_thesis: verum end; hence (b 'imp' (c 'or' a)) . z = TRUE ; ::_thesis: verum end; theorem Th22: :: BVFUNC10:22 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' ('not' a)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' ('not' a)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' ('not' a)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or (b 'imp' (c 'or' ('not' a))) . z = TRUE ) A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20 .= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8 .= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4 .= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ; assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: (b 'imp' (c 'or' ('not' a))) . z = TRUE now__::_thesis:_(_(b_'imp'_(c_'or'_('not'_a)))_._z_<>_TRUE_implies_(b_'imp'_(c_'or'_('not'_a)))_._z_=_TRUE_) assume (b 'imp' (c 'or' ('not' a))) . z <> TRUE ; ::_thesis: (b 'imp' (c 'or' ('not' a))) . z = TRUE A3: ( ('not' b) . z = TRUE or ('not' b) . z = FALSE ) by XBOOLEAN:def_3; A4: ( (c . z) 'or' (('not' a) . z) = TRUE or (c . z) 'or' (('not' a) . z) = FALSE ) by XBOOLEAN:def_3; A5: ( ('not' a) . z = TRUE or ('not' a) . z = FALSE ) by XBOOLEAN:def_3; (b 'imp' (c 'or' ('not' a))) . z = (('not' b) 'or' (c 'or' ('not' a))) . z by BVFUNC_4:8 .= (('not' b) . z) 'or' ((c 'or' ('not' a)) . z) by BVFUNC_1:def_4 .= (('not' b) . z) 'or' ((c . z) 'or' (('not' a) . z)) by BVFUNC_1:def_4 ; hence (b 'imp' (c 'or' ('not' a))) . z = TRUE by A2, A1, A3, A4, A5; ::_thesis: verum end; hence (b 'imp' (c 'or' ('not' a))) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC10:23 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' b) '&' (b 'imp' (c 'or' a)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' b) '&' (b 'imp' (c 'or' a)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' b) '&' (b 'imp' (c 'or' a)) (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a) by Th21; then A1: ((a 'imp' b) '&' (b 'imp' c)) 'imp' (b 'imp' (c 'or' a)) = I_el Y by BVFUNC_1:16; ((a 'imp' b) '&' (b 'imp' c)) 'imp' (a 'imp' b) = I_el Y by BVFUNC_6:38; then ((a 'imp' b) '&' (b 'imp' c)) 'imp' ((a 'imp' b) '&' (b 'imp' (c 'or' a))) = I_el Y by A1, BVFUNC_6:18; hence (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' b) '&' (b 'imp' (c 'or' a)) by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC10:24 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c) (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c)) by Th20; then A1: ((a 'imp' b) '&' (b 'imp' c)) 'imp' (a 'imp' (b 'or' ('not' c))) = I_el Y by BVFUNC_1:16; ((a 'imp' b) '&' (b 'imp' c)) 'imp' (b 'imp' c) = I_el Y by BVFUNC_6:38; then ((a 'imp' b) '&' (b 'imp' c)) 'imp' ((a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c)) = I_el Y by A1, BVFUNC_6:18; hence (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c) by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC10:25 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' c)) '&' (b 'imp' (c 'or' a)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' c)) '&' (b 'imp' (c 'or' a)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' c)) '&' (b 'imp' (c 'or' a)) (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a) by Th21; then A1: ((a 'imp' b) '&' (b 'imp' c)) 'imp' (b 'imp' (c 'or' a)) = I_el Y by BVFUNC_1:16; (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' c) by Th19; then ((a 'imp' b) '&' (b 'imp' c)) 'imp' (a 'imp' (b 'or' c)) = I_el Y by BVFUNC_1:16; then ((a 'imp' b) '&' (b 'imp' c)) 'imp' ((a 'imp' (b 'or' c)) '&' (b 'imp' (c 'or' a))) = I_el Y by A1, BVFUNC_6:18; hence (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' c)) '&' (b 'imp' (c 'or' a)) by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC10:26 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a)) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a)) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a)) (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a) by Th21; then A1: ((a 'imp' b) '&' (b 'imp' c)) 'imp' (b 'imp' (c 'or' a)) = I_el Y by BVFUNC_1:16; (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c)) by Th20; then ((a 'imp' b) '&' (b 'imp' c)) 'imp' (a 'imp' (b 'or' ('not' c))) = I_el Y by BVFUNC_1:16; then ((a 'imp' b) '&' (b 'imp' c)) 'imp' ((a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a))) = I_el Y by A1, BVFUNC_6:18; hence (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a)) by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC10:27 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a))) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a))) let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a))) (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' ('not' a)) by Th22; then A1: ((a 'imp' b) '&' (b 'imp' c)) 'imp' (b 'imp' (c 'or' ('not' a))) = I_el Y by BVFUNC_1:16; (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c)) by Th20; then ((a 'imp' b) '&' (b 'imp' c)) 'imp' (a 'imp' (b 'or' ('not' c))) = I_el Y by BVFUNC_1:16; then ((a 'imp' b) '&' (b 'imp' c)) 'imp' ((a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a)))) = I_el Y by A1, BVFUNC_6:18; hence (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a))) by BVFUNC_1:16; ::_thesis: verum end;