:: 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-2021 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 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 <> {} ) )
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 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 <> {} ) )
proof end;
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
proof end;
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 ;
pred b is_upper_min_depend_of G means :: 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 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 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 ) )
proof end;
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 ) )
proof end;
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
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 Function of Y,BOOLEAN;
let G be Subset of (PARTITIONS Y);
let PA be a_partition of Y;
pred a is_independent_of PA,G means :: BVFUNC_2:def 8
a is_dependent_of CompF (PA,G);
end;

:: deftheorem 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)
proof end;

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)
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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))
proof end;

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))
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

theorem :: BVFUNC_2:20
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 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:21
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 st u is_independent_of PA,G holds
All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
proof end;

theorem Th22: :: BVFUNC_2:22
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 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:23
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 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 a, u 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
proof end;

theorem Th25: :: BVFUNC_2:25
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 st u is_independent_of PA,G holds
All ((u '&' a),PA,G) = u '&' (All (a,PA,G))
proof end;

theorem :: BVFUNC_2:26
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 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
proof end;

theorem Th28: :: BVFUNC_2:28
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 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:29
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 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 a, u 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))
proof end;

theorem :: BVFUNC_2:31
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 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 a, u 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))
proof end;

theorem :: BVFUNC_2:33
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 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 a, u 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))
proof end;

theorem :: BVFUNC_2:35
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 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 a, u 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)
proof end;

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)
proof end;

theorem Th38: :: BVFUNC_2:38
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 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:39
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 st u is_independent_of PA,G holds
(Ex (a,PA,G)) 'xor' u '<' Ex ((a 'xor' u),PA,G) by Th38;