:: BVFUNC_1 semantic presentation

definition

let c₁, c₂ be boolean set ;
func c₁ 'imp' c₂ -> set equals :: BVFUNC_1:def 1
('not' a₁) 'or' a₂;
correctness ;
func c₁ 'eqv' c₂ -> set equals :: BVFUNC_1:def 2
'not' (a₁ 'xor' a₂);
correctness ;
commutativity ;

end;

:: deftheorem Def1 defines 'imp' BVFUNC_1:def 1 :

:: deftheorem Def2 defines 'eqv' BVFUNC_1:def 2 :

registration

let c₁, c₂ be boolean set ;
cluster a₁ 'imp' a₂ -> boolean ;
correctness ;
cluster a₁ 'eqv' a₂ -> boolean ;
correctness ;

end;

registration

cluster boolean -> natural set ;
coherence

proof end;

end;

notation

let c₁, c₂ be boolean set ;
synonym c₁ '<' c₂ for c₁ <= c₂;

end;

definition

let c₁, c₂ be boolean set ;
redefine pred c₁ <= c₂ means :Def3: :: BVFUNC_1:def 3
a₁ 'imp' a₂ = TRUE ;
compatibility

proof end;

end;

:: deftheorem Def3 defines '<' BVFUNC_1:def 3 :

definition

let c₁ be set ;
func BVF c₁ -> set equals :: BVFUNC_1:def 4
Funcs a₁,BOOLEAN ;
correctness ;

end;

:: deftheorem Def4 defines BVF BVFUNC_1:def 4 :

registration

let c₁ be set ;
cluster BVF a₁ -> non empty functional ;
coherence ;

end;

registration

let c₁ be set ;
cluster -> boolean-valued Element of BVF a₁;
coherence

proof end;

end;

notation

let c₁ be boolean-valued Function;
let c₂ be set ;
synonym Pj c₁,c₂ for c₁ . c₂;

end;

scheme :: BVFUNC_1:sch 1
s1{ F₁() -> non empty set , F₂() -> Element of Funcs F₁(),BOOLEAN , F₃() -> Element of Funcs F₁(),BOOLEAN , F₄( set , Element of Funcs F₁(),BOOLEAN , Element of Funcs F₁(),BOOLEAN ) -> set } :

for b₁, b₂ being Element of Funcs F₁(),BOOLEAN st ( for b₃ being Element of F₁() holds Pj b₁,b₃ = F₄(b₃,F₂(),F₃()) ) & ( for b₃ being Element of F₁() holds Pj b₂,b₃ = F₄(b₃,F₂(),F₃()) ) holds
b₁ = b₂

proof end;

scheme :: BVFUNC_1:sch 2
s2{ F₁() -> non empty set , F₂( set ) -> set } :

for b₁, b₂ being Element of Funcs F₁(),BOOLEAN st ( for b₃ being Element of F₁() holds Pj b₁,b₃ = F₂(b₃) ) & ( for b₃ being Element of F₁() holds Pj b₂,b₃ = F₂(b₃) ) holds
b₁ = b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of BVF c₁;
redefine func 'not' as 'not' c₂ -> Element of BVF a₁;
coherence

proof end;

let c₃ be Element of BVF c₁;
redefine func '&' as c₂ '&' c₃ -> Element of BVF a₁;
coherence

proof end;

end;

definition

