:: 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
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
1
being
Element
of
F
holds
b
1
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
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
<>
{}
) )
proof
end;
uniqueness
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
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
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
<>
{}
) ) );
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
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
) )
proof
end;
uniqueness
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
) )
proof
end;
consistency
for
b
1
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
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
) ) );
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;
begin
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
:
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
)
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
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
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
)
)
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
;
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
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
)
)
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
;
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
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
;
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
)
)
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
;
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
)
)
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
;
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
)
)
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
;
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
)
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
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
;