:: A Theory of Boolean Valued Functions and Partitions
:: by Shunichi Kobayashi and Kui Jia
::
:: Received October 22, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

definition
let k, l be boolean set ;
redefine pred k <= l means :Def1: :: BVFUNC_1:def 1
k => l = TRUE ;
compatibility
( k <= l iff k => l = TRUE )
proof end;
end;

:: deftheorem Def1 defines <= BVFUNC_1:def 1 :
for k, l being boolean set holds
( k <= l iff k => l = TRUE );

begin

scheme :: BVFUNC_1:sch 1
BVFUniq1{ F1() -> non empty set , F2( set ) -> set } :
for f1, f2 being Function of F1(),BOOLEAN st ( for x being Element of F1() holds f1 . x = F2(x) ) & ( for x being Element of F1() holds f2 . x = F2(x) ) holds
f1 = f2
proof end;

definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
:: original: 'not'
redefine func 'not' a -> Function of Y,BOOLEAN;
coherence
'not' a is Function of Y,BOOLEAN
proof end;
let b be Function of Y,BOOLEAN;
:: original: '&'
redefine func a '&' b -> Function of Y,BOOLEAN;
coherence
a '&' b is Function of Y,BOOLEAN
proof end;
end;

definition
let p, q be boolean-valued Function;
func p 'or' q -> boolean-valued Function means :Def2: :: BVFUNC_1:def 2
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) 'or' (q . x) ) );
existence
ex b1 being boolean-valued Function st
( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'or' (q . x) ) )
proof end;
uniqueness
for b1, b2 being boolean-valued Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'or' (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds
b2 . x = (p . x) 'or' (q . x) ) holds
b1 = b2
proof end;
commutativity
for b1, p, q being boolean-valued Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'or' (q . x) ) holds
( dom b1 = (dom q) /\ (dom p) & ( for x being set st x in dom b1 holds
b1 . x = (q . x) 'or' (p . x) ) )
;
idempotence
for p being boolean-valued Function holds
( dom p = (dom p) /\ (dom p) & ( for x being set st x in dom p holds
p . x = (p . x) 'or' (p . x) ) )
;
func p 'xor' q -> Function means :Def3: :: BVFUNC_1:def 3
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) 'xor' (q . x) ) );
existence
ex b1 being Function st
( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'xor' (q . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'xor' (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds
b2 . x = (p . x) 'xor' (q . x) ) holds
b1 = b2
proof end;
commutativity
for b1 being Function
for p, q being boolean-valued Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'xor' (q . x) ) holds
( dom b1 = (dom q) /\ (dom p) & ( for x being set st x in dom b1 holds
b1 . x = (q . x) 'xor' (p . x) ) )
;
end;

:: deftheorem Def2 defines 'or' BVFUNC_1:def 2 :
for p, q, b3 being boolean-valued Function holds
( b3 = p 'or' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) 'or' (q . x) ) ) );

:: deftheorem Def3 defines 'xor' BVFUNC_1:def 3 :
for p, q being boolean-valued Function
for b3 being Function holds
( b3 = p 'xor' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) 'xor' (q . x) ) ) );

registration
let p, q be boolean-valued Function;
cluster p 'xor' q -> boolean-valued ;
coherence
p 'xor' q is boolean-valued
proof end;
end;

definition
let A be non empty set ;
let p, q be Function of A,BOOLEAN;
:: original: 'or'
redefine func p 'or' q -> Function of A,BOOLEAN means :Def4: :: BVFUNC_1:def 4
for x being Element of A holds it . x = (p . x) 'or' (q . x);
coherence
p 'or' q is Function of A,BOOLEAN
proof end;
compatibility
for b1 being Function of A,BOOLEAN holds
( b1 = p 'or' q iff for x being Element of A holds b1 . x = (p . x) 'or' (q . x) )
proof end;
:: original: 'xor'
redefine func p 'xor' q -> Function of A,BOOLEAN means :: BVFUNC_1:def 5
for x being Element of A holds it . x = (p . x) 'xor' (q . x);
coherence
p 'xor' q is Function of A,BOOLEAN
proof end;
compatibility
for b1 being Function of A,BOOLEAN holds
( b1 = p 'xor' q iff for x being Element of A holds b1 . x = (p . x) 'xor' (q . x) )
proof end;
end;