let c₁, c₂ be boolean-valued Function;
func c₁ 'or' c₂ -> Function means :Def5: :: BVFUNC_1:def 5
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) 'or' (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;
func c₁ 'xor' c₂ -> Function means :Def6: :: BVFUNC_1:def 6
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) 'xor' (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def5 defines 'or' BVFUNC_1:def 5 :

:: deftheorem Def6 defines 'xor' BVFUNC_1:def 6 :

registration

let c₁, c₂ be boolean-valued Function;
cluster a₁ 'or' a₂ -> boolean-valued ;
coherence

proof end;

cluster a₁ 'xor' a₂ -> boolean-valued ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of Funcs c₁,BOOLEAN ;
redefine func 'or' as c₂ 'or' c₃ -> Element of Funcs a₁,BOOLEAN means :Def7: :: BVFUNC_1:def 7
for b₁ being Element of a₁ holds a₄ . b₁ = (a₂ . b₁) 'or' (a₃ . b₁);
coherence

proof end;

compatibility

proof end;

redefine func 'xor' as c₂ 'xor' c₃ -> Element of Funcs a₁,BOOLEAN means :: BVFUNC_1:def 8
for b₁ being Element of a₁ holds a₄ . b₁ = (a₂ . b₁) 'xor' (a₃ . b₁);
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def7 defines 'or' BVFUNC_1:def 7 :

:: deftheorem Def8 defines 'xor' BVFUNC_1:def 8 :

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of BVF c₁;
redefine func 'or' as c₂ 'or' c₃ -> Element of BVF a₁;
coherence

proof end;

redefine func 'xor' as c₂ 'xor' c₃ -> Element of BVF a₁;
coherence

proof end;

end;

definition

let c₁, c₂ be boolean-valued Function;
func c₁ 'imp' c₂ -> Function means :Def9: :: BVFUNC_1:def 9
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) 'imp' (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

func c₁ 'eqv' c₂ -> Function means :Def10: :: BVFUNC_1:def 10
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) 'eqv' (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def9 defines 'imp' BVFUNC_1:def 9 :

:: deftheorem Def10 defines 'eqv' BVFUNC_1:def 10 :

registration

let c₁, c₂ be boolean-valued Function;
cluster a₁ 'imp' a₂ -> boolean-valued ;
coherence

proof end;

cluster a₁ 'eqv' a₂ -> boolean-valued ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of Funcs c₁,BOOLEAN ;
redefine func 'imp' as c₂ 'imp' c₃ -> Element of Funcs a₁,BOOLEAN means :Def11: :: BVFUNC_1:def 11
for b₁ being Element of a₁ holds a₄ . b₁ = ('not' (Pj a₂,b₁)) 'or' (Pj a₃,b₁);
coherence

proof end;

compatibility

proof end;

redefine func 'eqv' as c₂ 'eqv' c₃ -> Element of Funcs a₁,BOOLEAN means :Def12: :: BVFUNC_1:def 12
for b₁ being Element of a₁ holds a₄ . b₁ = 'not' ((Pj a₂,b₁) 'xor' (Pj a₃,b₁));
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def11 defines 'imp' BVFUNC_1:def 11 :

:: deftheorem Def12 defines 'eqv' BVFUNC_1:def 12 :

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of BVF c₁;
redefine func 'imp' as c₂ 'imp' c₃ -> Element of BVF a₁;
coherence

proof end;

redefine func 'eqv' as c₂ 'eqv' c₃ -> Element of BVF a₁;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
func O_el c₁ -> Element of Funcs a₁,BOOLEAN means :Def13: :: BVFUNC_1:def 13
for b₁ being Element of a₁ holds Pj a₂,b₁ = FALSE ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines O_el BVFUNC_1:def 13 :

definition

let c₁ be non empty set ;
func I_el c₁ -> Element of Funcs a₁,BOOLEAN means :Def14: :: BVFUNC_1:def 14
for b₁ being Element of a₁ holds Pj a₂,b₁ = TRUE ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines I_el BVFUNC_1:def 14 :

theorem Th1: :: BVFUNC_1:1

canceled;

theorem Th2: :: BVFUNC_1:2

canceled;

theorem Th3: :: BVFUNC_1:3

canceled;

theorem Th4: :: BVFUNC_1:4

for b₁ being boolean-valued Function holds 'not' ('not' b₁) = b₁

proof end;

theorem Th5: :: BVFUNC_1:5

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds
( 'not' (I_el b₁) = O_el b₁ & 'not' (O_el b₁) = I_el b₁ )

proof end;

theorem Th6: :: BVFUNC_1:6

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ '&' b₂ = b₂

proof end;

theorem Th7: :: BVFUNC_1:7

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ '&' b₃) '&' b₄ = b₂ '&' (b₃ '&' b₄)

proof end;

theorem Th8: :: BVFUNC_1:8

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds b₂ '&' (O_el b₁) = O_el b₁

proof end;

theorem Th9: :: BVFUNC_1:9

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds b₂ '&' (I_el b₁) = b₂

proof end;

theorem Th10: :: BVFUNC_1:10

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds b₂ 'or' b₂ = b₂

proof end;

theorem Th11: :: BVFUNC_1:11

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'or' b₃) 'or' b₄ = b₂ 'or' (b₃ 'or' b₄)

proof end;

theorem Th12: :: BVFUNC_1:12

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds b₂ 'or' (O_el b₁) = b₂

proof end;

theorem Th13: :: BVFUNC_1:13

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds b₂ 'or' (I_el b₁) = I_el b₁

proof end;

theorem Th14: :: BVFUNC_1:14

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ '&' b₃) 'or' b₄ = (b₂ 'or' b₄) '&' (b₃ 'or' b₄)

proof end;

theorem Th15: :: BVFUNC_1:15

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'or' b₃) '&' b₄ = (b₂ '&' b₄) 'or' (b₃ '&' b₄)

proof end;

theorem Th16: :: BVFUNC_1:16

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds 'not' (b₂ 'or' b₃) = ('not' b₂) '&' ('not' b₃)

proof end;

