:: BVFUNC26 semantic presentation

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) ) )
proof
deffunc H1( set ) ->  set = (p . $1) 'nand' (q . $1);
consider s being Function such that
A1: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in (dom p) /\ (dom q) holds
s . x = H1(x) ) ) from FUNCT_1:sch_3();
take  s ; ::_thesis: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) 'nand' (q . x) ) )
thus  ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) 'nand' (q . x) ) ) by A1; ::_thesis: verum
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
let s1, s2 be Function; ::_thesis: ( dom s1 = (dom p) /\ (dom q) & ( for x being set st x in dom s1 holds
s1 . x = (p . x) 'nand' (q . x) ) & dom s2 = (dom p) /\ (dom q) & ( for x being set st x in dom s2 holds
s2 . x = (p . x) 'nand' (q . x) ) implies s1 = s2 )
assume that
A2: dom s1 = (dom p) /\ (dom q) and
A3: for x being set st x in dom s1 holds
s1 . x = (p . x) 'nand' (q . x) and
A4: dom s2 = (dom p) /\ (dom q) and
A5: for x being set st x in dom s2 holds
s2 . x = (p . x) 'nand' (q . x) ; ::_thesis: s1 = s2
 for x being set st x in dom s1 holds
s1 . x = s2 . x
proof
let x be set ; ::_thesis: ( x in dom s1 implies s1 . x = s2 . x )
assume A6: x in dom s1 ; ::_thesis: s1 . x = s2 . x
then  s1 . x = (p . x) 'nand' (q . x) by A3;
hence  s1 . x = s2 . x by A2, A4, A5, A6; ::_thesis: verum
end;
hence  s1 = s2 by A2, A4, FUNCT_1:2; ::_thesis: verum
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) ) ) ;
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) ) )
proof
deffunc H1( set ) ->  set = (p . $1) 'nor' (q . $1);
consider s being Function such that
A7: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in (dom p) /\ (dom q) holds
s . x = H1(x) ) ) from FUNCT_1:sch_3();
take  s ; ::_thesis: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) 'nor' (q . x) ) )
thus  ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) 'nor' (q . x) ) ) by A7; ::_thesis: verum
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
let s1, s2 be Function; ::_thesis: ( dom s1 = (dom p) /\ (dom q) & ( for x being set st x in dom s1 holds
s1 . x = (p . x) 'nor' (q . x) ) & dom s2 = (dom p) /\ (dom q) & ( for x being set st x in dom s2 holds
s2 . x = (p . x) 'nor' (q . x) ) implies s1 = s2 )
assume that
A8: dom s1 = (dom p) /\ (dom q) and
A9: for x being set st x in dom s1 holds
s1 . x = (p . x) 'nor' (q . x) and
A10: dom s2 = (dom p) /\ (dom q) and
A11: for x being set st x in dom s2 holds
s2 . x = (p . x) 'nor' (q . x) ; ::_thesis: s1 = s2
 for x being set st x in dom s1 holds
s1 . x = s2 . x
proof
let x be set ; ::_thesis: ( x in dom s1 implies s1 . x = s2 . x )
assume A12: x in dom s1 ; ::_thesis: s1 . x = s2 . x
then  s1 . x = (p . x) 'nor' (q . x) by A9;
hence  s1 . x = s2 . x by A8, A10, A11, A12; ::_thesis: verum
end;
hence  s1 = s2 by A8, A10, FUNCT_1:2; ::_thesis: verum
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' 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
proof
let x be set ; :: according to TARSKI:def_3,MARGREL1:def_16 ::_thesis: ( not x in rng (p 'nand' q) or x in BOOLEAN )
assume  x in rng (p 'nand' q) ; ::_thesis: x in BOOLEAN
then consider y being set  such that
A1: ( y in dom (p 'nand' q) & x = (p 'nand' q) . y ) by FUNCT_1:def_3;
 x = (p . y) 'nand' (q . y) by A1, Def1;
then  ( x = FALSE or x = TRUE ) by XBOOLEAN:def_3;
hence  x in BOOLEAN ; ::_thesis: verum
end;
clusterp 'nor' q ->  boolean-valued ;
coherence
 p 'nor' q is boolean-valued
proof
let x be set ; :: according to TARSKI:def_3,MARGREL1:def_16 ::_thesis: ( not x in rng (p 'nor' q) or x in BOOLEAN )
assume  x in rng (p 'nor' q) ; ::_thesis: x in BOOLEAN
then consider y being set  such that
A2: ( y in dom (p 'nor' q) & x = (p 'nor' q) . y ) by FUNCT_1:def_3;
 x = (p . y) 'nor' (q . y) by A2, Def2;
then  ( x = FALSE or x = TRUE ) by XBOOLEAN:def_3;
hence  x in BOOLEAN ; ::_thesis: verum
end;
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
proof
 ( dom p = A & dom q = A ) by PARTFUN1:def_2;
then A1: dom (p 'nand' q) = A /\ A by Def1
.= A ;
 rng (p 'nand' q) c= BOOLEAN by MARGREL1:def_16;
hence  p 'nand' q is Function of A,BOOLEAN by A1, FUNCT_2:2; ::_thesis: verum
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
let IT be Function of A,BOOLEAN; ::_thesis: ( IT = p 'nand' q iff for x being Element of A holds IT . x = (p . x) 'nand' (q . x) )
A2: dom IT = A by FUNCT_2:def_1;
hereby  ::_thesis: ( ( for x being Element of A holds IT . x = (p . x) 'nand' (q . x) ) implies IT = p 'nand' q )
assume A3: IT = p 'nand' q ; ::_thesis: for x being Element of A holds IT . x = (p . x) 'nand' (q . x)
let x be Element of A; ::_thesis: IT . x = (p . x) 'nand' (q . x)
 ( dom p = A & dom q = A ) by FUNCT_2:def_1;