:: deftheorem Def4 defines 'or' BVFUNC_1:def 4 :
for A being non empty set
for p, q, b4 being Function of A,BOOLEAN holds
( b4 = p 'or' q iff for x being Element of A holds b4 . x = (p . x) 'or' (q . x) );

:: deftheorem defines 'xor' BVFUNC_1:def 5 :
for A being non empty set
for p, q, b4 being Function of A,BOOLEAN holds
( b4 = p 'xor' q iff for x being Element of A holds b4 . x = (p . x) 'xor' (q . x) );

definition
let p, q be boolean-valued Function;
func p 'imp' q -> Function means :Def6: :: BVFUNC_1:def 6
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) => (q . x) ) );
existence
ex b1 being Function st
( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) => (q . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) => (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds
b2 . x = (p . x) => (q . x) ) holds
b1 = b2
proof end;
func p 'eqv' q -> Function means :Def7: :: BVFUNC_1:def 7
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) <=> (q . x) ) );
existence
ex b1 being Function st
( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) <=> (q . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) <=> (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds
b2 . x = (p . x) <=> (q . x) ) holds
b1 = b2
proof end;
commutativity
for b1 being Function
for p, q being boolean-valued Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) <=> (q . x) ) holds
( dom b1 = (dom q) /\ (dom p) & ( for x being set st x in dom b1 holds
b1 . x = (q . x) <=> (p . x) ) )
;
end;

:: deftheorem Def6 defines 'imp' BVFUNC_1:def 6 :
for p, q being boolean-valued Function
for b3 being Function holds
( b3 = p 'imp' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) => (q . x) ) ) );

:: deftheorem Def7 defines 'eqv' BVFUNC_1:def 7 :
for p, q being boolean-valued Function
for b3 being Function holds
( b3 = p 'eqv' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) <=> (q . x) ) ) );

registration
let p, q be boolean-valued Function;
cluster p 'imp' q -> boolean-valued ;
coherence
p 'imp' q is boolean-valued
proof end;
cluster p 'eqv' q -> boolean-valued ;
coherence
p 'eqv' q is boolean-valued
proof end;
end;

definition
let A be non empty set ;
let p, q be Function of A,BOOLEAN;
:: original: 'imp'
redefine func p 'imp' q -> Function of A,BOOLEAN means :Def8: :: BVFUNC_1:def 8
for x being Element of A holds it . x = ('not' (p . x)) 'or' (q . x);
coherence
p 'imp' q is Function of A,BOOLEAN
proof end;
compatibility
for b1 being Function of A,BOOLEAN holds
( b1 = p 'imp' q iff for x being Element of A holds b1 . x = ('not' (p . x)) 'or' (q . x) )
proof end;
:: original: 'eqv'
redefine func p 'eqv' q -> Function of A,BOOLEAN means :Def9: :: BVFUNC_1:def 9
for x being Element of A holds it . x = 'not' ((p . x) 'xor' (q . x));
coherence
p 'eqv' q is Function of A,BOOLEAN
proof end;
compatibility
for b1 being Function of A,BOOLEAN holds
( b1 = p 'eqv' q iff for x being Element of A holds b1 . x = 'not' ((p . x) 'xor' (q . x)) )
proof end;
end;

:: deftheorem Def8 defines 'imp' BVFUNC_1:def 8 :
for A being non empty set
for p, q, b4 being Function of A,BOOLEAN holds
( b4 = p 'imp' q iff for x being Element of A holds b4 . x = ('not' (p . x)) 'or' (q . x) );

:: deftheorem Def9 defines 'eqv' BVFUNC_1:def 9 :
for A being non empty set
for p, q, b4 being Function of A,BOOLEAN holds
( b4 = p 'eqv' q iff for x being Element of A holds b4 . x = 'not' ((p . x) 'xor' (q . x)) );

