:: Predicate Calculus for Boolean Valued Functions, III :: by Shunichi Kobayashi and Yatsuka Nakamura :: :: Received July 14, 1999 :: Copyright (c) 1999-2021 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, EQREL_1, TARSKI, BVFUNC_2, FUNCOP_1, FUNCT_1, ZFMISC_1, SETFAM_1, RELAT_1, BVFUNC_1, XBOOLEAN; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MARGREL1, RELAT_1, SETFAM_1, FUNCT_1, FUNCT_2, EQREL_1, FUNCOP_1, PARTIT1, BVFUNC_1, BVFUNC_2, FUNCT_4; constructors SETFAM_1, FUNCT_4, XCMPLX_0, BVFUNC_1, BVFUNC_2, RELSET_1, NUMBERS, FUNCOP_1; registrations XBOOLE_0, FUNCOP_1, FUNCT_4, EQREL_1, MARGREL1, ORDINAL1; requirements SUBSET, BOOLE, ARITHM, NUMERALS; begin :: Chap. 1 Preliminaries reserve Y for non empty set, a, b for Function of Y,BOOLEAN, G for Subset of PARTITIONS(Y), A, B for a_partition of Y; theorem :: BVFUNC11:1 for z being Element of Y, PA,PB being a_partition of Y st PA '<' PB holds EqClass(z,PA) c= EqClass(z,PB); theorem :: BVFUNC11:2 for z being Element of Y, PA,PB being a_partition of Y holds EqClass(z ,PA) c= EqClass(z,PA '\/' PB); theorem :: BVFUNC11:3 for z being Element of Y, PA,PB being a_partition of Y holds EqClass(z ,PA '/\' PB) c= EqClass(z,PA); theorem :: BVFUNC11:4 for z being Element of Y, PA being a_partition of Y holds EqClass(z,PA ) c= EqClass(z,%O(Y)) & EqClass(z,%I(Y)) c= EqClass(z,PA); theorem :: BVFUNC11:5 for G being Subset of PARTITIONS(Y), A,B being a_partition of Y st G is independent & G={A,B} & A<>B holds for a,b being set st a in A & b in B holds a meets b; theorem :: BVFUNC11:6 for G being Subset of PARTITIONS(Y), A,B being a_partition of Y st G is independent & G={A,B} & A <> B holds '/\' G = A '/\' B; theorem :: BVFUNC11:7 for G being Subset of PARTITIONS(Y), A,B being a_partition of Y st G={ A,B} & A<>B holds CompF(A,G) = B; begin theorem :: BVFUNC11:8 a '<' b implies All(a,A,G) '<' Ex(b,A,G); theorem :: BVFUNC11:9 G is independent implies All(All(a,A,G),B,G) '<' Ex(All(a,B,G),A,G); theorem :: BVFUNC11:10 All(All(a,A,G),B,G) '<' Ex(Ex(a,B,G),A,G); theorem :: BVFUNC11:11 G is independent implies All(All(a,A,G),B,G) '<' All(Ex(a,B,G),A,G); theorem :: BVFUNC11:12 All(Ex(a,A,G),B,G) '<' Ex(Ex(a,B,G),A,G); theorem :: BVFUNC11:13 'not' Ex(All(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G); theorem :: BVFUNC11:14 G is independent implies Ex('not' All(a,A,G),B,G) '<' Ex(Ex( 'not' a,B,G),A,G); theorem :: BVFUNC11:15 G is independent implies 'not' All(All(a,A,G),B,G) = Ex('not' All(a,B,G),A,G) ; theorem :: BVFUNC11:16 G is independent implies All('not' All(a,A,G),B,G) '<' Ex(Ex('not' a,B ,G),A,G); theorem :: BVFUNC11:17 G is independent implies 'not' All(All(a,A,G),B,G) = Ex(Ex('not' a,B,G ),A,G) ; theorem :: BVFUNC11:18 G is independent implies 'not' All(All(a,A,G),B,G) '<' Ex(Ex('not' a,A ,G),B,G); :: from BVFUNC12 theorem :: BVFUNC11:19 'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G); theorem :: BVFUNC11:20 'not' Ex(All(a,A,G),B,G) = All(Ex('not' a,A,G),B,G); theorem :: BVFUNC11:21 'not' All(All(a,A,G),B,G) = Ex(Ex('not' a,A,G),B,G); theorem :: BVFUNC11:22 G is independent implies Ex(All(a,A,G),B,G) '<' Ex(Ex(a,B,G),A,G); theorem :: BVFUNC11:23 All(All(a,A,G),B,G) '<' All(Ex(a,A,G),B,G); theorem :: BVFUNC11:24 All(All(a,A,G),B,G) '<' Ex(Ex(a,A,G),B,G); theorem :: BVFUNC11:25 Ex(All(a,A,G),B,G) '<' Ex(Ex(a,A,G),B,G); :: BVFUNC13 theorem :: BVFUNC11:26 G is independent implies All('not' All(a,A,G),B,G) '<' 'not' All( All(a,B,G),A,G); theorem :: BVFUNC11:27 All(All('not' a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G); theorem :: BVFUNC11:28 All('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G); theorem :: BVFUNC11:29 G is independent implies All(Ex('not' a,A,G),B,G) '<' 'not' All( All(a,B,G),A,G); theorem :: BVFUNC11:30 G is independent implies Ex(All('not' a,A,G),B,G) '<' 'not' All(All(a, B,G),A,G); theorem :: BVFUNC11:31 G is independent implies Ex('not' Ex(a,A,G),B,G) '<' 'not' All( All(a,B,G),A,G); theorem :: BVFUNC11:32 G is independent implies 'not' All(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B ,G),A,G); theorem :: BVFUNC11:33 G is independent implies 'not' Ex(Ex(a,A,G),B,G) '<' 'not' Ex( All(a,B,G),A,G); theorem :: BVFUNC11:34 'not' Ex(Ex(a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G); theorem :: BVFUNC11:35 G is independent implies 'not' Ex(All(a,A,G),B,G) '<' 'not' All(All(a, B,G),A,G); theorem :: BVFUNC11:36 G is independent implies 'not' All(Ex(a,A,G),B,G) '<' 'not' All(All(a, B,G),A,G); theorem :: BVFUNC11:37 'not' Ex(Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G); theorem :: BVFUNC11:38 G is independent implies 'not' Ex(All(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G); theorem :: BVFUNC11:39 G is independent implies 'not' All(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G); theorem :: BVFUNC11:40 'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G); theorem :: BVFUNC11:41 G is independent implies 'not' All(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G); theorem :: BVFUNC11:42 G is independent implies 'not' Ex(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G); theorem :: BVFUNC11:43 'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G); theorem :: BVFUNC11:44 G is independent implies 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex( a,B,G),A,G); theorem :: BVFUNC11:45 G is independent implies 'not' All(Ex(a,A,G),B,G) '<' Ex(Ex( 'not' a,B,G),A,G); theorem :: BVFUNC11:46 'not' Ex(Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G); theorem :: BVFUNC11:47 G is independent implies 'not' All(Ex(a,A,G),B,G) '<' All(Ex( 'not' a,B,G),A,G); theorem :: BVFUNC11:48 G is independent implies 'not' Ex(Ex(a,A,G),B,G) '<' All(Ex( 'not' a,B,G),A,G); theorem :: BVFUNC11:49 'not' Ex(Ex(a,A,G),B,G) '<' Ex(All('not' a,B,G),A,G); theorem :: BVFUNC11:50 G is independent implies 'not' Ex(Ex(a,A,G),B,G) = All(All('not' a,B,G),A,G); theorem :: BVFUNC11:51 G is independent implies Ex('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B, G),A,G); theorem :: BVFUNC11:52 All('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G); theorem :: BVFUNC11:53 All('not' Ex(a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G); theorem :: BVFUNC11:54 G is independent implies All('not' Ex(a,A,G),B,G) = 'not' Ex(Ex(a,B,G) ,A,G); theorem :: BVFUNC11:55 G is independent implies Ex('not' All(a,A,G),B,G) = Ex('not' All(a,B,G ),A,G) ; theorem :: BVFUNC11:56 G is independent implies All('not' All(a,A,G),B,G) '<' Ex('not' All(a, B,G),A,G); theorem :: BVFUNC11:57 G is independent implies Ex('not' Ex(a,A,G),B,G) '<' Ex('not' All(a,B, G),A,G); theorem :: BVFUNC11:58 All('not' Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G); theorem :: BVFUNC11:59 G is independent implies Ex('not' Ex(a,A,G),B,G) '<' All('not' All(a,B ,G),A,G); theorem :: BVFUNC11:60 G is independent implies All('not' Ex(a,A,G),B,G) '<' All('not' All(a, B,G),A,G); theorem :: BVFUNC11:61 All('not' Ex(a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G); theorem :: BVFUNC11:62 G is independent implies All('not' Ex(a,A,G),B,G) = All('not' Ex(a,B,G ),A,G) ; theorem :: BVFUNC11:63 G is independent implies Ex('not' Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G ),A,G) ; theorem :: BVFUNC11:64 All('not' Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G); theorem :: BVFUNC11:65 G is independent implies Ex('not' Ex(a,A,G),B,G) '<' All(Ex('not' a,B, G),A,G); theorem :: BVFUNC11:66 G is independent implies All('not' Ex(a,A,G),B,G) '<' All(Ex('not' a,B ,G),A,G); theorem :: BVFUNC11:67 All('not' Ex(a,A,G),B,G) '<' Ex(All('not' a,B,G),A,G); theorem :: BVFUNC11:68 G is independent implies All('not' Ex(a,A,G),B,G) = All(All('not' a,B, G),A,G); theorem :: BVFUNC11:69 G is independent implies Ex(All('not' a,A,G),B,G) '<' 'not' Ex(All(a,B ,G),A,G); theorem :: BVFUNC11:70 G is independent implies All(All('not' a,A,G),B,G) '<' 'not' Ex(All(a, B,G),A,G); theorem :: BVFUNC11:71 All(All('not' a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G); theorem :: BVFUNC11:72 G is independent implies All(All('not' a,A,G),B,G) '<' 'not' Ex(Ex(a,B ,G),A,G); theorem :: BVFUNC11:73 G is independent implies Ex(Ex('not' a,A,G),B,G) '<' Ex('not' All(a,B, G),A,G); theorem :: BVFUNC11:74 G is independent implies All(Ex('not' a,A,G),B,G) '<' Ex('not' All(a,B ,G),A,G); theorem :: BVFUNC11:75 G is independent implies Ex(All('not' a,A,G),B,G) '<' Ex('not' All(a,B ,G),A,G); theorem :: BVFUNC11:76 All(All('not' a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G); theorem :: BVFUNC11:77 G is independent implies Ex(All('not' a,A,G),B,G) '<' All('not' All(a, B,G),A,G); theorem :: BVFUNC11:78 G is independent implies All(All('not' a,A,G),B,G) '<' All('not' All(a ,B,G),A,G); theorem :: BVFUNC11:79 All(All('not' a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G); theorem :: BVFUNC11:80 G is independent implies All(All('not' a,A,G),B,G) = All('not' Ex(a,B, G),A,G); theorem :: BVFUNC11:81 All(Ex('not' a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G); theorem :: BVFUNC11:82 G is independent implies Ex(All('not' a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G);