:: by Shunichi Kobayashi

::

:: Received February 6, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

theorem Th1: :: BVFUNC25:1

for Y being non empty set

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

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

proof end;

theorem Th2: :: BVFUNC25:2

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' b) 'imp' ('not' a)

for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' b) 'imp' ('not' a)

proof end;

theorem :: BVFUNC25:3

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'eqv' b = ('not' a) 'eqv' ('not' b)

for a, b being Function of Y,BOOLEAN holds a 'eqv' b = ('not' a) 'eqv' ('not' b)

proof end;

theorem :: BVFUNC25:5

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' b) 'imp' (a '&' b)

for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' b) 'imp' (a '&' b)

proof end;

theorem :: BVFUNC25:7

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:8

for Y being non empty set

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

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

proof end;

theorem Th11: :: BVFUNC25:10

for Y being non empty set

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

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

proof end;

theorem Red1: :: BVFUNC25:14

for Y being non empty set

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

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

proof end;

registration

let Y be non empty set ;

let a, b be Function of Y,BOOLEAN;

reducibility

(a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a by Red1;

end;
let a, b be Function of Y,BOOLEAN;

reducibility

(a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a by Red1;

theorem Th15: :: BVFUNC25:15

for Y being non empty set

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

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

proof end;

theorem Th16: :: BVFUNC25:16

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:17

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:18

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:19

theorem :: BVFUNC25:20

for Y being non empty set

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

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

proof end;

theorem Th21: :: BVFUNC25:21

for Y being non empty set

for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'imp' a) = I_el Y

for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'imp' a) = I_el Y

proof end;

theorem :: BVFUNC25:22

for Y being non empty set

for a being Function of Y,BOOLEAN holds (('not' a) 'imp' a) 'eqv' a = I_el Y

for a being Function of Y,BOOLEAN holds (('not' a) 'imp' a) 'eqv' a = I_el Y

proof end;

theorem :: BVFUNC25:24

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:25

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y

for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y

proof end;

theorem :: BVFUNC25:26

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y

for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y

proof end;

theorem :: BVFUNC25:27

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y

for a, b being Function of Y,BOOLEAN holds ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y

proof end;

theorem :: BVFUNC25:28

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:30

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds

( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b )

for a, b being Function of Y,BOOLEAN holds

( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b )

proof end;

theorem Th32: :: BVFUNC25:32

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'imp' ((a 'imp' b) 'imp' a) = I_el Y

for a, b being Function of Y,BOOLEAN holds a 'imp' ((a 'imp' b) 'imp' a) = I_el Y

proof end;

theorem :: BVFUNC25:34

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:35

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:38

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (a 'imp' a) = I_el Y

for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (a 'imp' a) = I_el Y

proof end;

theorem :: BVFUNC25:39

for Y being non empty set

for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el Y

for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el Y

proof end;

theorem :: BVFUNC25:40

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:41

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:42

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:43

theorem :: BVFUNC25:44

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:45

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:46

for Y being non empty set

for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c)

for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c)

proof end;

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) 'nand' (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) 'nand' (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) 'nand' (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) 'nand' (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) 'nand' (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) 'nor' (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) 'nor' (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) 'nor' (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) 'nor' (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) 'nor' (p . x) ) )
;

end;
func p 'nand' q -> Function means :Def1: :: BVFUNC25:def 1

( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds

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

existence ( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds

it . x = (p . x) 'nand' (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

func p 'nor' q -> Function means :Def2: :: BVFUNC25:def 2

( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds

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

existence ( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds

it . x = (p . x) 'nor' (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 Def1 defines 'nand' BVFUNC25:def 1 :

for p, q being boolean-valued Function

for b_{3} being Function holds

( b_{3} = p 'nand' 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) 'nand' (q . x) ) ) );

for p, q being boolean-valued Function

for b

( b

b

:: deftheorem Def2 defines 'nor' BVFUNC25:def 2 :

for p, q being boolean-valued Function

for b_{3} being Function holds

( b_{3} = p 'nor' 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) 'nor' (q . x) ) ) );

for p, q being boolean-valued Function

for b

( b

b

registration

let p, q be boolean-valued Function;

coherence

p 'nand' q is boolean-valued

p 'nor' q is boolean-valued

end;
coherence

p 'nand' q is boolean-valued

proof end;

coherence p 'nor' q is boolean-valued

proof end;

definition

let A be non empty set ;

let p, q be Function of A,BOOLEAN;

p 'nand' q is Function of A,BOOLEAN

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

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

p 'nor' q is Function of A,BOOLEAN

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

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

end;
let p, q be Function of A,BOOLEAN;

:: original: 'nand'

redefine func p 'nand' q -> Function of A,BOOLEAN means :Def3: :: BVFUNC25:def 3

for x being Element of A holds it . x = (p . x) 'nand' (q . x);

coherence redefine func p 'nand' q -> Function of A,BOOLEAN means :Def3: :: BVFUNC25:def 3

for x being Element of A holds it . x = (p . x) 'nand' (q . x);

p 'nand' q is Function of A,BOOLEAN

proof end;

compatibility for b

( b

proof end;

:: original: 'nor'

redefine func p 'nor' q -> Function of A,BOOLEAN means :Def4: :: BVFUNC25:def 4

for x being Element of A holds it . x = (p . x) 'nor' (q . x);

coherence redefine func p 'nor' q -> Function of A,BOOLEAN means :Def4: :: BVFUNC25:def 4

for x being Element of A holds it . x = (p . x) 'nor' (q . x);

p 'nor' q is Function of A,BOOLEAN

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def3 defines 'nand' BVFUNC25:def 3 :

for A being non empty set

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

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

for A being non empty set

for p, q, b

( b

:: deftheorem Def4 defines 'nor' BVFUNC25:def 4 :

for A being non empty set

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

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

for A being non empty set

for p, q, b

( b

definition

let Y be non empty set ;

let a, b be Function of Y,BOOLEAN;

:: original: 'nand'

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

coherence

a 'nand' b is Function of Y,BOOLEAN

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

coherence

a 'nor' b is Function of Y,BOOLEAN

end;
let a, b be Function of Y,BOOLEAN;

:: original: 'nand'

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

coherence

a 'nand' b is Function of Y,BOOLEAN

proof end;

:: original: 'nor'redefine func a 'nor' b -> Function of Y,BOOLEAN;

coherence

a 'nor' b is Function of Y,BOOLEAN

proof end;

theorem :: BVFUNC25:51

for Y being non empty set holds

( (O_el Y) 'nand' (O_el Y) = I_el Y & (O_el Y) 'nand' (I_el Y) = I_el Y & (I_el Y) 'nand' (I_el Y) = O_el Y )

( (O_el Y) 'nand' (O_el Y) = I_el Y & (O_el Y) 'nand' (I_el Y) = I_el Y & (I_el Y) 'nand' (I_el Y) = O_el Y )

proof end;

theorem :: BVFUNC25:52

for Y being non empty set

for a being Function of Y,BOOLEAN holds

( a 'nand' a = 'not' a & 'not' (a 'nand' a) = a )

for a being Function of Y,BOOLEAN holds

( a 'nand' a = 'not' a & 'not' (a 'nand' a) = a )

proof end;

theorem :: BVFUNC25:54

for Y being non empty set

for a being Function of Y,BOOLEAN holds

( a 'nand' ('not' a) = I_el Y & 'not' (a 'nand' ('not' a)) = O_el Y )

for a being Function of Y,BOOLEAN holds

( a 'nand' ('not' a) = I_el Y & 'not' (a 'nand' ('not' a)) = O_el Y )

proof end;

theorem Th9: :: BVFUNC25:55

for Y being non empty set

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

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

proof end;

theorem Th10: :: BVFUNC25:56

for Y being non empty set

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

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

proof end;

theorem th11: :: BVFUNC25:57

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:58

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:59

for Y being non empty set

for a, b, c being Function of Y,BOOLEAN holds

( a 'nand' (b 'nand' c) = ('not' a) 'or' (b '&' c) & a 'nand' (b 'nand' c) = a 'imp' (b '&' c) )

for a, b, c being Function of Y,BOOLEAN holds

( a 'nand' (b 'nand' c) = ('not' a) 'or' (b '&' c) & a 'nand' (b 'nand' c) = a 'imp' (b '&' c) )

proof end;

theorem :: BVFUNC25:60

for Y being non empty set

for a, b, c being Function of Y,BOOLEAN holds

( a 'nand' (b 'nor' c) = (('not' a) 'or' b) 'or' c & a 'nand' (b 'nor' c) = a 'imp' (b 'or' c) )

for a, b, c being Function of Y,BOOLEAN holds

( a 'nand' (b 'nor' c) = (('not' a) 'or' b) 'or' c & a 'nand' (b 'nor' c) = a 'imp' (b 'or' c) )

proof end;

theorem :: BVFUNC25:61

for Y being non empty set

for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b 'eqv' c) = a 'imp' (b 'xor' c)

for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b 'eqv' c) = a 'imp' (b 'xor' c)

proof end;

theorem :: BVFUNC25:62

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:63

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'or' b) = ('not' a) '&' ('not' (a '&' b))

for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'or' b) = ('not' a) '&' ('not' (a '&' b))

proof end;

theorem :: BVFUNC25:64

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'eqv' b) = a 'imp' (a 'xor' b)

for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'eqv' b) = a 'imp' (a 'xor' b)

proof end;

theorem :: BVFUNC25:65

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds

( a 'nand' (a 'nand' b) = ('not' a) 'or' b & a 'nand' (a 'nand' b) = a 'imp' b )

for a, b being Function of Y,BOOLEAN holds

( a 'nand' (a 'nand' b) = ('not' a) 'or' b & a 'nand' (a 'nand' b) = a 'imp' b )

proof end;

theorem :: BVFUNC25:67

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'eqv' b) = ('not' a) 'or' ('not' b)

