:: A Theory of Boolean Valued Functions and Quantifiers withRespect to Partitions
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received December 21, 1998
:: Copyright (c) 1998 Association of Mizar Users

definition

let X be set ;
:: original: PARTITIONS
redefine func PARTITIONS X -> Part-Family of X;
coherence
PARTITIONS X is Part-Family of X

proof end;

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 b₁ being Element of F holds b₁ is a_partition of X by EQREL_1:def 10;

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 <> {} ) )

proof end;

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 b₁ being a_partition of Y st
for x being set holds
( x in b₁ 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 <> {} ) )

proof end;

uniqueness
for b₁, b₂ being a_partition of Y st ( for x being set holds
( x in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines '/\' BVFUNC_2:def 1 :

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b₃ being a_partition of Y holds
( b₃ = '/\' G iff for x being set holds
( x in b₃ 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 ;
pred b 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 )

proof end;

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 b₁ being a_partition of Y st
for x being set holds
( x in b₁ iff x is_upper_min_depend_of G ) ) & ( not G <> {} implies ex b₁ being a_partition of Y st b₁ = %I Y ) )

proof end;

uniqueness
for b₁, b₂ being a_partition of Y holds
( ( G <> {} & ( for x being set holds
( x in b₁ iff x is_upper_min_depend_of G ) ) & ( for x being set holds
( x in b₂ iff x is_upper_min_depend_of G ) ) implies b₁ = b₂ ) & ( not G <> {} & b₁ = %I Y & b₂ = %I Y implies b₁ = b₂ ) )

proof end;

consistency
for b₁ 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 b₃ being a_partition of Y holds
( ( G <> {} implies ( b₃ = '\/' G iff for x being set holds
( x in b₃ iff x is_upper_min_depend_of G ) ) ) & ( not G <> {} implies ( b₃ = '\/' G iff b₃ = %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

proof end;

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

proof end;

definition

let Y be non empty set ;
let G be Subset of (PARTITIONS Y);
attr G 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);
attr G 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);
pred G 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)

proof end;

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 Element of Funcs Y,BOOLEAN ;
let G be Subset of (PARTITIONS Y);
let PA be a_partition of Y;
pred a 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 Element of Funcs 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 Element of Funcs Y,BOOLEAN ;
let G be Subset of (PARTITIONS Y);
let PA be a_partition of Y;
func All a,PA,G -> Element of Funcs Y,BOOLEAN equals :: BVFUNC_2:def 9
B_INF a,(CompF PA,G);
correctness
coherence
B_INF a,(CompF PA,G) is Element of Funcs Y,BOOLEAN ;
;

end;

:: deftheorem defines All BVFUNC_2:def 9 :

for Y being non empty set
for a being Element of Funcs 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 Element of Funcs Y,BOOLEAN ;
let G be Subset of (PARTITIONS Y);
let PA be a_partition of Y;
func Ex a,PA,G -> Element of Funcs Y,BOOLEAN equals :: BVFUNC_2:def 10
B_SUP a,(CompF PA,G);
correctness
coherence
B_SUP a,(CompF PA,G) is Element of Funcs Y,BOOLEAN ;
;

end;

:: deftheorem defines Ex BVFUNC_2:def 10 :

for Y being non empty set
for a being Element of Funcs 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 Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds All a,PA,G is_dependent_of CompF PA,G

proof end;

theorem :: BVFUNC_2:6

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds Ex a,PA,G is_dependent_of CompF PA,G

proof end;

theorem :: BVFUNC_2:7

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds All (I_el Y),PA,G = I_el Y

proof end;

theorem :: BVFUNC_2:8

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds Ex (I_el Y),PA,G = I_el Y

proof end;

theorem :: BVFUNC_2:9

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds All (O_el Y),PA,G = O_el Y

proof end;

theorem :: BVFUNC_2:10

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds Ex (O_el Y),PA,G = O_el Y

proof end;

theorem :: BVFUNC_2:11

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds All a,PA,G '<' a

proof end;

theorem :: BVFUNC_2:12

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds a '<' Ex a,PA,G

proof end;

theorem :: BVFUNC_2:13

canceled;

theorem :: BVFUNC_2:14

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs 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

proof end;

theorem :: BVFUNC_2:15

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs 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)

proof end;

theorem :: BVFUNC_2:16

canceled;

theorem :: BVFUNC_2:17

for Y being non empty set
for a, b being Element of Funcs 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)

proof end;

theorem :: BVFUNC_2:18

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs 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

proof end;

theorem :: BVFUNC_2:19

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs 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

proof end;

theorem :: BVFUNC_2:20

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds 'not' (All a,PA,G) = Ex ('not' a),PA,G

proof end;

theorem :: BVFUNC_2:21

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds 'not' (Ex a,PA,G) = All ('not' a),PA,G

proof end;

theorem :: BVFUNC_2:22

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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)

proof end;

theorem :: BVFUNC_2:23

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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

proof end;

theorem Th24: :: BVFUNC_2:24

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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)

proof end;

theorem :: BVFUNC_2:25

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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 Th24;

theorem :: BVFUNC_2:26

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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

proof end;

theorem Th27: :: BVFUNC_2:27

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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)

proof end;

theorem :: BVFUNC_2:28

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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 Th27;

theorem :: BVFUNC_2:29

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, u being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds All (a '&' u),PA,G '<' (Ex a,PA,G) '&' u

proof end;

theorem Th30: :: BVFUNC_2:30

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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)

proof end;

theorem :: BVFUNC_2:31

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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 Th30;

theorem Th32: :: BVFUNC_2:32

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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)

proof end;

theorem :: BVFUNC_2:33

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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 Th32;

theorem Th34: :: BVFUNC_2:34

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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)

proof end;

theorem :: BVFUNC_2:35

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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 Th34;

theorem Th36: :: BVFUNC_2:36

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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)

proof end;

theorem :: BVFUNC_2:37

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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 Th36;

theorem :: BVFUNC_2:38

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds u 'imp' (Ex a,PA,G) '<' Ex (u 'imp' a),PA,G

proof end;

theorem :: BVFUNC_2:39

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, u being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds (Ex a,PA,G) 'imp' u '<' Ex (a 'imp' u),PA,G

proof end;

theorem Th40: :: BVFUNC_2:40

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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

proof end;

theorem :: BVFUNC_2:41

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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 Th40;