:: by Shunichi Kobayashi and Kui Jia

::

:: Received October 22, 1998

:: Copyright (c) 1998-2012 Association of Mizar Users

begin

:: deftheorem Def1 defines <= BVFUNC_1:def 1 :

for k, l being boolean set holds

( k <= l iff k => l = TRUE );

for k, l being boolean set holds

( k <= l iff k => l = TRUE );

begin

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

:: original: '&'

redefine func a '&' b -> Function of Y,BOOLEAN;

coherence

a '&' b is Function of Y,BOOLEAN

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

definition

let p, q be boolean-valued Function;

ex b_{1} being boolean-valued Function st

( dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) 'or' (q . x) ) )

for b_{1}, b_{2} being boolean-valued Function st dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) 'or' (q . x) ) & dom b_{2} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (p . x) 'or' (q . x) ) holds

b_{1} = b_{2}

for b_{1}, p, q being boolean-valued Function st dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) 'or' (q . x) ) holds

( dom b_{1} = (dom q) /\ (dom p) & ( for x being set st x in dom b_{1} holds

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

ex b_{1} being Function st

( dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) 'xor' (q . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) 'xor' (q . x) ) & dom b_{2} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (p . x) 'xor' (q . x) ) holds

b_{1} = b_{2}

for b_{1} being Function

for p, q being boolean-valued Function st dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) 'xor' (q . x) ) holds

( dom b_{1} = (dom q) /\ (dom p) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (q . x) 'xor' (p . x) ) )
;