definition
let Y be non empty set ;
func O_el Y -> Function of Y,BOOLEAN means :Def10: :: BVFUNC_1:def 10
for x being Element of Y holds it . x = FALSE ;
existence
ex b1 being Function of Y,BOOLEAN st
for x being Element of Y holds b1 . x = FALSE
proof end;
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for x being Element of Y holds b1 . x = FALSE ) & ( for x being Element of Y holds b2 . x = FALSE ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines O_el BVFUNC_1:def 10 :
for Y being non empty set
for b2 being Function of Y,BOOLEAN holds
( b2 = O_el Y iff for x being Element of Y holds b2 . x = FALSE );

definition
let Y be non empty set ;
func I_el Y -> Function of Y,BOOLEAN means :Def11: :: BVFUNC_1:def 11
for x being Element of Y holds it . x = TRUE ;
existence
ex b1 being Function of Y,BOOLEAN st
for x being Element of Y holds b1 . x = TRUE
proof end;
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for x being Element of Y holds b1 . x = TRUE ) & ( for x being Element of Y holds b2 . x = TRUE ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines I_el BVFUNC_1:def 11 :
for Y being non empty set
for b2 being Function of Y,BOOLEAN holds
( b2 = I_el Y iff for x being Element of Y holds b2 . x = TRUE );

theorem :: BVFUNC_1:1
canceled;

theorem Th2: :: BVFUNC_1:2
for Y being non empty set holds
( 'not' (I_el Y) = O_el Y & 'not' (O_el Y) = I_el Y )
proof end;

theorem :: BVFUNC_1:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' a = a ;

theorem :: BVFUNC_1:4
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) '&' c = a '&' (b '&' c)
proof end;

theorem Th5: :: BVFUNC_1:5
for Y being non empty set
for a being Function of Y,BOOLEAN holds a '&' (O_el Y) = O_el Y
proof end;

theorem Th6: :: BVFUNC_1:6
for Y being non empty set
for a being Function of Y,BOOLEAN holds a '&' (I_el Y) = a
proof end;

theorem :: BVFUNC_1:7
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'or' a = a ;

theorem :: BVFUNC_1:8
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'or' c = a 'or' (b 'or' c)
proof end;

theorem Th9: :: BVFUNC_1:9
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'or' (O_el Y) = a
proof end;

theorem Th10: :: BVFUNC_1:10
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'or' (I_el Y) = I_el Y
proof end;

theorem :: BVFUNC_1:11
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'or' c = (a 'or' c) '&' (b 'or' c)
proof end;

theorem :: BVFUNC_1:12
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' c = (a '&' c) 'or' (b '&' c)
proof end;

theorem :: BVFUNC_1:13
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'or' b) = ('not' a) '&' ('not' b)
proof end;

theorem :: BVFUNC_1:14
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a '&' b) = ('not' a) 'or' ('not' b)
proof end;

definition
let Y be non empty set ;
let a, b be Function of Y,BOOLEAN;
pred a '<' b means :Def12: :: BVFUNC_1:def 12
for x being Element of Y st a . x = TRUE holds
b . x = TRUE ;
reflexivity
for a being Function of Y,BOOLEAN
for x being Element of Y st a . x = TRUE holds
a . x = TRUE
;
end;

:: deftheorem Def12 defines '<' BVFUNC_1:def 12 :
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a '<' b iff for x being Element of Y st a . x = TRUE holds
b . x = TRUE );

theorem :: BVFUNC_1:15
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds
( ( a '<' b & b '<' a implies a = b ) & ( a '<' b & b '<' c implies a '<' c ) )
proof end;

theorem Th16: :: BVFUNC_1:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'imp' b = I_el Y iff a '<' b )
proof end;

theorem :: BVFUNC_1:17
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff a = b )
proof end;

theorem :: BVFUNC_1:18
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( O_el Y '<' a & a '<' I_el Y )
proof end;

begin

definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
func B_INF a -> Function of Y,BOOLEAN equals :Def13: :: BVFUNC_1:def 13
I_el Y if for x being Element of Y holds a . x = TRUE
otherwise O_el Y;
correctness
coherence
( ( ( for x being Element of Y holds a . x = TRUE ) implies I_el Y is Function of Y,BOOLEAN ) & ( not for x being Element of Y holds a . x = TRUE implies O_el Y is Function of Y,BOOLEAN ) )
;
consistency
for b1 being Function of Y,BOOLEAN holds verum
;
;
func B_SUP a -> Function of Y,BOOLEAN equals :Def14: :: BVFUNC_1:def 14
O_el Y if for x being Element of Y holds a . x = FALSE
otherwise I_el Y;
correctness
coherence
( ( ( for x being Element of Y holds a . x = FALSE ) implies O_el Y is Function of Y,BOOLEAN ) & ( not for x being Element of Y holds a . x = FALSE implies I_el Y is Function of Y,BOOLEAN ) )
;
consistency
for b1 being Function of Y,BOOLEAN holds verum
;
;
end;

