:: A Theory of Boolean Valued Functions and Quantifiers with Respect to Partitions :: by Shunichi Kobayashi and Yatsuka Nakamura :: :: Received December 21, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users begin definition let X be set ; :: original:PARTITIONS redefine func PARTITIONS X -> Part-Family of X; coherence PARTITIONS X is Part-Family of X proofend; end; definition let X be set ; let F be non empty Part-Family of X; :: original:Element redefine mode Element of F -> a_partition of X; coherence for b1 being Element of F holds b1 is a_partition of X by EQREL_1:def_7; end; theorem Th1: :: BVFUNC_2:1 for Y being non empty set for G being Subset of (PARTITIONS Y) for y being Element of Y ex X being Subset of Y st ( y in X & ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & X = Intersect F & X <> {} ) ) proofend; definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); func '/\' G -> a_partition of Y means :Def1: :: BVFUNC_2:def 1 for x being set holds ( x in it iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ); existence ex b1 being a_partition of Y st for x being set holds ( x in b1 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) proofend; uniqueness for b1, b2 being a_partition of Y st ( for x being set holds ( x in b1 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ) & ( for x being set holds ( x in b2 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines '/\' BVFUNC_2:def_1_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) for b3 being a_partition of Y holds ( b3 = '/\' G iff for x being set holds ( x in b3 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ); definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); let b be set ; predb is_upper_min_depend_of G means :Def2: :: BVFUNC_2:def 2 ( ( for d being a_partition of Y st d in G holds b is_a_dependent_set_of d ) & ( for e being set st e c= b & ( for d being a_partition of Y st d in G holds e is_a_dependent_set_of d ) holds e = b ) ); end; :: deftheorem Def2 defines is_upper_min_depend_of BVFUNC_2:def_2_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) for b being set holds ( b is_upper_min_depend_of G iff ( ( for d being a_partition of Y st d in G holds b is_a_dependent_set_of d ) & ( for e being set st e c= b & ( for d being a_partition of Y st d in G holds e is_a_dependent_set_of d ) holds e = b ) ) ); theorem Th2: :: BVFUNC_2:2 for Y being non empty set for G being Subset of (PARTITIONS Y) for y being Element of Y st G <> {} holds ex X being Subset of Y st ( y in X & X is_upper_min_depend_of G ) proofend; definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); func '\/' G -> a_partition of Y means :Def3: :: BVFUNC_2:def 3 for x being set holds ( x in it iff x is_upper_min_depend_of G ) if G <> {} otherwise it = %I Y; existence ( ( G <> {} implies ex b1 being a_partition of Y st for x being set holds ( x in b1 iff x is_upper_min_depend_of G ) ) & ( not G <> {} implies ex b1 being a_partition of Y st b1 = %I Y ) ) proofend; uniqueness for b1, b2 being a_partition of Y holds ( ( G <> {} & ( for x being set holds ( x in b1 iff x is_upper_min_depend_of G ) ) & ( for x being set holds ( x in b2 iff x is_upper_min_depend_of G ) ) implies b1 = b2 ) & ( not G <> {} & b1 = %I Y & b2 = %I Y implies b1 = b2 ) ) proofend; consistency for b1 being a_partition of Y holds verum ; end; :: deftheorem Def3 defines '\/' BVFUNC_2:def_3_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) for b3 being a_partition of Y holds ( ( G <> {} implies ( b3 = '\/' G iff for x being set holds ( x in b3 iff x is_upper_min_depend_of G ) ) ) & ( not G <> {} implies ( b3 = '\/' G iff b3 = %I Y ) ) ); theorem :: BVFUNC_2:3 for Y being non empty set for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st PA in G holds PA '>' '/\' G proofend; theorem :: BVFUNC_2:4 for Y being non empty set for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st PA in G holds PA '<' '\/' G proofend; begin definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); attrG is generating means :: BVFUNC_2:def 4 '/\' G = %I Y; end; :: deftheorem defines generating BVFUNC_2:def_4_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) holds ( G is generating iff '/\' G = %I Y ); definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); attrG is independent means :: BVFUNC_2:def 5 for h being Function for F being Subset-Family of Y st dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) holds Intersect F <> {} ; end; :: deftheorem defines independent BVFUNC_2:def_5_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) holds ( G is independent iff for h being Function for F being Subset-Family of Y st dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) holds Intersect F <> {} ); definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); predG is_a_coordinate means :: BVFUNC_2:def 6 ( G is independent & G is generating ); end; :: deftheorem defines is_a_coordinate BVFUNC_2:def_6_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) holds ( G is_a_coordinate iff ( G is independent & G is generating ) ); definition let Y be non empty set ; let PA be a_partition of Y; :: original:{ redefine func{PA} -> Subset of (PARTITIONS Y); coherence {PA} is Subset of (PARTITIONS Y) proofend; end; definition let Y be non empty set ; let PA be a_partition of Y; let G be Subset of (PARTITIONS Y); func CompF (PA,G) -> a_partition of Y equals :: BVFUNC_2:def 7 '/\' (G \ {PA}); correctness coherence '/\' (G \ {PA}) is a_partition of Y; ; end; :: deftheorem defines CompF BVFUNC_2:def_7_:_ for Y being non empty set for PA being a_partition of Y for G being Subset of (PARTITIONS Y) holds CompF (PA,G) = '/\' (G \ {PA}); definition let Y be non empty set ; let a be Function of Y,BOOLEAN; let G be Subset of (PARTITIONS Y); let PA be a_partition of Y; preda is_independent_of PA,G means :Def8: :: BVFUNC_2:def 8 a is_dependent_of CompF (PA,G); end; :: deftheorem Def8 defines is_independent_of BVFUNC_2:def_8_:_ for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds ( a is_independent_of PA,G iff a is_dependent_of CompF (PA,G) ); definition let Y be non empty set ; let a be Function of Y,BOOLEAN; let G be Subset of (PARTITIONS Y); let PA be a_partition of Y; func All (a,PA,G) -> Function of Y,BOOLEAN equals :: BVFUNC_2:def 9 B_INF (a,(CompF (PA,G))); correctness coherence B_INF (a,(CompF (PA,G))) is Function of Y,BOOLEAN; ; end; :: deftheorem defines All BVFUNC_2:def_9_:_ for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All (a,PA,G) = B_INF (a,(CompF (PA,G))); definition let Y be non empty set ; let a be Function of Y,BOOLEAN; let G be Subset of (PARTITIONS Y); let PA be a_partition of Y; func Ex (a,PA,G) -> Function of Y,BOOLEAN equals :: BVFUNC_2:def 10 B_SUP (a,(CompF (PA,G))); correctness coherence B_SUP (a,(CompF (PA,G))) is Function of Y,BOOLEAN; ; end; :: deftheorem defines Ex BVFUNC_2:def_10_:_ for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds Ex (a,PA,G) = B_SUP (a,(CompF (PA,G))); theorem :: BVFUNC_2:5 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G) proofend; theorem :: BVFUNC_2:6 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex (a,PA,G) is_dependent_of CompF (PA,G) proofend; theorem :: BVFUNC_2:7 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((I_el Y),PA,G) = I_el Y proofend; theorem :: BVFUNC_2:8 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex ((I_el Y),PA,G) = I_el Y proofend; theorem :: BVFUNC_2:9 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((O_el Y),PA,G) = O_el Y proofend; theorem :: BVFUNC_2:10 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex ((O_el Y),PA,G) = O_el Y proofend; theorem :: BVFUNC_2:11 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All (a,PA,G) '<' a proofend; theorem :: BVFUNC_2:12 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds a '<' Ex (a,PA,G) proofend; theorem :: BVFUNC_2:13 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G) proofend; theorem :: BVFUNC_2:14 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G)) proofend; theorem :: BVFUNC_2:15 for Y being non empty set for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G)) proofend; theorem :: BVFUNC_2:16 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G) proofend; theorem :: BVFUNC_2:17 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G) proofend; theorem :: BVFUNC_2:18 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds 'not' (All (a,PA,G)) = Ex (('not' a),PA,G) proofend; theorem :: BVFUNC_2:19 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G) proofend; theorem :: BVFUNC_2:20 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G)) proofend; theorem :: BVFUNC_2:21 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u proofend; theorem Th22: :: BVFUNC_2:22 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G)) proofend; theorem :: BVFUNC_2:23 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'or' u),PA,G) = (All (a,PA,G)) 'or' u by Th22; theorem :: BVFUNC_2:24 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u proofend; theorem Th25: :: BVFUNC_2:25 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) proofend; theorem :: BVFUNC_2:26 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a '&' u),PA,G) = (All (a,PA,G)) '&' u by Th25; theorem :: BVFUNC_2:27 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, u being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u proofend; theorem Th28: :: BVFUNC_2:28 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G)) proofend; theorem :: BVFUNC_2:29 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'xor' u),PA,G) '<' (All (a,PA,G)) 'xor' u by Th28; theorem Th30: :: BVFUNC_2:30 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G)) proofend; theorem :: BVFUNC_2:31 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'eqv' u),PA,G) '<' (All (a,PA,G)) 'eqv' u by Th30; theorem Th32: :: BVFUNC_2:32 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) proofend; theorem :: BVFUNC_2:33 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((a 'or' u),PA,G) = (Ex (a,PA,G)) 'or' u by Th32; theorem Th34: :: BVFUNC_2:34 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) proofend; theorem :: BVFUNC_2:35 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((a '&' u),PA,G) = (Ex (a,PA,G)) '&' u by Th34; theorem :: BVFUNC_2:36 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y holds u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G) proofend; theorem :: BVFUNC_2:37 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, u being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) proofend; theorem Th38: :: BVFUNC_2:38 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G) proofend; theorem :: BVFUNC_2:39 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds (Ex (a,PA,G)) 'xor' u '<' Ex ((a 'xor' u),PA,G) by Th38;