theorem Th17: :: BVFUNC_1:17

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds 'not' (b₂ '&' b₃) = ('not' b₂) 'or' ('not' b₃)

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of Funcs c₁,BOOLEAN ;
pred c₂ '<' c₃ means :Def15: :: BVFUNC_1:def 15
for b₁ being Element of a₁ st Pj a₂,b₁ = TRUE holds
Pj a₃,b₁ = TRUE ;
reflexivity ;

end;

:: deftheorem Def15 defines '<' BVFUNC_1:def 15 :

theorem Th18: :: BVFUNC_1:18

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds
( ( b₂ '<' b₃ & b₃ '<' b₂ implies b₂ = b₃ ) & ( b₂ '<' b₃ & b₃ '<' b₄ implies b₂ '<' b₄ ) )

proof end;

theorem Th19: :: BVFUNC_1:19

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds
( b₂ 'imp' b₃ = I_el b₁ iff b₂ '<' b₃ )

proof end;

theorem Th20: :: BVFUNC_1:20

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds
( b₂ 'eqv' b₃ = I_el b₁ iff b₂ = b₃ )

proof end;

theorem Th21: :: BVFUNC_1:21

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds
( O_el b₁ '<' b₂ & b₂ '<' I_el b₁ )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of Funcs c₁,BOOLEAN ;
func B_INF c₂ -> Element of Funcs a₁,BOOLEAN means :Def16: :: BVFUNC_1:def 16
a₃ = I_el a₁ if for b₁ being Element of a₁ holds Pj a₂,b₁ = TRUE
otherwise a₃ = O_el a₁;
correctness ;
func B_SUP c₂ -> Element of Funcs a₁,BOOLEAN means :Def17: :: BVFUNC_1:def 17
a₃ = O_el a₁ if for b₁ being Element of a₁ holds Pj a₂,b₁ = FALSE
otherwise a₃ = I_el a₁;
correctness ;

end;

:: deftheorem Def16 defines B_INF BVFUNC_1:def 16 :

:: deftheorem Def17 defines B_SUP BVFUNC_1:def 17 :

theorem Th22: :: BVFUNC_1:22

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds
( 'not' (B_INF b₂) = B_SUP ('not' b₂) & 'not' (B_SUP b₂) = B_INF ('not' b₂) )

proof end;

theorem Th23: :: BVFUNC_1:23

for b₁ being non empty set holds
( B_INF (O_el b₁) = O_el b₁ & B_INF (I_el b₁) = I_el b₁ & B_SUP (O_el b₁) = O_el b₁ & B_SUP (I_el b₁) = I_el b₁ )

proof end;

registration

let c₁ be non empty set ;
cluster O_el a₁ -> constant ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster I_el a₁ -> constant ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster constant Element of Funcs a₁,BOOLEAN ;
existence

proof end;

end;

theorem Th24: :: BVFUNC_1:24

for b₁ being non empty set
for b₂ being constant Element of Funcs b₁,BOOLEAN holds
( b₂ = O_el b₁ or b₂ = I_el b₁ )

proof end;

theorem Th25: :: BVFUNC_1:25

for b₁ being non empty set
for b₂ being constant Element of Funcs b₁,BOOLEAN holds
( B_INF b₂ = b₂ & B_SUP b₂ = b₂ )

proof end;

theorem Th26: :: BVFUNC_1:26

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds
( B_INF (b₂ '&' b₃) = (B_INF b₂) '&' (B_INF b₃) & B_SUP (b₂ 'or' b₃) = (B_SUP b₂) 'or' (B_SUP b₃) )

proof end;

theorem Th27: :: BVFUNC_1:27

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN
for b₃ being constant Element of Funcs b₁,BOOLEAN holds
( B_INF (b₃ 'imp' b₂) = b₃ 'imp' (B_INF b₂) & B_INF (b₂ 'imp' b₃) = (B_SUP b₂) 'imp' b₃ )

proof end;

theorem Th28: :: BVFUNC_1:28

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN
for b₃ being constant Element of Funcs b₁,BOOLEAN holds
( B_INF (b₃ 'or' b₂) = b₃ 'or' (B_INF b₂) & B_SUP (b₃ '&' b₂) = b₃ '&' (B_SUP b₂) & B_SUP (b₂ '&' b₃) = (B_SUP b₂) '&' b₃ )

proof end;

theorem Th29: :: BVFUNC_1:29

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN
for b₃ being Element of b₁ holds Pj (B_INF b₂),b₃ '<' Pj b₂,b₃

proof end;

theorem Th30: :: BVFUNC_1:30

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN
for b₃ being Element of b₁ holds Pj b₂,b₃ '<' Pj (B_SUP b₂),b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of Funcs c₁,BOOLEAN ;
let c₃ be a_partition of c₁;
pred c₂ is_dependent_of c₃ means :Def18: :: BVFUNC_1:def 18
for b₁ being set st b₁ in a₃ holds
for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
a₂ . b₂ = a₂ . b₃;

