:: Propositional Calculus for Boolean Valued Functions, {VIII}
:: by Shunichi Kobayashi
::
:: Received September 25, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

definition
let p, q be boolean-valued Function;
funcp 'nand' q ->  Function means :Def1: :: BVFUNC26: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) ) )
proofend;
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
proofend;
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) ) ) ;
funcp 'nor' q ->  Function means :Def2: :: BVFUNC26: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) ) )
proofend;
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
proofend;
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' BVFUNC26: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' BVFUNC26: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;
clusterp 'nand' q ->  boolean-valued ;
coherence
 p 'nand' q is boolean-valued
proofend;
clusterp 'nor' q ->  boolean-valued ;
coherence
 p 'nor' q is boolean-valued
proofend;
end;

definition
let A be non empty set ;
let p, q be Function of A,BOOLEAN;
:: original:'nand'
redefine funcp 'nand' q ->  Function of A,BOOLEAN means :Def3: :: BVFUNC26: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
proofend;
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) )
proofend;
:: original:'nor'
redefine funcp 'nor' q ->  Function of A,BOOLEAN means :Def4: :: BVFUNC26: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
proofend;
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) )
proofend;
end;

:: deftheorem Def3 defines 'nand' BVFUNC26: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' BVFUNC26: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 funca 'nand' b ->  Function of Y,BOOLEAN;
coherence
 a 'nand' b is Function of Y,BOOLEAN
proofend;
:: original:'nor'
redefine funca 'nor' b ->  Function of Y,BOOLEAN;
coherence
 a 'nor' b is Function of Y,BOOLEAN
proofend;
end;

theorem Th1: :: BVFUNC26:1
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nand' b = 'not' (a '&' b)
proofend;

theorem Th2: :: BVFUNC26:2
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' b = 'not' (a 'or' b)
proofend;

theorem Th3: :: BVFUNC26:3
for Y being non empty set
for a being Function of Y,BOOLEAN holds (I_el Y) 'nand' a = 'not' a
proofend;

theorem Th4: :: BVFUNC26:4
for Y being non empty set
for a being Function of Y,BOOLEAN holds (O_el Y) 'nand' a = I_el Y
proofend;

theorem :: BVFUNC26:5
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 )
proofend;

theorem :: BVFUNC26:6
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( a 'nand' a = 'not' a & 'not' (a 'nand' a) = a )
proofend;

theorem :: BVFUNC26:7
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'nand' b) = a '&' b
proofend;

theorem :: BVFUNC26:8
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 )
proofend;

theorem Th9: :: BVFUNC26:9
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b '&' c) = 'not' ((a '&' b) '&' c)
proofend;

theorem Th10: :: BVFUNC26:10
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b '&' c) = (a '&' b) 'nand' c
proofend;

theorem Th11: :: BVFUNC26:11
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))
proofend;

theorem :: BVFUNC26:12
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)
proofend;

theorem :: BVFUNC26:13
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) )
proofend;

theorem :: BVFUNC26:14
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) )
proofend;

theorem :: BVFUNC26:15
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)
proofend;

theorem :: BVFUNC26:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nand' (a '&' b) = a 'nand' b
proofend;

theorem :: BVFUNC26:17
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))
proofend;

theorem :: BVFUNC26:18
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)
proofend;

theorem :: BVFUNC26:19
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 )
proofend;

theorem :: BVFUNC26:20
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'nor' b) = I_el Y
proofend;

theorem :: BVFUNC26:21
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)
proofend;

theorem :: BVFUNC26:22
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b = (a 'nand' b) 'nand' (a 'nand' b)
proofend;

theorem :: BVFUNC26:23
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)
proofend;

theorem Th24: :: BVFUNC26:24
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))
proofend;

theorem :: BVFUNC26:25
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'imp' b) = 'not' (a '&' b)
proofend;

theorem Th26: :: BVFUNC26:26
for Y being non empty set
for a being Function of Y,BOOLEAN holds (I_el Y) 'nor' a = O_el Y
proofend;

theorem Th27: :: BVFUNC26:27
for Y being non empty set
for a being Function of Y,BOOLEAN holds (O_el Y) 'nor' a = 'not' a
proofend;