then  dom (p 'nand' q) = A /\ A by Def1
.= A ;
hence  IT . x = (p . x) 'nand' (q . x) by A3, Def1; ::_thesis: verum
end;
A4: dom q = A by FUNCT_2:def_1;
A5: dom IT = A /\ A by FUNCT_2:def_1
.= (dom p) /\ (dom q) by A4, FUNCT_2:def_1 ;
assume  for x being Element of A holds IT . x = (p . x) 'nand' (q . x) ; ::_thesis: IT = p 'nand' q
then  for x being set st x in dom IT holds
IT . x = (p . x) 'nand' (q . x) by A2;
hence  IT = p 'nand' q by A5, Def1; ::_thesis: verum
end;
:: 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
proof
 ( dom p = A & dom q = A ) by PARTFUN1:def_2;
then A6: dom (p 'nor' q) = A /\ A by Def2
.= A ;
 rng (p 'nor' q) c= BOOLEAN by MARGREL1:def_16;
hence  p 'nor' q is Function of A,BOOLEAN by A6, FUNCT_2:2; ::_thesis: verum
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
let IT be Function of A,BOOLEAN; ::_thesis: ( IT = p 'nor' q iff for x being Element of A holds IT . x = (p . x) 'nor' (q . x) )
A7: dom IT = A by FUNCT_2:def_1;
hereby  ::_thesis: ( ( for x being Element of A holds IT . x = (p . x) 'nor' (q . x) ) implies IT = p 'nor' q )
assume A8: IT = p 'nor' q ; ::_thesis: for x being Element of A holds IT . x = (p . x) 'nor' (q . x)
let x be Element of A; ::_thesis: IT . x = (p . x) 'nor' (q . x)
 ( dom p = A & dom q = A ) by FUNCT_2:def_1;
then  dom (p 'nor' q) = A /\ A by Def2
.= A ;
hence  IT . x = (p . x) 'nor' (q . x) by A8, Def2; ::_thesis: verum
end;
A9: dom q = A by FUNCT_2:def_1;
A10: dom IT = A /\ A by FUNCT_2:def_1
.= (dom p) /\ (dom q) by A9, FUNCT_2:def_1 ;
assume  for x being Element of A holds IT . x = (p . x) 'nor' (q . x) ; ::_thesis: IT = p 'nor' q
then  for x being set st x in dom IT holds
IT . x = (p . x) 'nor' (q . x) by A7;
hence  IT = p 'nor' q by A10, Def2; ::_thesis: verum
end;
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
proof
 a 'nand' b is Function of Y,BOOLEAN ;
hence  a 'nand' b is Function of Y,BOOLEAN ; ::_thesis: verum
end;
:: original: 'nor'
redefine funca 'nor' b ->  Function of Y,BOOLEAN;
coherence
 a 'nor' b is Function of Y,BOOLEAN
proof
 a 'nor' b is Function of Y,BOOLEAN ;
hence  a 'nor' b is Function of Y,BOOLEAN ; ::_thesis: verum
end;
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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nand' b = 'not' (a '&' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nand' b = 'not' (a '&' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'nand' b) . x = ('not' (a '&' b)) . x
thus ('not' (a '&' b)) . x = 'not' ((a '&' b) . x) by MARGREL1:def_19
.= 'not' ((a . x) '&' (b . x)) by MARGREL1:def_20
.= 'not' ('not' ((a . x) 'nand' (b . x))) by BVFUNC_1:46
.= (a 'nand' b) . x by Def3 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nor' b = 'not' (a 'or' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nor' b = 'not' (a 'or' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'nor' b) . x = ('not' (a 'or' b)) . x
thus ('not' (a 'or' b)) . x = 'not' ((a 'or' b) . x) by MARGREL1:def_19
.= 'not' ((a . x) 'or' (b . x)) by BVFUNC_1:def_4
.= 'not' ('not' ((a . x) 'nor' (b . x))) by BVFUNC_1:53
.= (a 'nor' b) . x by Def4 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (I_el Y) 'nand' a = 'not' a
let a be Function of Y,BOOLEAN; ::_thesis: (I_el Y) 'nand' a = 'not' a
 (I_el Y) 'nand' a = 'not' ((I_el Y) '&' a) by Th1;
hence  (I_el Y) 'nand' a = 'not' a by BVFUNC_1:6; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (O_el Y) 'nand' a = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: (O_el Y) 'nand' a = I_el Y
 ( (O_el Y) 'nand' a = 'not' ((O_el Y) '&' a) & (O_el Y) '&' a = O_el Y ) by Th1, BVFUNC_1:5;
hence  (O_el Y) 'nand' a = I_el Y by BVFUNC_1:2; ::_thesis: verum
end;

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 )
proof
let Y be non empty set ; ::_thesis: ( (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 )
thus  (O_el Y) 'nand' (O_el Y) = I_el Y by Th4; ::_thesis: ( (O_el Y) 'nand' (I_el Y) = I_el Y & (I_el Y) 'nand' (I_el Y) = O_el Y )
thus  (O_el Y) 'nand' (I_el Y) = I_el Y by Th4; ::_thesis: (I_el Y) 'nand' (I_el Y) = O_el Y
thus (I_el Y) 'nand' (I_el Y) = 'not' (I_el Y) by Th3
.= O_el Y by BVFUNC_1:2 ; ::_thesis: verum
end;

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 )
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds
( a 'nand' a = 'not' a & 'not' (a 'nand' a) = a )
let a be Function of Y,BOOLEAN; ::_thesis: ( a 'nand' a = 'not' a & 'not' (a 'nand' a) = a )
a 'nand' a = 'not' (a '&' a) by Th1
.= 'not' a ;
hence  ( a 'nand' a = 'not' a & 'not' (a 'nand' a) = a ) ; ::_thesis: verum
end;

theorem :: BVFUNC26:7
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'nand' b) = a '&' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds 'not' (a 'nand' b) = a '&' b
let a, b be Function of Y,BOOLEAN; ::_thesis: 'not' (a 'nand' b) = a '&' b
 'not' (a 'nand' b) = 'not' ('not' (a '&' b)) by Th1;
