:: BVFUNC_2 semantic presentation

definition

let c₁ be set ;
redefine func PARTITIONS as PARTITIONS c₁ -> Part-Family of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty Part-Family of c₁;
redefine mode Element as Element of c₂ -> a_partition of a₁;
coherence by T_1TOPSP:def 3;

end;

theorem Th1: :: BVFUNC_2:1

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of b₁ ex b₄ being Subset of b₁ st
( b₃ in b₄ & ex b₅ being Functionex b₆ being Subset-Family of b₁ st
( dom b₅ = b₂ & rng b₅ = b₆ & ( for b₇ being set st b₇ in b₂ holds
b₅ . b₇ in b₇ ) & b₄ = Intersect b₆ & b₄ <> {} ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Subset of (PARTITIONS c₁);
func '/\' c₂ -> a_partition of a₁ means :Def1: :: BVFUNC_2:def 1
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being Functionex b₃ being Subset-Family of a₁ st
( dom b₂ = a₂ & rng b₂ = b₃ & ( for b₄ being set st b₄ in a₂ holds
b₂ . b₄ in b₄ ) & b₁ = Intersect b₃ & b₁ <> {} ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be non empty set ;
let c₂ be Subset of (PARTITIONS c₁);
let c₃ be set ;
pred c₃ is_upper_min_depend_of c₂ means :Def2: :: BVFUNC_2:def 2
( ( for b₁ being a_partition of a₁ st b₁ in a₂ holds
a₃ is_a_dependent_set_of b₁ ) & ( for b₁ being set st b₁ c= a₃ & ( for b₂ being a_partition of a₁ st b₂ in a₂ holds
b₁ is_a_dependent_set_of b₂ ) holds
b₁ = a₃ ) );

end;

:: deftheorem Def2 defines is_upper_min_depend_of BVFUNC_2:def 2 :

theorem Th2: :: BVFUNC_2:2

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of b₁ st b₂ <> {} holds
ex b₄ being Subset of b₁ st
( b₃ in b₄ & b₄ is_upper_min_depend_of b₂ )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Subset of (PARTITIONS c₁);
func '\/' c₂ -> a_partition of a₁ means :Def3: :: BVFUNC_2:def 3
for b₁ being set holds
( b₁ in a₃ iff b₁ is_upper_min_depend_of a₂ ) if a₂ <> {}
otherwise a₃ = %I a₁;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

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

theorem Th3: :: BVFUNC_2:3

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being a_partition of b₁ st b₃ in b₂ holds
b₃ '>' '/\' b₂

proof end;

theorem Th4: :: BVFUNC_2:4

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being a_partition of b₁ st b₃ in b₂ holds
b₃ '<' '\/' b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be Subset of (PARTITIONS c₁);
attr a₂ is generating means :: BVFUNC_2:def 4
'/\' a₂ = %I a₁;

end;

:: deftheorem Def4 defines generating BVFUNC_2:def 4 :

definition

let c₁ be non empty set ;
let c₂ be Subset of (PARTITIONS c₁);
attr a₂ is independent means :: BVFUNC_2:def 5
for b₁ being Function
for b₂ being Subset-Family of a₁ st dom b₁ = a₂ & rng b₁ = b₂ & ( for b₃ being set st b₃ in a₂ holds
b₁ . b₃ in b₃ ) holds
Intersect b₂ <> {} ;

end;

:: deftheorem Def5 defines independent BVFUNC_2:def 5 :

definition

let c₁ be non empty set ;
let c₂ be Subset of (PARTITIONS c₁);
pred c₂ is_a_coordinate means :: BVFUNC_2:def 6
( a₂ is independent & a₂ is generating );

end;

:: deftheorem Def6 defines is_a_coordinate BVFUNC_2:def 6 :

definition

let c₁ be non empty set ;
let c₂ be a_partition of c₁;
redefine func { as {c₂} -> Subset of (PARTITIONS a₁);
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be a_partition of c₁;
let c₃ be Subset of (PARTITIONS c₁);
func CompF c₂,c₃ -> a_partition of a₁ equals :: BVFUNC_2:def 7
'/\' (a₃ \ {a₂});
correctness ;

end;

:: deftheorem Def7 defines CompF BVFUNC_2:def 7 :

definition

let c₁ be non empty set ;
let c₂ be Element of Funcs c₁,BOOLEAN ;
let c₃ be Subset of (PARTITIONS c₁);
let c₄ be a_partition of c₁;
pred c₂ is_independent_of c₄,c₃ means :Def8: :: BVFUNC_2:def 8
a₂ is_dependent_of CompF a₄,a₃;

end;

:: deftheorem Def8 defines is_independent_of BVFUNC_2:def 8 :

definition

let c₁ be non empty set ;
let c₂ be Element of Funcs c₁,BOOLEAN ;
let c₃ be Subset of (PARTITIONS c₁);
let c₄ be a_partition of c₁;
func All c₂,c₄,c₃ -> Element of Funcs a₁,BOOLEAN equals :: BVFUNC_2:def 9
B_INF a₂,(CompF a₄,a₃);
correctness ;

end;

:: deftheorem Def9 defines All BVFUNC_2:def 9 :

definition

let c₁ be non empty set ;
let c₂ be Element of Funcs c₁,BOOLEAN ;
let c₃ be Subset of (PARTITIONS c₁);
let c₄ be a_partition of c₁;
func Ex c₂,c₄,c₃ -> Element of Funcs a₁,BOOLEAN equals :: BVFUNC_2:def 10
B_SUP a₂,(CompF a₄,a₃);
correctness ;

end;

:: deftheorem Def10 defines Ex BVFUNC_2:def 10 :

theorem Th5: :: BVFUNC_2:5

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds All b₃,b₄,b₂ is_dependent_of CompF b₄,b₂

proof end;

theorem Th6: :: BVFUNC_2:6

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds Ex b₃,b₄,b₂ is_dependent_of CompF b₄,b₂

proof end;

theorem Th7: :: BVFUNC_2:7

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds All (I_el b₁),b₄,b₂ = I_el b₁

proof end;

theorem Th8: :: BVFUNC_2:8

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds Ex (I_el b₁),b₄,b₂ = I_el b₁

proof end;

theorem Th9: :: BVFUNC_2:9

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds All (O_el b₁),b₄,b₂ = O_el b₁

proof end;

theorem Th10: :: BVFUNC_2:10

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds Ex (O_el b₁),b₄,b₂ = O_el b₁

proof end;

theorem Th11: :: BVFUNC_2:11

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds All b₃,b₄,b₂ '<' b₃

proof end;

theorem Th12: :: BVFUNC_2:12

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds b₃ '<' Ex b₃,b₄,b₂

proof end;

theorem Th13: :: BVFUNC_2:13

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ holds All (b₃ '&' b₄),b₅,b₂ = (All b₃,b₅,b₂) '&' (All b₄,b₅,b₂) by BVFUNC_1:42;

theorem Th14: :: BVFUNC_2:14

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ holds (All b₃,b₅,b₂) 'or' (All b₄,b₅,b₂) '<' All (b₃ 'or' b₄),b₅,b₂

proof end;

theorem Th15: :: BVFUNC_2:15

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ holds All (b₃ 'imp' b₄),b₅,b₂ '<' (All b₃,b₅,b₂) 'imp' (All b₄,b₅,b₂)

proof end;

theorem Th16: :: BVFUNC_2:16

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ holds Ex (b₃ 'or' b₄),b₅,b₂ = (Ex b₃,b₅,b₂) 'or' (Ex b₄,b₅,b₂) by BVFUNC_1:43;

theorem Th17: :: BVFUNC_2:17

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being Subset of (PARTITIONS b₁)
for b₅ being a_partition of b₁ holds Ex (b₂ '&' b₃),b₅,b₄ '<' (Ex b₂,b₅,b₄) '&' (Ex b₃,b₅,b₄)

proof end;

theorem Th18: :: BVFUNC_2:18

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ holds (Ex b₃,b₅,b₂) 'xor' (Ex b₄,b₅,b₂) '<' Ex (b₃ 'xor' b₄),b₅,b₂

proof end;

theorem Th19: :: BVFUNC_2:19

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ holds (Ex b₃,b₅,b₂) 'imp' (Ex b₄,b₅,b₂) '<' Ex (b₃ 'imp' b₄),b₅,b₂

proof end;

theorem Th20: :: BVFUNC_2:20

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds 'not' (All b₃,b₄,b₂) = Ex ('not' b₃),b₄,b₂

proof end;

theorem Th21: :: BVFUNC_2:21

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds 'not' (Ex b₃,b₄,b₂) = All ('not' b₃),b₄,b₂

proof end;

theorem Th22: :: BVFUNC_2:22

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
All (b₃ 'imp' b₄),b₅,b₂ = b₃ 'imp' (All b₄,b₅,b₂)

proof end;

theorem Th23: :: BVFUNC_2:23

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
All (b₄ 'imp' b₃),b₅,b₂ = (Ex b₄,b₅,b₂) 'imp' b₃

proof end;

theorem Th24: :: BVFUNC_2:24

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
All (b₃ 'or' b₄),b₅,b₂ = b₃ 'or' (All b₄,b₅,b₂)

proof end;

theorem Th25: :: BVFUNC_2:25

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
All (b₄ 'or' b₃),b₅,b₂ = (All b₄,b₅,b₂) 'or' b₃ by Th24;

theorem Th26: :: BVFUNC_2:26

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
All (b₄ 'or' b₃),b₅,b₂ '<' (Ex b₄,b₅,b₂) 'or' b₃

proof end;

theorem Th27: :: BVFUNC_2:27

proof end;

theorem Th28: :: BVFUNC_2:28

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
All (b₄ '&' b₃),b₅,b₂ = (All b₄,b₅,b₂) '&' b₃ by Th27;

theorem Th29: :: BVFUNC_2:29

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ holds All (b₃ '&' b₄),b₅,b₂ '<' (Ex b₃,b₅,b₂) '&' b₄

proof end;

theorem Th30: :: BVFUNC_2:30

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
All (b₃ 'xor' b₄),b₅,b₂ '<' b₃ 'xor' (All b₄,b₅,b₂)

proof end;

theorem Th31: :: BVFUNC_2:31

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
All (b₄ 'xor' b₃),b₅,b₂ '<' (All b₄,b₅,b₂) 'xor' b₃ by Th30;

theorem Th32: :: BVFUNC_2:32

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
All (b₃ 'eqv' b₄),b₅,b₂ '<' b₃ 'eqv' (All b₄,b₅,b₂)

proof end;

theorem Th33: :: BVFUNC_2:33

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
All (b₄ 'eqv' b₃),b₅,b₂ '<' (All b₄,b₅,b₂) 'eqv' b₃ by Th32;

theorem Th34: :: BVFUNC_2:34

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
Ex (b₃ 'or' b₄),b₅,b₂ = b₃ 'or' (Ex b₄,b₅,b₂)

proof end;

theorem Th35: :: BVFUNC_2:35

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
Ex (b₄ 'or' b₃),b₅,b₂ = (Ex b₄,b₅,b₂) 'or' b₃ by Th34;

theorem Th36: :: BVFUNC_2:36

proof end;

theorem Th37: :: BVFUNC_2:37

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
Ex (b₄ '&' b₃),b₅,b₂ = (Ex b₄,b₅,b₂) '&' b₃ by Th36;

theorem Th38: :: BVFUNC_2:38

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ holds b₃ 'imp' (Ex b₄,b₅,b₂) '<' Ex (b₃ 'imp' b₄),b₅,b₂

proof end;

theorem Th39: :: BVFUNC_2:39

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ holds (Ex b₃,b₅,b₂) 'imp' b₄ '<' Ex (b₃ 'imp' b₄),b₅,b₂

proof end;

theorem Th40: :: BVFUNC_2:40

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
b₃ 'xor' (Ex b₄,b₅,b₂) '<' Ex (b₃ 'xor' b₄),b₅,b₂

proof end;

theorem Th41: :: BVFUNC_2:41

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being Element of Funcs b₁,BOOLEAN
for b₅ being a_partition of b₁ st b₃ is_independent_of b₅,b₂ holds
(Ex b₄,b₅,b₂) 'xor' b₃ '<' Ex (b₄ 'xor' b₃),b₅,b₂ by Th40;