:: 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

end;
:: original: PARTITIONS

redefine func PARTITIONS X -> Part-Family of X;

coherence

PARTITIONS X is Part-Family of X

proof 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_{1} being Element of F holds b_{1} is a_partition of X
by EQREL_1:def 7;

end;
let F be non empty Part-Family of X;

:: original: Element

redefine mode Element of F -> a_partition of X;

coherence

for b

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

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

ex b_{1} being a_partition of Y st

for x being set holds

( x in b_{1} 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 b_{1}, b_{2} being a_partition of Y st ( for x being set holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

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

ex b

for x being set holds

( x in b

( 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

( x in b

( 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

( 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

proof end;

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

for Y being non empty set

for G being Subset of (PARTITIONS Y)

for b_{3} being a_partition of Y holds

( b_{3} = '/\' G iff for x being set holds

( x in b_{3} 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 Y being non empty set

for G being Subset of (PARTITIONS Y)

for b

( b

( x in b

( 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 ;

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

( ( 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 ) );

:: 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 ) ) );

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 )

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

( ( G <> {} implies ex b_{1} being a_partition of Y st

for x being set holds

( x in b_{1} iff x is_upper_min_depend_of G ) ) & ( not G <> {} implies ex b_{1} being a_partition of Y st b_{1} = %I Y ) )

for b_{1}, b_{2} being a_partition of Y holds

( ( G <> {} & ( for x being set holds

( x in b_{1} iff x is_upper_min_depend_of G ) ) & ( for x being set holds

( x in b_{2} iff x is_upper_min_depend_of G ) ) implies b_{1} = b_{2} ) & ( not G <> {} & b_{1} = %I Y & b_{2} = %I Y implies b_{1} = b_{2} ) )

for b_{1} being a_partition of Y holds verum
;

end;
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 for x being set holds

( x in it iff x is_upper_min_depend_of G ) if G <> {}

otherwise it = %I Y;

( ( G <> {} implies ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( ( G <> {} & ( for x being set holds

( x in b

( x in b

proof end;

consistency for b

:: deftheorem Def3 defines '\/' BVFUNC_2:def 3 :

for Y being non empty set

for G being Subset of (PARTITIONS Y)

for b_{3} being a_partition of Y holds

( ( G <> {} implies ( b_{3} = '\/' G iff for x being set holds

( x in b_{3} iff x is_upper_min_depend_of G ) ) ) & ( not G <> {} implies ( b_{3} = '\/' G iff b_{3} = %I Y ) ) );

for Y being non empty set

for G being Subset of (PARTITIONS Y)

for b

( ( G <> {} implies ( b

( x in b

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

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

for G being Subset of (PARTITIONS Y)

for PA being a_partition of Y st PA in G holds

PA '<' '\/' G

proof end;

begin

:: 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 );

for Y being non empty set

for G being Subset of (PARTITIONS Y) holds

( G is generating iff '/\' G = %I Y );

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

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

:: 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 ) );

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)

end;
let PA be a_partition of Y;

:: original: {

redefine func {PA} -> Subset of (PARTITIONS Y);

coherence

{PA} is Subset of (PARTITIONS Y)

proof end;

definition

let Y be non empty set ;

let PA be a_partition of Y;

let G be Subset of (PARTITIONS Y);

correctness

coherence

'/\' (G \ {PA}) is a_partition of Y;

;

end;
let PA be a_partition of Y;

let G be Subset of (PARTITIONS Y);

correctness

coherence

'/\' (G \ {PA}) is a_partition of Y;

;

:: 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});

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;

end;
let a be Function of Y,BOOLEAN;

let G be Subset of (PARTITIONS Y);

let PA be a_partition of Y;

:: 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) );

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;

correctness

coherence

B_INF (a,(CompF (PA,G))) is Function of Y,BOOLEAN;

;

end;
let a be Function of Y,BOOLEAN;

let G be Subset of (PARTITIONS Y);

let PA be a_partition of Y;

correctness

coherence

B_INF (a,(CompF (PA,G))) is Function of Y,BOOLEAN;

;

:: 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)));

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;

correctness

coherence

B_SUP (a,(CompF (PA,G))) is Function of Y,BOOLEAN;

;

end;
let a be Function of Y,BOOLEAN;

let G be Subset of (PARTITIONS Y);

let PA be a_partition of Y;

correctness

coherence

B_SUP (a,(CompF (PA,G))) is Function of Y,BOOLEAN;

;

:: 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)));

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)

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)

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

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

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

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

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

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)

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)

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

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

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)

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)

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)

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)

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

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

proof end;

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

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

proof end;

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

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

proof end;

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;

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

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

proof end;

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

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

proof end;

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;

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

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

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

proof end;

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;

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

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

proof end;

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;

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

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

proof end;

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;

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

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

proof end;

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;

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)

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)

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)

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

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)

proof end;

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;

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;