hence  'not' (a 'nand' b) = a '&' b ; ::_thesis: verum
end;

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 )
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds
( a 'nand' ('not' a) = I_el Y & 'not' (a 'nand' ('not' a)) = O_el Y )
let a be Function of Y,BOOLEAN; ::_thesis: ( a 'nand' ('not' a) = I_el Y & 'not' (a 'nand' ('not' a)) = O_el Y )
a 'nand' ('not' a) = 'not' (a '&' ('not' a)) by Th1
.= 'not' (O_el Y) by BVFUNC_4:5
.= I_el Y by BVFUNC_1:2 ;
hence  ( a 'nand' ('not' a) = I_el Y & 'not' (a 'nand' ('not' a)) = O_el Y ) by BVFUNC_1:2; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b '&' c) = 'not' ((a '&' b) '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nand' (b '&' c) = 'not' ((a '&' b) '&' c)
 a 'nand' (b '&' c) = 'not' (a '&' (b '&' c)) by Th1;
hence  a 'nand' (b '&' c) = 'not' ((a '&' b) '&' c) by BVFUNC_1:4; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b '&' c) = (a '&' b) 'nand' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nand' (b '&' c) = (a '&' b) 'nand' c
 (a '&' b) 'nand' c = 'not' ((a '&' b) '&' c) by Th1;