:: deftheorem Def13 defines B_INF BVFUNC_1:def 13 :
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = TRUE ) implies B_INF a = I_el Y ) & ( not for x being Element of Y holds a . x = TRUE implies B_INF a = O_el Y ) );

:: deftheorem Def14 defines B_SUP BVFUNC_1:def 14 :
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = FALSE ) implies B_SUP a = O_el Y ) & ( not for x being Element of Y holds a . x = FALSE implies B_SUP a = I_el Y ) );

theorem Th19: :: BVFUNC_1:19
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
proof end;

theorem :: BVFUNC_1:20
for Y being non empty set holds
( B_INF (O_el Y) = O_el Y & B_INF (I_el Y) = I_el Y & B_SUP (O_el Y) = O_el Y & B_SUP (I_el Y) = I_el Y )
proof end;

registration
let Y be non empty set ;
cluster O_el Y -> constant ;
coherence
O_el Y is constant
proof end;
end;

registration
let Y be non empty set ;
cluster I_el Y -> constant ;
coherence
I_el Y is constant
proof end;
end;

registration
let Y be non empty set ;
cluster non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V21(Y) quasi_total boolean-valued for Element of bool [:Y,BOOLEAN:];
existence
ex b1 being Function of Y,BOOLEAN st b1 is constant
proof end;
end;

theorem Th21: :: BVFUNC_1:21
for Y being non empty set
for a being constant Function of Y,BOOLEAN holds
( a = O_el Y or a = I_el Y )
proof end;

theorem Th22: :: BVFUNC_1:22
for Y being non empty set
for d being constant Function of Y,BOOLEAN holds
( B_INF d = d & B_SUP d = d )
proof end;

theorem :: BVFUNC_1:23
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
proof end;

theorem :: BVFUNC_1:24
for Y being non empty set
for a being Function of Y,BOOLEAN
for d being constant Function of Y,BOOLEAN holds
( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
proof end;

theorem :: BVFUNC_1:25
for Y being non empty set
for a being Function of Y,BOOLEAN
for d being constant Function of Y,BOOLEAN holds
( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
proof end;

theorem :: BVFUNC_1:26
for Y being non empty set
for a being Function of Y,BOOLEAN
for x being Element of Y holds (B_INF a) . x <= a . x
proof end;

theorem :: BVFUNC_1:27
for Y being non empty set
for a being Function of Y,BOOLEAN
for x being Element of Y holds a . x <= (B_SUP a) . x
proof end;

begin

definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
pred a is_dependent_of PA means :Def15: :: BVFUNC_1:def 15
for F being set st F in PA holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2;
end;

:: deftheorem Def15 defines is_dependent_of BVFUNC_1:def 15 :
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds
( a is_dependent_of PA iff for F being set st F in PA holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 );

theorem :: BVFUNC_1:28
for Y being non empty set
for a being Function of Y,BOOLEAN holds a is_dependent_of %I Y
proof end;

theorem :: BVFUNC_1:29
for Y being non empty set
for a being constant Function of Y,BOOLEAN holds a is_dependent_of %O Y
proof end;

definition
let Y be non empty set ;
let PA be a_partition of Y;
:: original: Element
redefine mode Element of PA -> Subset of Y;
coherence
for b1 being Element of PA holds b1 is Subset of Y
proof end;
end;

definition
let Y be non empty set ;
let x be Element of Y;
let PA be a_partition of Y;
:: original: EqClass
redefine func EqClass (x,PA) -> Element of PA;
coherence
EqClass (x,PA) is Element of PA
by EQREL_1:def 6;
end;

definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
func B_INF (a,PA) -> Function of Y,BOOLEAN means :Def16: :: BVFUNC_1:def 16
for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies it . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies it . y = FALSE ) );
existence
ex b1 being Function of Y,BOOLEAN st
for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b1 . y = FALSE ) )
proof end;
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b2 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines B_INF BVFUNC_1:def 16 :
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y
for b4 being Function of Y,BOOLEAN holds
( b4 = B_INF (a,PA) iff for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b4 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b4 . y = FALSE ) ) );

definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
func B_SUP (a,PA) -> Function of Y,BOOLEAN means :Def17: :: BVFUNC_1:def 17
for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies it . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies it . y = FALSE ) );
existence
ex b1 being Function of Y,BOOLEAN st
for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b1 . y = FALSE ) )
proof end;
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b2 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines B_SUP BVFUNC_1:def 17 :
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y
for b4 being Function of Y,BOOLEAN holds
( b4 = B_SUP (a,PA) iff for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b4 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b4 . y = FALSE ) ) );

theorem :: BVFUNC_1:30
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_INF (a,PA) is_dependent_of PA
proof end;

theorem :: BVFUNC_1:31
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_SUP (a,PA) is_dependent_of PA
proof end;

theorem :: BVFUNC_1:32
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_INF (a,PA) '<' a
proof end;

theorem :: BVFUNC_1:33
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds a '<' B_SUP (a,PA)
proof end;

theorem :: BVFUNC_1:34
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (B_INF (a,PA)) = B_SUP (('not' a),PA)
proof end;

theorem :: BVFUNC_1:35
for Y being non empty set
for a being Function of Y,BOOLEAN holds B_INF (a,(%O Y)) = B_INF a
proof end;

theorem :: BVFUNC_1:36
for Y being non empty set
for a being Function of Y,BOOLEAN holds B_SUP (a,(%O Y)) = B_SUP a
proof end;

theorem :: BVFUNC_1:37
for Y being non empty set
for a being Function of Y,BOOLEAN holds B_INF (a,(%I Y)) = a
proof end;

theorem :: BVFUNC_1:38
for Y being non empty set
for a being Function of Y,BOOLEAN holds B_SUP (a,(%I Y)) = a
proof end;

theorem :: BVFUNC_1:39
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_INF ((a '&' b),PA) = (B_INF (a,PA)) '&' (B_INF (b,PA))
proof end;

theorem :: BVFUNC_1:40
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
proof end;

