:: Predicate Calculus for Boolean Valued Functions, II :: by Shunichi Kobayashi and Yatsuka Nakamura :: :: Received March 13, 1999 :: Copyright (c) 1999-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, MARGREL1, PARTIT1, BVFUNC_1, XBOOLEAN, FUNCT_1, EQREL_1, BVFUNC_2; notations TARSKI, XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1, FUNCT_1, FUNCT_2, EQREL_1, BVFUNC_1, BVFUNC_2; constructors BINARITH, BVFUNC_1, BVFUNC_2, NUMBERS; registrations XBOOLEAN, MARGREL1; requirements SUBSET, BOOLE, ARITHM, NUMERALS; begin ::Chap. 1 Preliminaries reserve Y for non empty set; theorem :: BVFUNC_4:1 for a,b,c being Function of Y,BOOLEAN holds a '<' (b 'imp' c) implies a '&' b '<' c; theorem :: BVFUNC_4:2 for a,b,c being Function of Y,BOOLEAN holds a '&' b '<' c implies a '<' (b 'imp' c); theorem :: BVFUNC_4:3 for a,b being Function of Y,BOOLEAN holds a 'or' (a '&' b) = a; theorem :: BVFUNC_4:4 for a,b being Function of Y,BOOLEAN holds a '&' (a 'or' b) = a; theorem :: BVFUNC_4:5 for a being Function of Y,BOOLEAN holds a '&' 'not' a = O_el(Y); theorem :: BVFUNC_4:6 for a being Function of Y,BOOLEAN holds a 'or' 'not' a = I_el(Y); theorem :: BVFUNC_4:7 for a,b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'imp' b) '&' (b 'imp' a); theorem :: BVFUNC_4:8 for a,b being Function of Y,BOOLEAN holds a 'imp' b = 'not' a 'or' b; theorem :: BVFUNC_4:9 for a,b being Function of Y,BOOLEAN holds a 'xor' b = ('not' a '&' b) 'or' (a '&' 'not' b); theorem :: BVFUNC_4:10 for a,b being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el (Y) iff (a 'imp' b)=I_el(Y) & (b 'imp' a)=I_el(Y); theorem :: BVFUNC_4:11 for a,b being Function of Y,BOOLEAN holds a 'eqv' b=I_el(Y) implies 'not' a 'eqv' 'not' b=I_el(Y); theorem :: BVFUNC_4:12 for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y ) & (c 'eqv' d)=I_el(Y) implies ((a '&' c) 'eqv' (b '&' d))=I_el(Y); theorem :: BVFUNC_4:13 for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y ) & (c 'eqv' d)=I_el(Y) implies ((a 'imp' c) 'eqv' (b 'imp' d))=I_el(Y); theorem :: BVFUNC_4:14 for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y ) & (c 'eqv' d)=I_el(Y) implies ((a 'or' c) 'eqv' (b 'or' d))=I_el(Y); theorem :: BVFUNC_4:15 for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y ) & (c 'eqv' d)=I_el(Y) implies ((a 'eqv' c) 'eqv' (b 'eqv' d))=I_el(Y); begin ::Chap. 2 Predicate Calculus theorem :: BVFUNC_4:16 for a,b being Function of Y,BOOLEAN, G being Subset of PARTITIONS(Y), PA being a_partition of Y holds All(a 'eqv' b,PA,G) = All(a 'imp' b,PA,G) '&' All(b 'imp' a,PA,G); theorem :: BVFUNC_4:17 for a being Function of Y,BOOLEAN, G being Subset of PARTITIONS( Y), PA,PB being a_partition of Y holds All(a,PA,G) '<' Ex(a,PB,G); theorem :: BVFUNC_4:18 for a,u being Function of Y,BOOLEAN, G being Subset of PARTITIONS(Y), PA being a_partition of Y st a 'imp' u = I_el(Y) holds All(a,PA, G) 'imp' u = I_el(Y); theorem :: BVFUNC_4:19 for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS( Y), PA being a_partition of Y st u is_independent_of PA,G holds Ex(u,PA,G) '<' u; theorem :: BVFUNC_4:20 for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS( Y), PA being a_partition of Y st u is_independent_of PA,G holds u '<' All(u,PA, G); theorem :: BVFUNC_4:21 for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS( Y), PA,PB being a_partition of Y st u is_independent_of PB,G holds All(u,PA,G) '<' All(u,PB,G); theorem :: BVFUNC_4:22 for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS( Y), PA,PB being a_partition of Y st u is_independent_of PA,G holds Ex(u,PA,G) '<' Ex(u,PB,G); theorem :: BVFUNC_4:23 for a,b being Function of Y,BOOLEAN, G being Subset of PARTITIONS(Y), PA being a_partition of Y holds All(a 'eqv' b,PA,G) '<' All(a,PA ,G) 'eqv' All(b,PA,G); theorem :: BVFUNC_4:24 for a,b being Function of Y,BOOLEAN, G being Subset of PARTITIONS(Y), PA being a_partition of Y holds All(a '&' b,PA,G) '<' a '&' All( b,PA,G); theorem :: BVFUNC_4:25 for a,u being Function of Y,BOOLEAN, G being Subset of PARTITIONS(Y), PA being a_partition of Y holds All(a,PA,G) 'imp' u '<' Ex(a 'imp' u,PA,G); theorem :: BVFUNC_4:26 for a,b being Function of Y,BOOLEAN, G being Subset of PARTITIONS(Y), PA being a_partition of Y holds (a 'eqv' b)=I_el(Y) implies (All (a,PA,G) 'eqv' All(b,PA,G))=I_el(Y); theorem :: BVFUNC_4:27 for a,b being Function of Y,BOOLEAN, G being Subset of PARTITIONS(Y), PA being a_partition of Y holds (a 'eqv' b)=I_el(Y) implies (Ex( a,PA,G) 'eqv' Ex(b,PA,G))=I_el(Y);