hence  a 'nand' (b '&' c) = (a '&' b) 'nand' c by Th9; ::_thesis: verum
end;

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))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b 'or' c) = ('not' (a '&' b)) '&' ('not' (a '&' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nand' (b 'or' c) = ('not' (a '&' b)) '&' ('not' (a '&' c))
thus a 'nand' (b 'or' c) = 'not' (a '&' (b 'or' c)) by Th1
.= 'not' ((a '&' b) 'or' (a '&' c)) by BVFUNC_1:12
.= ('not' (a '&' b)) '&' ('not' (a '&' c)) by BVFUNC_1:13 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b 'xor' c) = (a '&' b) 'eqv' (a '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nand' (b 'xor' c) = (a '&' b) 'eqv' (a '&' c)
thus a 'nand' (b 'xor' c) = 'not' (a '&' (b 'xor' c)) by Th1
.= 'not' ((a '&' b) 'xor' (a '&' c)) by BVFUNC25:11
.= 'not' ('not' ((a '&' b) 'eqv' (a '&' c))) by BVFUNC_8:12
.= (a '&' b) 'eqv' (a '&' c) ; ::_thesis: verum
end;

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) )
proof
let Y be non empty set ; ::_thesis: 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) )
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'nand' (b 'nand' c) = ('not' a) 'or' (b '&' c) & a 'nand' (b 'nand' c) = a 'imp' (b '&' c) )
a 'nand' (b 'nand' c) = 'not' (a '&' (b 'nand' c)) by Th1
.= 'not' (a '&' ('not' (b '&' c))) by Th1
.= ('not' a) 'or' ('not' ('not' (b '&' c))) by BVFUNC_1:14
.= ('not' a) 'or' (b '&' c) ;
hence  ( a 'nand' (b 'nand' c) = ('not' a) 'or' (b '&' c) & a 'nand' (b 'nand' c) = a 'imp' (b '&' c) ) by BVFUNC_4:8; ::_thesis: verum
end;

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) )
proof
let Y be non empty set ; ::_thesis: 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) )
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'nand' (b 'nor' c) = (('not' a) 'or' b) 'or' c & a 'nand' (b 'nor' c) = a 'imp' (b 'or' c) )
A1: a 'nand' (b 'nor' c) = 'not' (a '&' (b 'nor' c)) by Th1
.= 'not' (a '&' ('not' (b 'or' c))) by Th2
.= ('not' a) 'or' ('not' ('not' (b 'or' c))) by BVFUNC_1:14
.= (('not' a) 'or' b) 'or' c by BVFUNC_1:8 ;
then  a 'nand' (b 'nor' c) = ('not' a) 'or' (b 'or' c) by BVFUNC_1:8;
hence  ( a 'nand' (b 'nor' c) = (('not' a) 'or' b) 'or' c & a 'nand' (b 'nor' c) = a 'imp' (b 'or' c) ) by A1, BVFUNC_4:8; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b 'eqv' c) = a 'imp' (b 'xor' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nand' (b 'eqv' c) = a 'imp' (b 'xor' c)
a 'nand' (b 'eqv' c) = 'not' (a '&' (b 'eqv' c)) by Th1
.= ('not' a) 'or' ('not' (b 'eqv' c)) by BVFUNC_1:14
.= ('not' a) 'or' ('not' ('not' (b 'xor' c))) by BVFUNC25:12
.= ('not' a) 'or' (b 'xor' c) ;
hence  a 'nand' (b 'eqv' c) = a 'imp' (b 'xor' c) by BVFUNC_4:8; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nand' (a '&' b) = a 'nand' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nand' (a '&' b) = a 'nand' b
 a 'nand' (a '&' b) = (a '&' a) 'nand' b by Th10;
hence  a 'nand' (a '&' b) = a 'nand' b ; ::_thesis: verum
end;

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))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'or' b) = ('not' a) '&' ('not' (a '&' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nand' (a 'or' b) = ('not' a) '&' ('not' (a '&' b))
thus a 'nand' (a 'or' b) = ('not' (a '&' a)) '&' ('not' (a '&' b)) by Th11
.= ('not' a) '&' ('not' (a '&' b)) ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'eqv' b) = a 'imp' (a 'xor' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nand' (a 'eqv' b) = a 'imp' (a 'xor' b)
a 'nand' (a 'eqv' b) = 'not' (a '&' (a 'eqv' b)) by Th1
.= ('not' a) 'or' ('not' (a 'eqv' b)) by BVFUNC_1:14
.= ('not' a) 'or' ('not' ('not' (a 'xor' b))) by BVFUNC25:12
.= ('not' a) 'or' (a 'xor' b) ;
hence  a 'nand' (a 'eqv' b) = a 'imp' (a 'xor' b) by BVFUNC_4:8; ::_thesis: verum
end;

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 )
proof
let Y be non empty set ; ::_thesis: 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 )
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'nand' (a 'nand' b) = ('not' a) 'or' b & a 'nand' (a 'nand' b) = a 'imp' b )
a 'nand' (a 'nand' b) = 'not' (a '&' (a 'nand' b)) by Th1
.= 'not' (a '&' ('not' (a '&' b))) by Th1
.= ('not' a) 'or' ('not' ('not' (a '&' b))) by BVFUNC_1:14
.= (('not' a) 'or' a) '&' (('not' a) 'or' b) by BVFUNC_1:11
.= (I_el Y) '&' (('not' a) 'or' b) by BVFUNC_4:6
.= ('not' a) 'or' b by BVFUNC_1:6 ;
hence  ( a 'nand' (a 'nand' b) = ('not' a) 'or' b & a 'nand' (a 'nand' b) = a 'imp' b ) by BVFUNC_4:8; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'nor' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nand' (a 'nor' b) = I_el Y
thus a 'nand' (a 'nor' b) = 'not' (a '&' (a 'nor' b)) by Th1
.= 'not' (a '&' ('not' (a 'or' b))) by Th2
.= ('not' a) 'or' ('not' ('not' (a 'or' b))) by BVFUNC_1:14
.= (('not' a) 'or' a) 'or' b by BVFUNC_1:8
.= (I_el Y) 'or' b by BVFUNC_4:6
.= I_el Y by BVFUNC_1:10 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'eqv' b) = ('not' a) 'or' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nand' (a 'eqv' b) = ('not' a) 'or' ('not' b)
thus a 'nand' (a 'eqv' b) = 'not' (a '&' (a 'eqv' b)) by Th1
.= 'not' (a '&' ('not' (a 'xor' b))) by BVFUNC25:12
.= ('not' a) 'or' ('not' ('not' (a 'xor' b))) by BVFUNC_1:14
.= ('not' a) 'or' ((a 'or' b) '&' (('not' a) 'or' ('not' b))) by BVFUNC_8:13
.= (('not' a) 'or' (a 'or' b)) '&' (('not' a) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_1:11
.= ((('not' a) 'or' a) 'or' b) '&' (('not' a) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_1:8
.= ((I_el Y) 'or' b) '&' (('not' a) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_4:6
.= (I_el Y) '&' (('not' a) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_1:10
.= ('not' a) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:6
.= (('not' a) 'or' ('not' a)) 'or' ('not' b) by BVFUNC_1:8
.= ('not' a) 'or' ('not' b) ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' b = (a 'nand' b) 'nand' (a 'nand' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' b = (a 'nand' b) 'nand' (a 'nand' b)
thus (a 'nand' b) 'nand' (a 'nand' b) = 'not' ((a 'nand' b) '&' (a 'nand' b)) by Th1
.= (a '&' b) 'or' ('not' ('not' (a '&' b))) by Th1
.= a '&' b ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'nand' b) 'nand' (a 'nand' c) = a '&' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'nand' b) 'nand' (a 'nand' c) = a '&' (b 'or' c)
thus (a 'nand' b) 'nand' (a 'nand' c) = 'not' ((a 'nand' b) '&' (a 'nand' c)) by Th1
.= 'not' (('not' (a '&' b)) '&' (a 'nand' c)) by Th1
.= 'not' (('not' (a '&' b)) '&' ('not' (a '&' c))) by Th1
.= ('not' ('not' (a '&' b))) 'or' ('not' ('not' (a '&' c))) by BVFUNC_1:14
.= a '&' (b 'or' c) by BVFUNC_1:12 ; ::_thesis: verum
end;

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))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b 'imp' c) = (('not' a) 'or' b) '&' ('not' (a '&' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nand' (b 'imp' c) = (('not' a) 'or' b) '&' ('not' (a '&' c))
thus a 'nand' (b 'imp' c) = 'not' (a '&' (b 'imp' c)) by Th1
.= 'not' (a '&' (('not' b) 'or' c)) by BVFUNC_4:8
.= 'not' ((a '&' ('not' b)) 'or' (a '&' c)) by BVFUNC_1:12
.= ('not' (a '&' ('not' b))) '&' ('not' (a '&' c)) by BVFUNC_1:13
.= (('not' a) 'or' ('not' ('not' b))) '&' ('not' (a '&' c)) by BVFUNC_1:14
.= (('not' a) 'or' b) '&' ('not' (a '&' c)) ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'imp' b) = 'not' (a '&' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nand' (a 'imp' b) = 'not' (a '&' b)
thus a 'nand' (a 'imp' b) = (('not' a) 'or' a) '&' ('not' (a '&' b)) by Th24
.= (I_el Y) '&' ('not' (a '&' b)) by BVFUNC_4:6
.= 'not' (a '&' b) by BVFUNC_1:6 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (I_el Y) 'nor' a = O_el Y
let a be Function of Y,BOOLEAN; ::_thesis: (I_el Y) 'nor' a = O_el Y
thus (I_el Y) 'nor' a = 'not' ((I_el Y) 'or' a) by Th2
.= 'not' (I_el Y) by BVFUNC_1:10
.= O_el Y by BVFUNC_1:2 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (O_el Y) 'nor' a = 'not' a
let a be Function of Y,BOOLEAN; ::_thesis: (O_el Y) 'nor' a = 'not' a
thus (O_el Y) 'nor' a = 'not' ((O_el Y) 'or' a) by Th2
.= 'not' a by BVFUNC_1:9 ; ::_thesis: verum
end;

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 )
proof
let Y be non empty set ; ::_thesis: ( (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 )
thus (O_el Y) 'nor' (O_el Y) = 'not' (O_el Y) by Th27
.= I_el Y by BVFUNC_1:2 ; ::_thesis: ( (O_el Y) 'nor' (I_el Y) = O_el Y & (I_el Y) 'nor' (I_el Y) = O_el Y )
thus  (O_el Y) 'nor' (I_el Y) = O_el Y by Th26; ::_thesis: (I_el Y) 'nor' (I_el Y) = O_el Y
thus  (I_el Y) 'nor' (I_el Y) = O_el Y by Th26; ::_thesis: verum
end;

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 )
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds
( a 'nor' a = 'not' a & 'not' (a 'nor' a) = a )
let a be Function of Y,BOOLEAN; ::_thesis: ( a 'nor' a = 'not' a & 'not' (a 'nor' a) = a )
a 'nor' a = 'not' (a 'or' a) by Th2
.= 'not' a ;
hence  ( a 'nor' a = 'not' a & 'not' (a 'nor' a) = a ) ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds 'not' (a 'nor' b) = a 'or' b
let a, b be Function of Y,BOOLEAN; ::_thesis: 'not' (a 'nor' b) = a 'or' b
 'not' (a 'nor' b) = 'not' ('not' (a 'or' b)) by Th2;
hence  'not' (a 'nor' b) = a 'or' b ; ::_thesis: verum
end;

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 )
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds
( a 'nor' ('not' a) = O_el Y & 'not' (a 'nor' ('not' a)) = I_el Y )
let a be Function of Y,BOOLEAN; ::_thesis: ( a 'nor' ('not' a) = O_el Y & 'not' (a 'nor' ('not' a)) = I_el Y )
a 'nor' ('not' a) = 'not' (a 'or' ('not' a)) by Th2
.= 'not' (I_el Y) by BVFUNC_4:6
.= O_el Y by BVFUNC_1:2 ;
hence  ( a 'nor' ('not' a) = O_el Y & 'not' (a 'nor' ('not' a)) = I_el Y ) by BVFUNC_1:2; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ('not' a) '&' (a 'xor' b) = ('not' a) '&' b
let a, b be Function of Y,BOOLEAN; ::_thesis: ('not' a) '&' (a 'xor' b) = ('not' a) '&' b
thus ('not' a) '&' (a 'xor' b) = ('not' a) '&' ((('not' a) '&' b) 'or' (a '&' ('not' b))) by BVFUNC_4:9
.= (('not' a) '&' (('not' a) '&' b)) 'or' (('not' a) '&' (a '&' ('not' b))) by BVFUNC_1:12
.= ((('not' a) '&' ('not' a)) '&' b) 'or' (('not' a) '&' (a '&' ('not' b))) by BVFUNC_1:4
.= (('not' a) '&' b) 'or' ((('not' a) '&' a) '&' ('not' b)) by BVFUNC_1:4
.= (('not' a) '&' b) 'or' ((O_el Y) '&' ('not' b)) by BVFUNC_4:5
.= (('not' a) '&' b) 'or' (O_el Y) by BVFUNC_1:5
.= ('not' a) '&' b by BVFUNC_1:9 ; ::_thesis: verum
end;

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))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nor' (b '&' c) = ('not' (a 'or' b)) 'or' ('not' (a 'or' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nor' (b '&' c) = ('not' (a 'or' b)) 'or' ('not' (a 'or' c))
a 'nor' (b '&' c) = 'not' (a 'or' (b '&' c)) by Th2
.= 'not' ((a 'or' b) '&' (a 'or' c)) by BVFUNC_1:11 ;
hence  a 'nor' (b '&' c) = ('not' (a 'or' b)) 'or' ('not' (a 'or' c)) by BVFUNC_1:14; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nor' (b 'or' c) = 'not' ((a 'or' b) 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nor' (b 'or' c) = 'not' ((a 'or' b) 'or' c)
thus a 'nor' (b 'or' c) = 'not' (a 'or' (b 'or' c)) by Th2
.= 'not' ((a 'or' b) 'or' c) by BVFUNC_1:8 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nor' (b 'eqv' c) = ('not' a) '&' (b 'xor' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nor' (b 'eqv' c) = ('not' a) '&' (b 'xor' c)
thus a 'nor' (b 'eqv' c) = 'not' (a 'or' (b 'eqv' c)) by Th2
.= ('not' a) '&' ('not' (b 'eqv' c)) by BVFUNC_1:13
.= ('not' a) '&' ('not' ('not' (b 'xor' c))) by BVFUNC25:12
.= ('not' a) '&' (b 'xor' c) ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nor' (b 'imp' c) = (('not' a) '&' b) '&' ('not' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nor' (b 'imp' c) = (('not' a) '&' b) '&' ('not' c)
thus a 'nor' (b 'imp' c) = 'not' (a 'or' (b 'imp' c)) by Th2
.= ('not' a) '&' ('not' (b 'imp' c)) by BVFUNC_1:13
.= ('not' a) '&' (b '&' ('not' c)) by BVFUNC25:1
.= (('not' a) '&' b) '&' ('not' c) by BVFUNC_1:4 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nor' (b 'nand' c) = (('not' a) '&' b) '&' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nor' (b 'nand' c) = (('not' a) '&' b) '&' c
thus a 'nor' (b 'nand' c) = 'not' (a 'or' (b 'nand' c)) by Th2
.= 'not' (a 'or' ('not' (b '&' c))) by Th1
.= ('not' a) '&' ('not' ('not' (b '&' c))) by BVFUNC_1:13
.= (('not' a) '&' b) '&' c by BVFUNC_1:4 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nor' (b 'nor' c) = ('not' a) '&' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nor' (b 'nor' c) = ('not' a) '&' (b 'or' c)
thus a 'nor' (b 'nor' c) = 'not' (a 'or' (b 'nor' c)) by Th2
.= 'not' (a 'or' ('not' (b 'or' c))) by Th2
.= ('not' a) '&' ('not' ('not' (b 'or' c))) by BVFUNC_1:13
.= ('not' a) '&' (b 'or' c) ; ::_thesis: verum
end;

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))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nor' (a '&' b) = 'not' (a '&' (a 'or' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nor' (a '&' b) = 'not' (a '&' (a 'or' b))
thus a 'nor' (a '&' b) = ('not' (a 'or' a)) 'or' ('not' (a 'or' b)) by Th33
.= 'not' (a '&' (a 'or' b)) by BVFUNC_1:14 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'or' b) = 'not' (a 'or' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nor' (a 'or' b) = 'not' (a 'or' b)
thus a 'nor' (a 'or' b) = 'not' ((a 'or' a) 'or' b) by Th34
.= 'not' (a 'or' b) ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'eqv' b) = ('not' a) '&' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nor' (a 'eqv' b) = ('not' a) '&' b
thus a 'nor' (a 'eqv' b) = ('not' a) '&' (a 'xor' b) by Th35
.= ('not' a) '&' ((('not' a) '&' b) 'or' (a '&' ('not' b))) by BVFUNC_4:9
.= (('not' a) '&' (('not' a) '&' b)) 'or' (('not' a) '&' (a '&' ('not' b))) by BVFUNC_1:12
.= (('not' a) '&' (('not' a) '&' b)) 'or' ((('not' a) '&' a) '&' ('not' b)) by BVFUNC_1:4
.= (('not' a) '&' (('not' a) '&' b)) 'or' ((O_el Y) '&' ('not' b)) by BVFUNC_4:5
.= (('not' a) '&' (('not' a) '&' b)) 'or' (O_el Y) by BVFUNC_1:5
.= ('not' a) '&' (('not' a) '&' b) by BVFUNC_1:9
.= (('not' a) '&' ('not' a)) '&' b by BVFUNC_1:4
.= ('not' a) '&' b ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'imp' b) = O_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nor' (a 'imp' b) = O_el Y
thus a 'nor' (a 'imp' b) = (('not' a) '&' a) '&' ('not' b) by Th36
.= (O_el Y) '&' ('not' b) by BVFUNC_4:5
.= O_el Y by BVFUNC_1:5 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'nand' b) = O_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nor' (a 'nand' b) = O_el Y
thus a 'nor' (a 'nand' b) = (('not' a) '&' a) '&' b by Th37
.= (O_el Y) '&' b by BVFUNC_4:5
.= O_el Y by BVFUNC_1:5 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'nor' b) = ('not' a) '&' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nor' (a 'nor' b) = ('not' a) '&' b
thus a 'nor' (a 'nor' b) = ('not' a) '&' (a 'or' b) by Th38
.= (('not' a) '&' a) 'or' (('not' a) '&' b) by BVFUNC_1:12
.= (O_el Y) 'or' (('not' a) '&' b) by BVFUNC_4:5
.= ('not' a) '&' b by BVFUNC_1:9 ; ::_thesis: verum
end;

