Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

### Predicate Calculus for Boolean Valued Functions. Part II

**by****Shunichi Kobayashi, and****Yatsuka Nakamura**- Received March 13, 1999
- MML identifier: BVFUNC_4

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_2, MARGREL1, PARTIT1, BVFUNC_1, ZF_LANG, FUNCT_1, RELAT_1, BINARITH, EQREL_1, BVFUNC_2, T_1TOPSP; notation TARSKI, XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, RELAT_1, FUNCT_1, FRAENKEL, EQREL_1, BINARITH, BVFUNC_1, BVFUNC_2; constructors BINARITH, BVFUNC_2, BVFUNC_1; clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL; requirements SUBSET, BOOLE; begin ::Chap. 1 Preliminaries reserve Y for non empty set; theorem :: BVFUNC_4:1 for a,b,c being Element of Funcs(Y,BOOLEAN) holds a '<' (b 'imp' c) implies a '&' b '<' c; theorem :: BVFUNC_4:2 for a,b,c being Element of Funcs(Y,BOOLEAN) holds a '&' b '<' c implies a '<' (b 'imp' c); theorem :: BVFUNC_4:3 for a,b being Element of Funcs(Y,BOOLEAN) holds a 'or' (a '&' b) = a; theorem :: BVFUNC_4:4 for a,b being Element of Funcs(Y,BOOLEAN) holds a '&' (a 'or' b) = a; theorem :: BVFUNC_4:5 for a being Element of Funcs(Y,BOOLEAN) holds a '&' 'not' a = O_el(Y); theorem :: BVFUNC_4:6 for a being Element of Funcs(Y,BOOLEAN) holds a 'or' 'not' a = I_el(Y); theorem :: BVFUNC_4:7 for a,b being Element of Funcs(Y,BOOLEAN) holds a 'eqv' b = (a 'imp' b) '&' (b 'imp' a); theorem :: BVFUNC_4:8 for a,b being Element of Funcs(Y,BOOLEAN) holds a 'imp' b = 'not' a 'or' b; theorem :: BVFUNC_4:9 for a,b being Element of Funcs(Y,BOOLEAN) holds a 'xor' b = ('not' a '&' b) 'or' (a '&' 'not' b); theorem :: BVFUNC_4:10 for a,b being Element of Funcs(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,c being Element of Funcs(Y,BOOLEAN) holds (a 'eqv' b)=I_el(Y) & (b 'eqv' c)=I_el(Y) implies (a 'eqv' c)=I_el(Y); theorem :: BVFUNC_4:12 for a,b being Element of Funcs(Y,BOOLEAN) holds a 'eqv' b=I_el(Y) implies 'not' a 'eqv' 'not' b=I_el(Y); theorem :: BVFUNC_4:13 for a,b,c,d being Element of Funcs(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:14 for a,b,c,d being Element of Funcs(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:15 for a,b,c,d being Element of Funcs(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:16 for a,b,c,d being Element of Funcs(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:17 for a,b being Element of Funcs(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:18 for a being Element of Funcs(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:19 for a,u being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), PA being a_partition of Y st G is independent & PA in G & u is_independent_of PA,G holds a 'imp' u = I_el(Y) implies All(a,PA,G) 'imp' u = I_el(Y); theorem :: BVFUNC_4:20 for u being Element of Funcs(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:21 for u being Element of Funcs(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:22 for u being Element of Funcs(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:23 for u being Element of Funcs(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:24 for a,b being Element of Funcs(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:25 for a,b being Element of Funcs(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:26 for a,u being Element of Funcs(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:27 for a,b being Element of Funcs(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:28 for a,b being Element of Funcs(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);

Back to top