end;

:: deftheorem Def18 defines is_dependent_of BVFUNC_1:def 18 :

theorem Th31: :: BVFUNC_1:31

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds b₂ is_dependent_of %I b₁

proof end;

theorem Th32: :: BVFUNC_1:32

for b₁ being non empty set
for b₂ being constant Element of Funcs b₁,BOOLEAN holds b₂ is_dependent_of %O b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be a_partition of c₁;
redefine mode Element as Element of c₂ -> Subset of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be a_partition of c₁;
redefine func EqClass as EqClass c₂,c₃ -> Element of a₃;
coherence by T_1TOPSP:def 1;

end;

definition

let c₁ be non empty set ;
let c₂ be Element of Funcs c₁,BOOLEAN ;
let c₃ be a_partition of c₁;
func B_INF c₂,c₃ -> Element of Funcs a₁,BOOLEAN means :Def19: :: BVFUNC_1:def 19
for b₁ being Element of a₁ holds
( ( ( for b₂ being Element of a₁ st b₂ in EqClass b₁,a₃ holds
Pj a₂,b₂ = TRUE ) implies Pj a₄,b₁ = TRUE ) & ( ex b₂ being Element of a₁ st
( b₂ in EqClass b₁,a₃ & not Pj a₂,b₂ = TRUE ) implies Pj a₄,b₁ = FALSE ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines B_INF BVFUNC_1:def 19 :

definition

let c₁ be non empty set ;
let c₂ be Element of Funcs c₁,BOOLEAN ;
let c₃ be a_partition of c₁;
func B_SUP c₂,c₃ -> Element of Funcs a₁,BOOLEAN means :Def20: :: BVFUNC_1:def 20
for b₁ being Element of a₁ holds
( ( ex b₂ being Element of a₁ st
( b₂ in EqClass b₁,a₃ & Pj a₂,b₂ = TRUE ) implies Pj a₄,b₁ = TRUE ) & ( ( for b₂ being Element of a₁ holds
( not b₂ in EqClass b₁,a₃ or not Pj a₂,b₂ = TRUE ) ) implies Pj a₄,b₁ = FALSE ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines B_SUP BVFUNC_1:def 20 :

theorem Th33: :: BVFUNC_1:33

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN
for b₃ being a_partition of b₁ holds B_INF b₂,b₃ is_dependent_of b₃

proof end;

theorem Th34: :: BVFUNC_1:34

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN
for b₃ being a_partition of b₁ holds B_SUP b₂,b₃ is_dependent_of b₃

proof end;

theorem Th35: :: BVFUNC_1:35

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN
for b₃ being a_partition of b₁ holds B_INF b₂,b₃ '<' b₂

proof end;

theorem Th36: :: BVFUNC_1:36

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN
for b₃ being a_partition of b₁ holds b₂ '<' B_SUP b₂,b₃

proof end;

theorem Th37: :: BVFUNC_1:37

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN
for b₃ being a_partition of b₁ holds 'not' (B_INF b₂,b₃) = B_SUP ('not' b₂),b₃

proof end;

theorem Th38: :: BVFUNC_1:38

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds B_INF b₂,(%O b₁) = B_INF b₂

proof end;

theorem Th39: :: BVFUNC_1:39

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds B_SUP b₂,(%O b₁) = B_SUP b₂

proof end;

theorem Th40: :: BVFUNC_1:40

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds B_INF b₂,(%I b₁) = b₂

proof end;

theorem Th41: :: BVFUNC_1:41

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds B_SUP b₂,(%I b₁) = b₂

proof end;

theorem Th42: :: BVFUNC_1:42

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds B_INF (b₂ '&' b₃),b₄ = (B_INF b₂,b₄) '&' (B_INF b₃,b₄)

proof end;

theorem Th43: :: BVFUNC_1:43

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN
for b₄ being a_partition of b₁ holds B_SUP (b₂ 'or' b₃),b₄ = (B_SUP b₂,b₄) 'or' (B_SUP b₃,b₄)

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of Funcs c₁,BOOLEAN ;
func GPart c₂ -> a_partition of a₁ equals :: BVFUNC_1:def 21
{{ b₁ where B is Element of a₁ : a₂ . b₁ = TRUE } ,{ b₁ where B is Element of a₁ : a₂ . b₁ = FALSE } } \ {{} };
correctness

proof end;

end;

:: deftheorem Def21 defines GPart BVFUNC_1:def 21 :

theorem Th44: :: BVFUNC_1:44

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds b₂ is_dependent_of GPart b₂

proof end;

theorem Th45: :: BVFUNC_1:45

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN
for b₃ being a_partition of b₁ st b₂ is_dependent_of b₃ holds
b₃ is_finer_than GPart b₂

proof end;