end;
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 ( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds

it . x = (p . x) 'or' (q . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

b

( dom b

b

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 ( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds

it . x = (p . x) 'xor' (q . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

for p, q being boolean-valued Function st dom b

b

( dom b

b

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

for p, q, b_{3} being boolean-valued Function holds

( b_{3} = p 'or' q iff ( dom b_{3} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{3} holds

b_{3} . x = (p . x) 'or' (q . x) ) ) );

for p, q, b

( b

b

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

for p, q being boolean-valued Function

for b_{3} being Function holds

( b_{3} = p 'xor' q iff ( dom b_{3} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{3} holds

b_{3} . x = (p . x) 'xor' (q . x) ) ) );

for p, q being boolean-valued Function

for b

( b

b

registration
end;

definition

let A be non empty set ;

let p, q be Function of A,BOOLEAN;

p 'or' q is Function of A,BOOLEAN

for b_{1} being Function of A,BOOLEAN holds

( b_{1} = p 'or' q iff for x being Element of A holds b_{1} . x = (p . x) 'or' (q . x) )

p 'xor' q is Function of A,BOOLEAN

for b_{1} being Function of A,BOOLEAN holds

( b_{1} = p 'xor' q iff for x being Element of A holds b_{1} . x = (p . x) 'xor' (q . x) )

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

p 'or' q is Function of A,BOOLEAN

proof end;

compatibility for b

( b

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

p 'xor' q is Function of A,BOOLEAN

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def4 defines 'or' BVFUNC_1:def 4 :

for A being non empty set

for p, q, b_{4} being Function of A,BOOLEAN holds

( b_{4} = p 'or' q iff for x being Element of A holds b_{4} . x = (p . x) 'or' (q . x) );

for A being non empty set

for p, q, b

( b

:: deftheorem defines 'xor' BVFUNC_1:def 5 :

for A being non empty set

for p, q, b_{4} being Function of A,BOOLEAN holds

( b_{4} = p 'xor' q iff for x being Element of A holds b_{4} . x = (p . x) 'xor' (q . x) );

for A being non empty set

for p, q, b

( b

definition

let p, q be boolean-valued Function;

ex b_{1} being Function st

( dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) => (q . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) => (q . x) ) & dom b_{2} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (p . x) => (q . x) ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) <=> (q . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) <=> (q . x) ) & dom b_{2} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (p . x) <=> (q . x) ) holds

b_{1} = b_{2}

for b_{1} being Function

for p, q being boolean-valued Function st dom b_{1} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (p . x) <=> (q . x) ) holds

( dom b_{1} = (dom q) /\ (dom p) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (q . x) <=> (p . x) ) )
;

end;
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 ( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds

it . x = (p . x) => (q . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

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 ( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds

it . x = (p . x) <=> (q . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

for p, q being boolean-valued Function st dom b

b

( dom b

b

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

for p, q being boolean-valued Function

for b_{3} being Function holds

( b_{3} = p 'imp' q iff ( dom b_{3} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{3} holds

b_{3} . x = (p . x) => (q . x) ) ) );

for p, q being boolean-valued Function

for b

( b

b

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

for p, q being boolean-valued Function

for b_{3} being Function holds

( b_{3} = p 'eqv' q iff ( dom b_{3} = (dom p) /\ (dom q) & ( for x being set st x in dom b_{3} holds

b_{3} . x = (p . x) <=> (q . x) ) ) );

for p, q being boolean-valued Function

for b

( b

b

registration

let p, q be boolean-valued Function;

coherence

p 'imp' q is boolean-valued

p 'eqv' q is boolean-valued

end;
coherence

p 'imp' q is boolean-valued

proof end;

coherence p 'eqv' q is boolean-valued

proof end;

definition

let A be non empty set ;

let p, q be Function of A,BOOLEAN;

p 'imp' q is Function of A,BOOLEAN

for b_{1} being Function of A,BOOLEAN holds

( b_{1} = p 'imp' q iff for x being Element of A holds b_{1} . x = ('not' (p . x)) 'or' (q . x) )

p 'eqv' q is Function of A,BOOLEAN

for b_{1} being Function of A,BOOLEAN holds

( b_{1} = p 'eqv' q iff for x being Element of A holds b_{1} . x = 'not' ((p . x) 'xor' (q . x)) )

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

p 'imp' q is Function of A,BOOLEAN

proof end;

compatibility for b

( b

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

p 'eqv' q is Function of A,BOOLEAN

proof end;

compatibility for b

( b

proof end;

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

for A being non empty set

for p, q, b_{4} being Function of A,BOOLEAN holds

( b_{4} = p 'imp' q iff for x being Element of A holds b_{4} . x = ('not' (p . x)) 'or' (q . x) );

for A being non empty set

for p, q, b

( b

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

for A being non empty set

for p, q, b_{4} being Function of A,BOOLEAN holds

( b_{4} = p 'eqv' q iff for x being Element of A holds b_{4} . x = 'not' ((p . x) 'xor' (q . x)) );

for A being non empty set

for p, q, b

( b

definition

let Y be non empty set ;

ex b_{1} being Function of Y,BOOLEAN st

for x being Element of Y holds b_{1} . x = FALSE

for b_{1}, b_{2} being Function of Y,BOOLEAN st ( for x being Element of Y holds b_{1} . x = FALSE ) & ( for x being Element of Y holds b_{2} . x = FALSE ) holds

b_{1} = b_{2}

end;
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 for x being Element of Y holds it . x = FALSE ;

ex b

for x being Element of Y holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines O_el BVFUNC_1:def 10 :

for Y being non empty set

for b_{2} being Function of Y,BOOLEAN holds

( b_{2} = O_el Y iff for x being Element of Y holds b_{2} . x = FALSE );

for Y being non empty set

for b

( b

definition

let Y be non empty set ;

ex b_{1} being Function of Y,BOOLEAN st

for x being Element of Y holds b_{1} . x = TRUE

for b_{1}, b_{2} being Function of Y,BOOLEAN st ( for x being Element of Y holds b_{1} . x = TRUE ) & ( for x being Element of Y holds b_{2} . x = TRUE ) holds

b_{1} = b_{2}

end;
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 for x being Element of Y holds it . x = TRUE ;

ex b

for x being Element of Y holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines I_el BVFUNC_1:def 11 :

for Y being non empty set

for b_{2} being Function of Y,BOOLEAN holds

( b_{2} = I_el Y iff for x being Element of Y holds b_{2} . x = TRUE );

for Y being non empty set

for b

( b

theorem :: BVFUNC_1:3

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)

for a, b, c being Function of Y,BOOLEAN holds (a '&' b) '&' c = a '&' (b '&' c)

proof end;

theorem :: BVFUNC_1:7

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)

for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'or' c = a 'or' (b 'or' c)

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)

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)

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)

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)

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;

for a being Function of Y,BOOLEAN

for x being Element of Y st a . x = TRUE holds

a . x = TRUE ;

end;
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 x being Element of Y st a . x = TRUE holds

b . x = TRUE ;

for a being Function of Y,BOOLEAN

for x being Element of Y st a . x = TRUE holds

a . x = TRUE ;

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

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

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 )

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 )

for a, b being Function of Y,BOOLEAN holds

( a 'eqv' b = I_el Y iff a = b )

proof end;

begin

definition

let Y be non empty set ;

let a be Function of Y,BOOLEAN;

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 b_{1} being Function of Y,BOOLEAN holds verum;

;

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 b_{1} being Function of Y,BOOLEAN holds verum;

;

end;
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 I_el Y if for x being Element of Y holds a . x = TRUE

otherwise O_el Y;

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 b

;

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 O_el Y if for x being Element of Y holds a . x = FALSE

otherwise I_el Y;

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 b

;

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

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

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

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 )

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

registration
end;

registration

let Y be non empty set ;

ex b_{1} being Function of Y,BOOLEAN st b_{1} is constant

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

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

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 )

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

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 )

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 )

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

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

for a being Function of Y,BOOLEAN

for x being Element of Y holds a . x <= (B_SUP a) . x

proof end;

begin

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

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

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 b_{1} being Element of PA holds b_{1} is Subset of Y

end;
let PA be a_partition of Y;

:: original: Element

redefine mode Element of PA -> Subset of Y;

coherence

for b

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

definition

let Y be non empty set ;

let a be Function of Y,BOOLEAN;

let PA be a_partition of Y;

ex b_{1} 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 b_{1} . y = TRUE ) & ( ex x being Element of Y st

( x in EqClass (y,PA) & not a . x = TRUE ) implies b_{1} . y = FALSE ) )

for b_{1}, b_{2} 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 b_{1} . y = TRUE ) & ( ex x being Element of Y st

( x in EqClass (y,PA) & not a . x = TRUE ) implies b_{1} . 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 b_{2} . y = TRUE ) & ( ex x being Element of Y st

( x in EqClass (y,PA) & not a . x = TRUE ) implies b_{2} . y = FALSE ) ) ) holds