definition
let Y be non empty set ;
let f be Function of Y,BOOLEAN;
func GPart f -> a_partition of Y equals :: BVFUNC_1:def 18
{ { x where x is Element of Y : f . x = TRUE } , { x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{}};
correctness
coherence
{ { x where x is Element of Y : f . x = TRUE } , { x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{}} is a_partition of Y
;
proof end;
end;

:: deftheorem defines GPart BVFUNC_1:def 18 :
for Y being non empty set
for f being Function of Y,BOOLEAN holds GPart f = { { x where x is Element of Y : f . x = TRUE } , { x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{}};

theorem :: BVFUNC_1:41
for Y being non empty set
for a being Function of Y,BOOLEAN holds a is_dependent_of GPart a
proof end;

theorem :: BVFUNC_1:42
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y st a is_dependent_of PA holds
PA is_finer_than GPart a
proof end;

begin

definition
let x, y be Element of BOOLEAN ;
:: original: 'nand'
redefine func x 'nand' y -> Element of BOOLEAN ;
correctness
coherence
x 'nand' y is Element of BOOLEAN
;
proof end;
end;

definition
let x, y be Element of BOOLEAN ;
:: original: 'nor'
redefine func x 'nor' y -> Element of BOOLEAN ;
correctness
coherence
x 'nor' y is Element of BOOLEAN
;
proof end;
end;

definition
let x, y be boolean set ;
redefine func x <=> y equals :: BVFUNC_1:def 19
'not' (x 'xor' y);
correctness
compatibility
for b1 being set holds
( b1 = x <=> y iff b1 = 'not' (x 'xor' y) )
;
;
end;

:: deftheorem defines <=> BVFUNC_1:def 19 :
for x, y being boolean set holds x <=> y = 'not' (x 'xor' y);

definition
let x, y be Element of BOOLEAN ;
:: original: <=>
redefine func x <=> y -> Element of BOOLEAN ;
correctness
coherence
x <=> y is Element of BOOLEAN
;
proof end;
end;

theorem :: BVFUNC_1:43
for x being boolean set holds TRUE 'nand' x = 'not' x ;

theorem :: BVFUNC_1:44
for x being boolean set holds FALSE 'nand' x = TRUE ;

theorem :: BVFUNC_1:45
for x being boolean set holds
( x 'nand' x = 'not' x & 'not' (x 'nand' x) = x ) ;

theorem :: BVFUNC_1:46
for x, y being boolean set holds 'not' (x 'nand' y) = x '&' y ;

theorem :: BVFUNC_1:47
for x being boolean set holds
( x 'nand' ('not' x) = TRUE & 'not' (x 'nand' ('not' x)) = FALSE ) by XBOOLEAN:135, XBOOLEAN:138;

theorem :: BVFUNC_1:48
for x, y, z being boolean set holds x 'nand' (y '&' z) = 'not' ((x '&' y) '&' z) ;

theorem :: BVFUNC_1:49
for x, y, z being boolean set holds x 'nand' (y '&' z) = (x '&' y) 'nand' z ;

theorem :: BVFUNC_1:50
for x being boolean set holds TRUE 'nor' x = FALSE ;

theorem :: BVFUNC_1:51
for x being boolean set holds FALSE 'nor' x = 'not' x ;

theorem :: BVFUNC_1:52
for x being boolean set holds
( x 'nor' x = 'not' x & 'not' (x 'nor' x) = x ) ;

theorem :: BVFUNC_1:53
for x, y being boolean set holds 'not' (x 'nor' y) = x 'or' y ;

theorem :: BVFUNC_1:54
for x being boolean set holds
( x 'nor' ('not' x) = FALSE & 'not' (x 'nor' ('not' x)) = TRUE ) by XBOOLEAN:134, XBOOLEAN:138;

theorem :: BVFUNC_1:55
for x, y, z being boolean set holds x 'nor' (y 'or' z) = 'not' ((x 'or' y) 'or' z) ;

theorem :: BVFUNC_1:56
for x being boolean set holds TRUE <=> x = x ;

theorem :: BVFUNC_1:57
for x being boolean set holds FALSE <=> x = 'not' x ;

theorem :: BVFUNC_1:58
for x being boolean set holds
( x <=> x = TRUE & 'not' (x <=> x) = FALSE ) by XBOOLEAN:125, XBOOLEAN:143;

theorem :: BVFUNC_1:59
for x, y being boolean set holds 'not' (x <=> y) = x 'xor' y ;

theorem :: BVFUNC_1:60
for x being boolean set holds
( x <=> ('not' x) = FALSE & 'not' (x <=> ('not' x)) = TRUE ) by XBOOLEAN:129, XBOOLEAN:142;

theorem :: BVFUNC_1:61
for x, y, z being boolean set holds
( x <= y => z iff x '&' y <= z )
proof end;

theorem :: BVFUNC_1:62
for x, y being boolean set holds x <=> y = (x => y) '&' (y => x) ;

theorem :: BVFUNC_1:63
for x, y being boolean set holds x => y = ('not' y) => ('not' x) ;

theorem :: BVFUNC_1:64
for x, y being boolean set holds x <=> y = ('not' x) <=> ('not' y) ;

theorem :: BVFUNC_1:65
for x, y being boolean set st x = TRUE & x => y = TRUE holds
y = TRUE ;

theorem :: BVFUNC_1:66
for y, x being boolean set st y = TRUE holds
x => y = TRUE ;

theorem :: BVFUNC_1:67
for x, y being boolean set st 'not' x = TRUE holds
x => y = TRUE ;

theorem :: BVFUNC_1:68
for z, y, x being boolean set st z => (y => x) = TRUE holds
y => (z => x) = TRUE ;

theorem :: BVFUNC_1:69
for z, y, x being boolean set st z => (y => x) = TRUE & y = TRUE holds
z => x = TRUE ;

theorem :: BVFUNC_1:70
for z, y, x being boolean set st z => (y => x) = TRUE & y = TRUE & z = TRUE holds
x = TRUE ;