for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'eqv' b) = ('not' a) 'or' ('not' b)

proof end;

theorem :: BVFUNC25:68

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:69

for Y being non empty set

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

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

proof end;

theorem Th24: :: BVFUNC25:70

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:71

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'imp' b) = 'not' (a '&' b)

for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'imp' b) = 'not' (a '&' b)

proof end;

theorem :: BVFUNC25:74

for Y being non empty set holds

( (O_el Y) 'nor' (O_el Y) = I_el Y & (O_el Y) 'nor' (I_el Y) = O_el Y & (I_el Y) 'nor' (I_el Y) = O_el Y )

( (O_el Y) 'nor' (O_el Y) = I_el Y & (O_el Y) 'nor' (I_el Y) = O_el Y & (I_el Y) 'nor' (I_el Y) = O_el Y )

proof end;

theorem :: BVFUNC25:75

for Y being non empty set

for a being Function of Y,BOOLEAN holds

( a 'nor' a = 'not' a & 'not' (a 'nor' a) = a )

for a being Function of Y,BOOLEAN holds

( a 'nor' a = 'not' a & 'not' (a 'nor' a) = a )

proof end;

theorem :: BVFUNC25:77

for Y being non empty set

for a being Function of Y,BOOLEAN holds

( a 'nor' ('not' a) = O_el Y & 'not' (a 'nor' ('not' a)) = I_el Y )

for a being Function of Y,BOOLEAN holds

( a 'nor' ('not' a) = O_el Y & 'not' (a 'nor' ('not' a)) = I_el Y )

proof end;

theorem :: BVFUNC25:78

for Y being non empty set

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

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

proof end;

theorem Th33: :: BVFUNC25:79

for Y being non empty set

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

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

proof end;

theorem Th34: :: BVFUNC25:80

for Y being non empty set

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

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

proof end;

theorem Th35: :: BVFUNC25:81

for Y being non empty set

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

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

proof end;

theorem Th36: :: BVFUNC25:82

for Y being non empty set

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

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

proof end;

theorem Th37: :: BVFUNC25:83

for Y being non empty set

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

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

proof end;

theorem Th38: :: BVFUNC25:84

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:85

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'nor' (a '&' b) = 'not' (a '&' (a 'or' b))

for a, b being Function of Y,BOOLEAN holds a 'nor' (a '&' b) = 'not' (a '&' (a 'or' b))

proof end;

theorem :: BVFUNC25:86

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:87

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'eqv' b) = ('not' a) '&' b

for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'eqv' b) = ('not' a) '&' b

proof end;

theorem :: BVFUNC25:90

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:94

for Y being non empty set

for a being Function of Y,BOOLEAN holds

( a 'eqv' a = I_el Y & 'not' (a 'eqv' a) = O_el Y )

for a being Function of Y,BOOLEAN holds

( a 'eqv' a = I_el Y & 'not' (a 'eqv' a) = O_el Y )

proof end;

theorem :: BVFUNC25:95

for Y being non empty set

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

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

proof end;

theorem Th50: :: BVFUNC25:96

for Y being non empty set

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

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

proof end;

theorem Th51: :: BVFUNC25:97

for Y being non empty set

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

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

proof end;

theorem Th52: :: BVFUNC25:98

for Y being non empty set

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

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

proof end;

theorem Th53: :: BVFUNC25:99

for Y being non empty set

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

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

proof end;

theorem Th54: :: BVFUNC25:100

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:101

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:102

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:104

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'xor' (a 'nand' b) = ('not' a) 'or' b

for a, b being Function of Y,BOOLEAN holds a 'xor' (a 'nand' b) = ('not' a) 'or' b

proof end;

theorem :: BVFUNC25:105

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'nand' b) = a '&' ('not' b)

for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'nand' b) = a '&' ('not' b)

proof end;

theorem :: BVFUNC25:106

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'nand' b) = 'not' (a '&' b)

for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'nand' b) = 'not' (a '&' b)

proof end;

theorem Th61: :: BVFUNC25:107

for Y being non empty set

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

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

proof end;

theorem Th62: :: BVFUNC25:108

for Y being non empty set

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

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

proof end;

theorem Th63: :: BVFUNC25:109

for Y being non empty set

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

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

proof end;

theorem Th64: :: BVFUNC25:110

for Y being non empty set

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

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

proof end;

theorem Th65: :: BVFUNC25:111

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:112

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:114

for Y being non empty set

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

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

proof end;

theorem :: BVFUNC25:115

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'xor' (a 'nor' b) = a 'or' ('not' b)

for a, b being Function of Y,BOOLEAN holds a 'xor' (a 'nor' b) = a 'or' ('not' b)

proof end;

theorem :: BVFUNC25:116

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'nor' b) = ('not' a) '&' b

for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'nor' b) = ('not' a) '&' b

proof end;

theorem :: BVFUNC25:117

for Y being non empty set

for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'nor' b) = 'not' (a 'or' (a '&' b))

for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'nor' b) = 'not' (a 'or' (a '&' b))

proof end;