:: Propositional Calculus for Boolean Valued Functions, {VII}
:: by Shunichi Kobayashi
::
:: 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 '&' ()
proof end;

theorem Th2: :: BVFUNC25:2
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = () 'imp' ()
proof end;

theorem :: BVFUNC25:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = () 'eqv' ()
proof end;

theorem Th4: :: BVFUNC25:4
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'imp' (a '&' 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)
proof end;

theorem :: BVFUNC25:6
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' () = O_el Y
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)
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)
proof end;

theorem :: BVFUNC25:9
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = a 'xor' ()
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)
proof end;

theorem Th12: :: BVFUNC25:11
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = 'not' (a 'xor' b)
proof end;

theorem Th13: :: BVFUNC25:12
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' a = O_el Y
proof end;

theorem Th14: :: BVFUNC25:13
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' () = I_el Y
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
proof end;

registration
let Y be non empty set ;
let a, b be Function of Y,BOOLEAN;
reduce (a 'imp' b) 'imp' (b 'imp' a) to b 'imp' a;
reducibility
(a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a
by Red1;
end;

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

theorem Th16: :: BVFUNC25:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'or' (() '&' ()) = (() 'or' b) '&' (a 'or' ())
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
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
proof end;

theorem :: BVFUNC25:19
for Y being non empty set
for a being Function of Y,BOOLEAN holds ('not' ()) 'imp' a = I_el Y by BVFUNC_5:7;

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

theorem Th21: :: BVFUNC25:21
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (() 'imp' a) = I_el Y
proof end;

theorem :: BVFUNC25:22
for Y being non empty set
for a being Function of Y,BOOLEAN holds (() 'imp' a) 'eqv' a = I_el Y
proof end;

theorem :: BVFUNC25:23
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' (a 'imp' b) = 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
proof end;

theorem :: BVFUNC25:25
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (() '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' ()) = I_el Y
proof end;

theorem :: BVFUNC25:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds () 'imp' (() '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
proof end;

theorem :: BVFUNC25:29
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'eqv' (a '&' b)
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 )
proof end;

theorem :: BVFUNC25:31
for Y being non empty set
for a being Function of Y,BOOLEAN holds a = () 'imp' a
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
proof end;

theorem :: BVFUNC25:33
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a 'imp' b) 'imp' a
proof end;

theorem :: BVFUNC25:34
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (b 'imp' a) '&' (() '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' ())
proof end;

theorem :: BVFUNC25:36
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' b = () 'imp' b
proof end;

theorem :: BVFUNC25:37
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' b = (a 'imp' b) 'imp' 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
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
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
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
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
proof end;

theorem :: BVFUNC25:43
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y by ;

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
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
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) '<' () 'imp' (b 'or' c)
proof end;

definition
let p, q be boolean-valued Function;
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
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) 'nand' (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) 'nand' (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds
b2 . x = (p . x) 'nand' (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) 'nand' (q . x) ) holds
( dom b1 = (dom q) /\ (dom p) & ( for x being set st x in dom b1 holds
b1 . x = (q . x) 'nand' (p . x) ) )
;
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
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) 'nor' (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) 'nor' (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds
b2 . x = (p . x) 'nor' (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) 'nor' (q . x) ) holds
( dom b1 = (dom q) /\ (dom p) & ( for x being set st x in dom b1 holds
b1 . x = (q . x) 'nor' (p . x) ) )
;
end;

:: deftheorem Def1 defines 'nand' BVFUNC25:def 1 :
for p, q being boolean-valued Function
for b3 being Function holds
( b3 = p 'nand' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) 'nand' (q . x) ) ) );

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

registration
let p, q be boolean-valued Function;
coherence
proof end;
coherence
proof end;
end;