b_{1} = b_{2}

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

ex b

for y being Element of Y holds

( ( ( for x being Element of Y st x in EqClass (y,PA) holds

a . x = TRUE ) implies b

( x in EqClass (y,PA) & not a . x = TRUE ) implies b

proof end;

uniqueness for b

( ( ( for x being Element of Y st x in EqClass (y,PA) holds

a . x = TRUE ) implies b

( x in EqClass (y,PA) & not a . x = TRUE ) implies b

( ( ( for x being Element of Y st x in EqClass (y,PA) holds

a . x = TRUE ) implies b

( x in EqClass (y,PA) & not a . x = TRUE ) implies b

b

proof 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 b_{4} being Function of Y,BOOLEAN holds

( b_{4} = 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 b_{4} . y = TRUE ) & ( ex x being Element of Y st

( x in EqClass (y,PA) & not a . x = TRUE ) implies b_{4} . y = FALSE ) ) );

for Y being non empty set

for a being Function of Y,BOOLEAN

for PA being a_partition of Y

for b

( b

( ( ( for x being Element of Y st x in EqClass (y,PA) holds

a . x = TRUE ) implies b

( x in EqClass (y,PA) & not a . x = TRUE ) implies b

definition

let Y be non empty set ;

let a be Function of Y,BOOLEAN;

let PA be a_partition of Y;

ex b_{1} 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 b_{1} . y = TRUE ) & ( ( for x being Element of Y holds

( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b_{1} . y = FALSE ) )

for b_{1}, b_{2} 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 b_{1} . y = TRUE ) & ( ( for x being Element of Y holds

( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b_{1} . 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 b_{2} . y = TRUE ) & ( ( for x being Element of Y holds

( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b_{2} . y = FALSE ) ) ) holds

b_{1} = b_{2}

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

ex b

for y being Element of Y holds

( ( ex x being Element of Y st

( x in EqClass (y,PA) & a . x = TRUE ) implies b

( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b

proof end;

uniqueness for b

( ( ex x being Element of Y st

( x in EqClass (y,PA) & a . x = TRUE ) implies b

( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b

( ( ex x being Element of Y st

( x in EqClass (y,PA) & a . x = TRUE ) implies b

( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b

b

proof 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 b_{4} being Function of Y,BOOLEAN holds

( b_{4} = 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 b_{4} . y = TRUE ) & ( ( for x being Element of Y holds

( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b_{4} . y = FALSE ) ) );

for Y being non empty set

for a being Function of Y,BOOLEAN

for PA being a_partition of Y

for b

( b

( ( ex x being Element of Y st

( x in EqClass (y,PA) & a . x = TRUE ) implies b

( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b

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

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

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

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)

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)

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

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

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;

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;

end;
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 { { x where x is Element of Y : f . x = TRUE } , { x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{}};

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;

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

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

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 ;

end;
:: original: 'nand'

redefine func x 'nand' y -> Element of BOOLEAN ;

correctness

coherence

x 'nand' y is Element of BOOLEAN ;

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

end;
:: original: 'nor'

redefine func x 'nor' y -> Element of BOOLEAN ;

correctness

coherence

x 'nor' y is Element of BOOLEAN ;

proof end;

definition

let x, y be boolean set ;

correctness

compatibility

for b_{1} being set holds

( b_{1} = x <=> y iff b_{1} = 'not' (x 'xor' y) );

;

end;
correctness

compatibility

for b

( b

;

:: deftheorem defines <=> BVFUNC_1:def 19 :

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

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 ;

end;
:: original: <=>

redefine func x <=> y -> Element of BOOLEAN ;

correctness

coherence

x <=> y is Element of BOOLEAN ;

proof end;

theorem :: BVFUNC_1:45

theorem :: BVFUNC_1:47

theorem :: BVFUNC_1:48

theorem :: BVFUNC_1:49

theorem :: BVFUNC_1:52

theorem :: BVFUNC_1:54

theorem :: BVFUNC_1:55

theorem :: BVFUNC_1:58

theorem :: BVFUNC_1:60

theorem :: BVFUNC_1:68

theorem :: BVFUNC_1:69

theorem :: BVFUNC_1:70