theorem :: BVFUNC26:45
for Y being non empty set holds (O_el Y) 'eqv' (O_el Y) = I_el Y
proof
let Y be non empty set ; ::_thesis: (O_el Y) 'eqv' (O_el Y) = I_el Y
thus (O_el Y) 'eqv' (O_el Y) = 'not' ((O_el Y) 'xor' (O_el Y)) by BVFUNC25:12
.= 'not' (O_el Y) by BVFUNC25:13
.= I_el Y by BVFUNC_1:2 ; ::_thesis: verum
end;

theorem :: BVFUNC26:46
for Y being non empty set holds (O_el Y) 'eqv' (I_el Y) = O_el Y
proof
let Y be non empty set ; ::_thesis: (O_el Y) 'eqv' (I_el Y) = O_el Y
thus (O_el Y) 'eqv' (I_el Y) = 'not' ((O_el Y) 'xor' (I_el Y)) by BVFUNC25:12
.= 'not' ((O_el Y) 'xor' ('not' (O_el Y))) by BVFUNC_1:2
.= 'not' (I_el Y) by BVFUNC25:14
.= O_el Y by BVFUNC_1:2 ; ::_thesis: verum
end;

theorem :: BVFUNC26:47
for Y being non empty set holds (I_el Y) 'eqv' (I_el Y) = I_el Y
proof
let Y be non empty set ; ::_thesis: (I_el Y) 'eqv' (I_el Y) = I_el Y
thus (I_el Y) 'eqv' (I_el Y) = 'not' ((I_el Y) 'xor' (I_el Y)) by BVFUNC25:12
.= 'not' ('not' (I_el Y)) by BVFUNC_8:14
.= I_el Y ; ::_thesis: verum
end;

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 )
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds
( a 'eqv' a = I_el Y & 'not' (a 'eqv' a) = O_el Y )
let a be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' a = I_el Y & 'not' (a 'eqv' a) = O_el Y )
a 'eqv' a = 'not' (a 'xor' a) by BVFUNC25:12
.= 'not' (O_el Y) by BVFUNC25:13
.= I_el Y by BVFUNC_1:2 ;
hence  ( a 'eqv' a = I_el Y & 'not' (a 'eqv' a) = O_el Y ) by BVFUNC_1:2; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'or' b) = a 'or' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' (a 'or' b) = a 'or' ('not' b)
thus a 'eqv' (a 'or' b) = 'not' (a 'xor' (a 'or' b)) by BVFUNC25:12
.= 'not' ((('not' a) '&' (a 'or' b)) 'or' (a '&' ('not' (a 'or' b)))) by BVFUNC_4:9
.= 'not' (((('not' a) '&' a) 'or' (('not' a) '&' b)) 'or' (a '&' ('not' (a 'or' b)))) by BVFUNC_1:12
.= 'not' (((O_el Y) 'or' (('not' a) '&' b)) 'or' (a '&' ('not' (a 'or' b)))) by BVFUNC_4:5
.= 'not' ((('not' a) '&' b) 'or' (a '&' ('not' (a 'or' b)))) by BVFUNC_1:9
.= 'not' ((('not' a) '&' b) 'or' (a '&' (('not' a) '&' ('not' b)))) by BVFUNC_1:13
.= 'not' ((('not' a) '&' b) 'or' ((a '&' ('not' a)) '&' ('not' b))) by BVFUNC_1:4
.= 'not' ((('not' a) '&' b) 'or' ((O_el Y) '&' ('not' b))) by BVFUNC_4:5
.= 'not' ((('not' a) '&' b) 'or' (O_el Y)) by BVFUNC_1:5
.= 'not' (('not' a) '&' b) by BVFUNC_1:9
.= ('not' ('not' a)) 'or' ('not' b) by BVFUNC_1:14
.= a 'or' ('not' b) ; ::_thesis: verum
end;

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))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a '&' (b 'nand' c) = (a '&' ('not' b)) 'or' (a '&' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a '&' (b 'nand' c) = (a '&' ('not' b)) 'or' (a '&' ('not' c))
thus a '&' (b 'nand' c) = a '&' ('not' (b '&' c)) by Th1
.= a '&' (('not' b) 'or' ('not' c)) by BVFUNC_1:14
.= (a '&' ('not' b)) 'or' (a '&' ('not' c)) by BVFUNC_1:12 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'or' (b 'nand' c) = (a 'or' ('not' b)) 'or' ('not' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'or' (b 'nand' c) = (a 'or' ('not' b)) 'or' ('not' c)
thus a 'or' (b 'nand' c) = a 'or' ('not' (b '&' c)) by Th1
.= a 'or' (('not' b) 'or' ('not' c)) by BVFUNC_1:14
.= (a 'or' ('not' b)) 'or' ('not' c) by BVFUNC_1:8 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'xor' (b 'nand' c) = (('not' a) '&' ('not' (b '&' c))) 'or' ((a '&' b) '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'xor' (b 'nand' c) = (('not' a) '&' ('not' (b '&' c))) 'or' ((a '&' b) '&' c)
thus a 'xor' (b 'nand' c) = a 'xor' ('not' (b '&' c)) by Th1
.= (('not' a) '&' ('not' (b '&' c))) 'or' (a '&' ('not' ('not' (b '&' c)))) by BVFUNC_4:9
.= (('not' a) '&' ('not' (b '&' c))) 'or' ((a '&' b) '&' c) by BVFUNC_1:4 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'eqv' (b 'nand' c) = (a '&' ('not' (b '&' c))) 'or' ((('not' a) '&' b) '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'eqv' (b 'nand' c) = (a '&' ('not' (b '&' c))) 'or' ((('not' a) '&' b) '&' c)
thus a 'eqv' (b 'nand' c) = a 'eqv' ('not' (b '&' c)) by Th1
.= (a '&' ('not' (b '&' c))) 'or' (('not' a) '&' ('not' ('not' (b '&' c)))) by BVFUNC_8:19
.= (a '&' ('not' (b '&' c))) 'or' ((('not' a) '&' b) '&' c) by BVFUNC_1:4 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'nand' c) = 'not' ((a '&' b) '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b 'nand' c) = 'not' ((a '&' b) '&' c)
thus a 'imp' (b 'nand' c) = a 'imp' ('not' (b '&' c)) by Th1
.= ('not' a) 'or' ('not' (b '&' c)) by BVFUNC_4:8
.= 'not' (a '&' (b '&' c)) by BVFUNC_1:14
.= 'not' ((a '&' b) '&' c) by BVFUNC_1:4 ; ::_thesis: verum
end;

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))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nor' (b 'nand' c) = 'not' ((a 'or' ('not' b)) 'or' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nor' (b 'nand' c) = 'not' ((a 'or' ('not' b)) 'or' ('not' c))
thus a 'nor' (b 'nand' c) = a 'nor' ('not' (b '&' c)) by Th1
.= 'not' (a 'or' ('not' (b '&' c))) by Th2
.= 'not' (a 'or' (('not' b) 'or' ('not' c))) by BVFUNC_1:14
.= 'not' ((a 'or' ('not' b)) 'or' ('not' c)) by BVFUNC_1:8 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' (a 'nand' b) = a '&' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' (a 'nand' b) = a '&' ('not' b)
thus a '&' (a 'nand' b) = (a '&' ('not' a)) 'or' (a '&' ('not' b)) by Th50
.= (O_el Y) 'or' (a '&' ('not' b)) by BVFUNC_4:5
.= a '&' ('not' b) by BVFUNC_1:9 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' (a 'nand' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' (a 'nand' b) = I_el Y
thus a 'or' (a 'nand' b) = (a 'or' ('not' a)) 'or' ('not' b) by Th51
.= (I_el Y) 'or' ('not' b) by BVFUNC_4:6
.= I_el Y by BVFUNC_1:10 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'xor' (a 'nand' b) = ('not' a) 'or' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'xor' (a 'nand' b) = ('not' a) 'or' b
thus a 'xor' (a 'nand' b) = (('not' a) '&' ('not' (a '&' b))) 'or' ((a '&' a) '&' b) by Th52
.= (('not' a) 'or' (a '&' b)) '&' (('not' (a '&' b)) 'or' (a '&' b)) by BVFUNC_1:11
.= (('not' a) 'or' (a '&' b)) '&' (I_el Y) by BVFUNC_4:6
.= ('not' a) 'or' (a '&' b) by BVFUNC_1:6
.= (('not' a) 'or' a) '&' (('not' a) 'or' b) by BVFUNC_1:11
.= (I_el Y) '&' (('not' a) 'or' b) by BVFUNC_4:6
.= ('not' a) 'or' b by BVFUNC_1:6 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'nand' b) = a '&' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' (a 'nand' b) = a '&' ('not' b)
thus a 'eqv' (a 'nand' b) = (a '&' ('not' (a '&' b))) 'or' ((('not' a) '&' a) '&' b) by Th53
.= (a '&' ('not' (a '&' b))) 'or' ((O_el Y) '&' b) by BVFUNC_4:5
.= (a '&' ('not' (a '&' b))) 'or' (O_el Y) by BVFUNC_1:5
.= a '&' ('not' (a '&' b)) by BVFUNC_1:9
.= a '&' (('not' a) 'or' ('not' b)) by BVFUNC_1:14
.= (a '&' ('not' a)) 'or' (a '&' ('not' b)) by BVFUNC_1:12
.= (O_el Y) 'or' (a '&' ('not' b)) by BVFUNC_4:5
.= a '&' ('not' b) by BVFUNC_1:9 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'nand' b) = 'not' (a '&' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' (a 'nand' b) = 'not' (a '&' b)
thus a 'imp' (a 'nand' b) = 'not' ((a '&' a) '&' b) by Th54
.= 'not' (a '&' b) ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nor' (a 'nand' b) = O_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nor' (a 'nand' b) = O_el Y
thus a 'nor' (a 'nand' b) = 'not' ((a 'or' ('not' a)) 'or' ('not' b)) by Th55
.= 'not' ((I_el Y) 'or' ('not' b)) by BVFUNC_4:6
.= 'not' (I_el Y) by BVFUNC_1:10
.= O_el Y by BVFUNC_1:2 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a '&' (b 'nor' c) = (a '&' ('not' b)) '&' ('not' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a '&' (b 'nor' c) = (a '&' ('not' b)) '&' ('not' c)
thus a '&' (b 'nor' c) = a '&' ('not' (b 'or' c)) by Th2
.= a '&' (('not' b) '&' ('not' c)) by BVFUNC_1:13
.= (a '&' ('not' b)) '&' ('not' c) by BVFUNC_1:4 ; ::_thesis: verum
end;

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))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'or' (b 'nor' c) = (a 'or' ('not' b)) '&' (a 'or' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'or' (b 'nor' c) = (a 'or' ('not' b)) '&' (a 'or' ('not' c))
thus a 'or' (b 'nor' c) = a 'or' ('not' (b 'or' c)) by Th2
.= a 'or' (('not' b) '&' ('not' c)) by BVFUNC_1:13
.= (a 'or' ('not' b)) '&' (a 'or' ('not' c)) by BVFUNC_1:11 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: 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)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'xor' (b 'nor' c) = (a 'or' ('not' (b 'or' c))) '&' ((('not' a) 'or' b) 'or' c)
thus a 'xor' (b 'nor' c) = a 'xor' ('not' (b 'or' c)) by Th2
.= (a 'or' ('not' (b 'or' c))) '&' (('not' a) 'or' ('not' ('not' (b 'or' c)))) by BVFUNC_8:13
.= (a 'or' ('not' (b 'or' c))) '&' ((('not' a) 'or' b) 'or' c) by BVFUNC_1:8 ; ::_thesis: verum
end;

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)))
proof
let Y be non empty set ; ::_thesis: 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)))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'eqv' (b 'nor' c) = ((a 'or' b) 'or' c) '&' (('not' a) 'or' ('not' (b 'or' c)))
thus a 'eqv' (b 'nor' c) = a 'eqv' ('not' (b 'or' c)) by Th2
.= (a 'or' ('not' ('not' (b 'or' c)))) '&' (('not' a) 'or' ('not' (b 'or' c))) by BVFUNC_8:18
.= ((a 'or' b) 'or' c) '&' (('not' a) 'or' ('not' (b 'or' c))) by BVFUNC_1:8 ; ::_thesis: verum
end;

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))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'nor' c) = 'not' (a '&' (b 'or' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b 'nor' c) = 'not' (a '&' (b 'or' c))
thus a 'imp' (b 'nor' c) = a 'imp' ('not' (b 'or' c)) by Th2
.= ('not' a) 'or' ('not' (b 'or' c)) by BVFUNC_4:8
.= 'not' (a '&' (b 'or' c)) by BVFUNC_1:14 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'nand' (b 'nor' c) = (('not' a) 'or' b) 'or' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'nand' (b 'nor' c) = (('not' a) 'or' b) 'or' c
thus a 'nand' (b 'nor' c) = a 'nand' ('not' (b 'or' c)) by Th2
.= 'not' (a '&' ('not' (b 'or' c))) by Th1
.= ('not' a) 'or' ('not' ('not' (b 'or' c))) by BVFUNC_1:14
.= (('not' a) 'or' b) 'or' c by BVFUNC_1:8 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' (a 'nor' b) = O_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' (a 'nor' b) = O_el Y
thus a '&' (a 'nor' b) = (a '&' ('not' a)) '&' ('not' b) by Th62
.= (O_el Y) '&' ('not' b) by BVFUNC_4:5
.= O_el Y by BVFUNC_1:5 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' (a 'nor' b) = a 'or' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' (a 'nor' b) = a 'or' ('not' b)
thus a 'or' (a 'nor' b) = (a 'or' ('not' a)) '&' (a 'or' ('not' b)) by Th63
.= (I_el Y) '&' (a 'or' ('not' b)) by BVFUNC_4:6
.= a 'or' ('not' b) by BVFUNC_1:6 ; ::_thesis: verum
end;

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)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'xor' (a 'nor' b) = a 'or' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'xor' (a 'nor' b) = a 'or' ('not' b)
thus a 'xor' (a 'nor' b) = (a 'or' ('not' (a 'or' b))) '&' ((('not' a) 'or' a) 'or' b) by Th64
.= (a 'or' ('not' (a 'or' b))) '&' ((I_el Y) 'or' b) by BVFUNC_4:6
.= (a 'or' ('not' (a 'or' b))) '&' (I_el Y) by BVFUNC_1:10
.= a 'or' ('not' (a 'or' b)) by BVFUNC_1:6
.= a 'or' (('not' a) '&' ('not' b)) by BVFUNC_1:13
.= (a 'or' ('not' a)) '&' (a 'or' ('not' b)) by BVFUNC_1:11
.= (I_el Y) '&' (a 'or' ('not' b)) by BVFUNC_4:6
.= a 'or' ('not' b) by BVFUNC_1:6 ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'nor' b) = ('not' a) '&' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' (a 'nor' b) = ('not' a) '&' b
thus a 'eqv' (a 'nor' b) = ((a 'or' a) 'or' b) '&' (('not' a) 'or' ('not' (a 'or' b))) by Th65
.= ((a 'or' b) '&' ('not' a)) 'or' ((a 'or' b) '&' ('not' (a 'or' b))) by BVFUNC_1:12
.= ((a 'or' b) '&' ('not' a)) 'or' (O_el Y) by BVFUNC_4:5
.= (a 'or' b) '&' ('not' a) by BVFUNC_1:9
.= (a '&' ('not' a)) 'or' (b '&' ('not' a)) by BVFUNC_1:12
.= (O_el Y) 'or' (b '&' ('not' a)) by BVFUNC_4:5
.= ('not' a) '&' b by BVFUNC_1:9 ; ::_thesis: verum
end;

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))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'nor' b) = 'not' (a 'or' (a '&' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' (a 'nor' b) = 'not' (a 'or' (a '&' b))
thus a 'imp' (a 'nor' b) = 'not' (a '&' (a 'or' b)) by Th66
.= 'not' ((a '&' a) 'or' (a '&' b)) by BVFUNC_1:12
.= 'not' (a 'or' (a '&' b)) ; ::_thesis: verum
end;

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
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'nand' (a 'nor' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'nand' (a 'nor' b) = I_el Y
thus a 'nand' (a 'nor' b) = (('not' a) 'or' a) 'or' b by Th67
.= (I_el Y) 'or' b by BVFUNC_4:6
.= I_el Y by BVFUNC_1:10 ; ::_thesis: verum
end;