definition
let A be non empty set ;
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
p 'nand' q is Function of A,BOOLEAN
proof end;
compatibility
for b1 being Function of A,BOOLEAN holds
( b1 = p 'nand' q iff for x being Element of A holds b1 . x = (p . x) 'nand' (q . x) )
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
p 'nor' q is Function of A,BOOLEAN
proof end;
compatibility
for b1 being Function of A,BOOLEAN holds
( b1 = p 'nor' q iff for x being Element of A holds b1 . x = (p . x) 'nor' (q . x) )
proof end;
end;

:: deftheorem Def3 defines 'nand' BVFUNC25:def 3 :
for A being non empty set
for p, q, b4 being Function of A,BOOLEAN holds
( b4 = p 'nand' q iff for x being Element of A holds b4 . x = (p . x) 'nand' (q . x) );

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

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
proof end;
:: original: 'nor'
redefine func a 'nor' b -> Function of Y,BOOLEAN;
coherence
a 'nor' b is Function of Y,BOOLEAN
proof end;
end;

theorem th1: :: BVFUNC25:47
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nand' b = 'not' (a '&' b)
proof end;

theorem Th2: :: BVFUNC25:48
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' b = 'not' (a 'or' b)
proof end;

theorem Th3: :: BVFUNC25:49
for Y being non empty set
for a being Function of Y,BOOLEAN holds (I_el Y) 'nand' a = 'not' a
proof end;

theorem Th4: :: BVFUNC25:50
for Y being non empty set
for a being Function of Y,BOOLEAN holds (O_el Y) 'nand' a = I_el Y
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 )
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 )
proof end;

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

theorem :: BVFUNC25:54
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( a 'nand' () = I_el Y & 'not' (a 'nand' ()) = 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)
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
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))
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)
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) = () '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) = (() '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)
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
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 '&' 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)
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) = () 'or' b & a 'nand' (a 'nand' b) = a 'imp' b )
proof end;

theorem :: BVFUNC25:66
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'nor' b) = I_el Y
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) = () 'or' ()
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)
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)
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) = (() '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)
proof end;

theorem Th26: :: BVFUNC25:72
for Y being non empty set
for a being Function of Y,BOOLEAN holds (I_el Y) 'nor' a = O_el Y
proof end;

theorem Th27: :: BVFUNC25:73
for Y being non empty set
for a being Function of Y,BOOLEAN holds (O_el Y) 'nor' a = 'not' a
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 )
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 )
proof end;

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

theorem :: BVFUNC25:77
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( a 'nor' () = O_el Y & 'not' (a 'nor' ()) = I_el Y )
proof end;

theorem :: BVFUNC25:78
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds () '&' (a 'xor' b) = () '&' 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))
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)
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) = () '&' (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) = (() '&' b) '&' ()
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) = (() '&' 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) = () '&' (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))
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)
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) = () '&' b
proof end;

theorem :: BVFUNC25:88
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'imp' b) = O_el Y
proof end;

theorem :: BVFUNC25:89
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'nand' b) = O_el Y
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) = () '&' b
proof end;

theorem :: BVFUNC25:91
for Y being non empty set holds (O_el Y) 'eqv' (O_el Y) = I_el Y
proof end;

theorem :: BVFUNC25:92
for Y being non empty set holds (O_el Y) 'eqv' (I_el Y) = O_el Y
proof end;

theorem :: BVFUNC25:93
for Y being non empty set holds (I_el Y) 'eqv' (I_el Y) = I_el Y
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 )
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' ()
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 '&' ()) 'or' (a '&' ())
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' ()) 'or' ()
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' (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' ((() '&' 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)
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' ()) 'or' ())
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 '&' ()
proof end;

theorem :: BVFUNC25:103
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' (a 'nand' b) = I_el Y
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) = () '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 '&' ()
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)
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 '&' ()) '&' ()
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' ()) '&' (a 'or' ())
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))) '&' ((() '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) '&' (() '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))
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) = (() 'or' b) 'or' c
proof end;

theorem :: BVFUNC25:113
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'nor' b) = O_el Y
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' ()
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' ()
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) = () '&' 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))
proof end;