BVFUNC

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

:: BVFUNC_1 semantic presentation

definition

let k, l be boolean set ;
canceled;
canceled;
redefine pred k <= l means :Def3: :: BVFUNC_1:def 3
k => l = TRUE ;
compatibility

proof end;

end;

:: deftheorem BVFUNC_1:def 1 :

:: deftheorem BVFUNC_1:def 2 :

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

definition

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

end;

:: deftheorem defines BVF BVFUNC_1:def 4 :

registration

let Y be set ;
cluster BVF Y -> non empty functional ;
coherence ;

end;

registration

let Y be set ;
cluster -> boolean-valued Element of BVF Y;
coherence ;

end;

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

for f1, f2 being Element of Funcs F₁(),BOOLEAN st ( for x being Element of F₁() holds f1 . x = F₂(x) ) & ( for x being Element of F₁() holds f2 . x = F₂(x) ) holds
f1 = f2

proof end;

definition

let Y be non empty set ;
let a be Element of BVF Y;
:: original: 'not'
redefine func 'not' a -> Element of BVF Y;
coherence

proof end;

let b be Element of BVF Y;
:: original: '&'
redefine func a '&' b -> Element of BVF Y;
coherence

proof end;

end;

definition

let p, q be boolean-valued Function;
func p 'or' q -> boolean-valued Function means :Def5: :: BVFUNC_1:def 5
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) 'or' (q . x) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;
idempotence ;
func p 'xor' 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) 'xor' (q . x) ) );
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 p, q be boolean-valued Function;
cluster p 'xor' q -> boolean-valued ;
coherence

proof end;

end;

definition

let A be non empty set ;
let p, q be Element of Funcs A,BOOLEAN ;
:: original: 'or'
redefine func p 'or' q -> Element of Funcs A,BOOLEAN means :Def7: :: BVFUNC_1:def 7
for x being Element of A holds it . x = (p . x) 'or' (q . x);
coherence

proof end;

compatibility

proof end;

:: original: 'xor'
redefine func p 'xor' q -> Element of Funcs A,BOOLEAN means :: BVFUNC_1:def 8
for x being Element of A holds it . x = (p . x) 'xor' (q . x);
coherence

proof end;

compatibility

proof end;

end;

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

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

definition

let Y be non empty set ;
let a, b be Element of BVF Y;
:: original: 'or'
redefine func a 'or' b -> Element of BVF Y;
coherence

proof end;

:: original: 'xor'
redefine func a 'xor' b -> Element of BVF Y;
coherence

proof end;

end;

definition

let p, q be boolean-valued Function;
func p 'imp' q -> Function means :Def9: :: BVFUNC_1:def 9
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) => (q . x) ) );
existence

proof end;

uniqueness

proof end;

func p 'eqv' q -> Function means :Def10: :: BVFUNC_1:def 10
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) <=> (q . x) ) );
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 p, q be boolean-valued Function;
cluster p 'imp' q -> boolean-valued ;
coherence

proof end;

cluster p 'eqv' q -> boolean-valued ;
coherence

proof end;

end;

definition

let A be non empty set ;
let p, q be Element of Funcs A,BOOLEAN ;
:: original: 'imp'
redefine func p 'imp' q -> Element of Funcs A,BOOLEAN means :Def11: :: BVFUNC_1:def 11
for x being Element of A holds it . x = ('not' (p . x)) 'or' (q . x);
coherence

proof end;

compatibility

proof end;

:: original: 'eqv'
redefine func p 'eqv' q -> Element of Funcs A,BOOLEAN means :Def12: :: BVFUNC_1:def 12
for x being Element of A holds it . x = 'not' ((p . x) 'xor' (q . x));
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 Y be non empty set ;
let a, b be Element of BVF Y;
:: original: 'imp'
redefine func a 'imp' b -> Element of BVF Y;
coherence

proof end;

:: original: 'eqv'
redefine func a 'eqv' b -> Element of BVF Y;
coherence

proof end;

end;

definition

let Y be non empty set ;
func O_el Y -> Element of Funcs Y,BOOLEAN means :Def13: :: BVFUNC_1:def 13
for x being Element of Y holds it . x = FALSE ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines O_el BVFUNC_1:def 13 :

definition

let Y be non empty set ;
func I_el Y -> Element of Funcs Y,BOOLEAN means :Def14: :: BVFUNC_1:def 14
for x being Element of Y holds it . x = TRUE ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines I_el BVFUNC_1:def 14 :

theorem :: BVFUNC_1:1

canceled;

theorem :: BVFUNC_1:2

canceled;

theorem :: BVFUNC_1:3

canceled;

theorem :: BVFUNC_1:4

for a being boolean-valued Function holds 'not' ('not' a) = a ;

theorem Th5: :: BVFUNC_1:5

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

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds a '&' a = a ;

theorem :: BVFUNC_1:7

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a '&' b) '&' c = a '&' (b '&' c)

proof end;

theorem Th8: :: BVFUNC_1:8

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a '&' (O_el Y) = O_el Y

proof end;

theorem Th9: :: BVFUNC_1:9

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a '&' (I_el Y) = a

proof end;

theorem :: BVFUNC_1:10

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a 'or' a = a ;

theorem :: BVFUNC_1:11

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a 'or' b) 'or' c = a 'or' (b 'or' c)

proof end;

theorem Th12: :: BVFUNC_1:12

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a 'or' (O_el Y) = a

proof end;

theorem Th13: :: BVFUNC_1:13

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN holds a 'or' (I_el Y) = I_el Y

proof end;

theorem :: BVFUNC_1:14

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a '&' b) 'or' c = (a 'or' c) '&' (b 'or' c)

proof end;

theorem :: BVFUNC_1:15

for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (a 'or' b) '&' c = (a '&' c) 'or' (b '&' c)

proof end;

theorem :: BVFUNC_1:16

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds 'not' (a 'or' b) = ('not' a) '&' ('not' b)

proof end;

theorem :: BVFUNC_1:17

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds 'not' (a '&' b) = ('not' a) 'or' ('not' b)

proof end;

definition

let Y be non empty set ;
let a, b be Element of Funcs Y,BOOLEAN ;
pred a '<' b means :Def15: :: BVFUNC_1:def 15
for x being Element of Y st a . x = TRUE holds
b . x = TRUE ;
reflexivity ;

end;

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