theorem :: BVFUNC26:28
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 )
proofend;

theorem :: BVFUNC26:29
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( a 'nor' a = 'not' a & 'not' (a 'nor' a) = a )
proofend;

theorem :: BVFUNC26:30
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'nor' b) = a 'or' b
proofend;

theorem :: BVFUNC26:31
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 )
proofend;

theorem :: BVFUNC26:32
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' a) '&' (a 'xor' b) = ('not' a) '&' b
proofend;

theorem Th33: :: BVFUNC26:33
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))
proofend;

theorem Th34: :: BVFUNC26:34
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)
proofend;

theorem Th35: :: BVFUNC26:35
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)
proofend;

theorem Th36: :: BVFUNC26:36
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)
proofend;

theorem Th37: :: BVFUNC26:37
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
proofend;

theorem Th38: :: BVFUNC26:38
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)
proofend;

theorem :: BVFUNC26:39
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' (a '&' b) = 'not' (a '&' (a 'or' b))
proofend;

theorem :: BVFUNC26:40
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'or' b) = 'not' (a 'or' b)
proofend;

theorem :: BVFUNC26:41
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'eqv' b) = ('not' a) '&' b
proofend;

theorem :: BVFUNC26:42
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'imp' b) = O_el Y
proofend;

theorem :: BVFUNC26:43
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'nand' b) = O_el Y
proofend;

theorem :: BVFUNC26:44
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'nor' b) = ('not' a) '&' b
proofend;

theorem :: BVFUNC26:45
for Y being non empty set holds (O_el Y) 'eqv' (O_el Y) = I_el Y
proofend;

theorem :: BVFUNC26:46
for Y being non empty set holds (O_el Y) 'eqv' (I_el Y) = O_el Y
proofend;

theorem :: BVFUNC26:47
for Y being non empty set holds (I_el Y) 'eqv' (I_el Y) = I_el Y
proofend;

theorem :: BVFUNC26:48
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 )
proofend;

theorem :: BVFUNC26:49
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'or' b) = a 'or' ('not' b)
proofend;

theorem Th50: :: BVFUNC26:50
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))
proofend;

theorem Th51: :: BVFUNC26:51
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)
proofend;

theorem Th52: :: BVFUNC26:52
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)
proofend;

theorem Th53: :: BVFUNC26:53
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)
proofend;

theorem Th54: :: BVFUNC26:54
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)
proofend;

theorem Th55: :: BVFUNC26:55
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))
proofend;

theorem :: BVFUNC26:56
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'nand' b) = a '&' ('not' b)
proofend;

theorem :: BVFUNC26:57
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' (a 'nand' b) = I_el Y
proofend;

theorem :: BVFUNC26:58
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' (a 'nand' b) = ('not' a) 'or' b
proofend;

theorem :: BVFUNC26:59
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'nand' b) = a '&' ('not' b)
proofend;

theorem :: BVFUNC26:60
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'nand' b) = 'not' (a '&' b)
proofend;

theorem :: BVFUNC26:61
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'nand' b) = O_el Y
proofend;

theorem Th62: :: BVFUNC26:62
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)
proofend;

theorem Th63: :: BVFUNC26:63
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))
proofend;

theorem Th64: :: BVFUNC26:64
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)
proofend;

theorem Th65: :: BVFUNC26:65
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)))
proofend;

theorem Th66: :: BVFUNC26:66
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))
proofend;

theorem Th67: :: BVFUNC26:67
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
proofend;

theorem :: BVFUNC26:68
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'nor' b) = O_el Y
proofend;

theorem :: BVFUNC26:69
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' (a 'nor' b) = a 'or' ('not' b)
proofend;

theorem :: BVFUNC26:70
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' (a 'nor' b) = a 'or' ('not' b)
proofend;

theorem :: BVFUNC26:71
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'nor' b) = ('not' a) '&' b
proofend;

theorem :: BVFUNC26:72
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))
proofend;

theorem :: BVFUNC26:73
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'nor' b) = I_el Y
proofend;