:: BVFUNC26 semantic presentation

definition
let c1, c2 be boolean-valued Function;
func a1 'nand' a2 -> Function means :E1: :: BVFUNC26:def 1
( dom a3 = (dom a1) /\ (dom a2) & for b1 being set holds
( b1 in dom a3 implies a3 . b1 = (a1 . b1) 'nand' (a2 . b1) ) );
existence
ex b1 being Function st
( dom b1 = (dom c1) /\ (dom c2) & for b2 being set holds
( b2 in dom b1 implies b1 . b2 = (c1 . b2) 'nand' (c2 . b2) ) )
proof
deffunc H1( set ) -> set = (c1 . a1) 'nand' (c2 . a1);
consider c3 being Function such that
E1: dom c3 = (dom c1) /\ (dom c2)
and E2: for b1 being set holds
( b1 in (dom c1) /\ (dom c2) implies c3 . b1 = H1(b1) ) from FUNCT_1:sch 3();
 take c3 ;
thus ( dom c3 = (dom c1) /\ (dom c2) & for b1 being set holds
( b1 in dom c3 implies c3 . b1 = (c1 . b1) 'nand' (c2 . b1) ) ) by E1, E2;
end;
uniqueness
for b1, b2 being Function holds
( ( dom b1 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b1 implies b1 . b3 = (c1 . b3) 'nand' (c2 . b3) ) & dom b2 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b2 implies b2 . b3 = (c1 . b3) 'nand' (c2 . b3) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Function;
assume that E1: dom c3 = (dom c1) /\ (dom c2)
and E2: for b1 being set holds
( b1 in dom c3 implies c3 . b1 = (c1 . b1) 'nand' (c2 . b1) )
and E3: dom c4 = (dom c1) /\ (dom c2)
and E4: for b1 being set holds
( b1 in dom c4 implies c4 . b1 = (c1 . b1) 'nand' (c2 . b1) ) ;
for b1 being set holds
( b1 in dom c3 implies c3 . b1 = c4 . b1 )
proof
let c5 be set ;
assume c5 in dom c3 ;
then ( c3 . c5 = (c1 . c5) 'nand' (c2 . c5) & c4 . c5 = (c1 . c5) 'nand' (c2 . c5) ) by E1, E2, E3, E4;
hence c3 . c5 = c4 . c5 ;
end;
hence c3 = c4 by E1, E3, FUNCT_1:9;
end;
commutativity
for b1 being Function
for b2, b3 being boolean-valued Function holds
( ( dom b1 = (dom b2) /\ (dom b3) & for b4 being set holds
( b4 in dom b1 implies b1 . b4 = (b2 . b4) 'nand' (b3 . b4) ) ) implies ( ( dom b1 = (dom b3) /\ (dom b2) & for b4 being set holds
( b4 in dom b1 implies b1 . b4 = (b3 . b4) 'nand' (b2 . b4) ) ) ) ) ;
func a1 'nor' a2 -> Function means :E2: :: BVFUNC26:def 2
( dom a3 = (dom a1) /\ (dom a2) & for b1 being set holds
( b1 in dom a3 implies a3 . b1 = (a1 . b1) 'nor' (a2 . b1) ) );
existence
ex b1 being Function st
( dom b1 = (dom c1) /\ (dom c2) & for b2 being set holds
( b2 in dom b1 implies b1 . b2 = (c1 . b2) 'nor' (c2 . b2) ) )
proof
deffunc H1( set ) -> set = (c1 . a1) 'nor' (c2 . a1);
consider c3 being Function such that
E1: dom c3 = (dom c1) /\ (dom c2)
and E2: for b1 being set holds
( b1 in (dom c1) /\ (dom c2) implies c3 . b1 = H1(b1) ) from FUNCT_1:sch 3();
 take c3 ;
thus ( dom c3 = (dom c1) /\ (dom c2) & for b1 being set holds
( b1 in dom c3 implies c3 . b1 = (c1 . b1) 'nor' (c2 . b1) ) ) by E1, E2;
end;
uniqueness
for b1, b2 being Function holds
( ( dom b1 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b1 implies b1 . b3 = (c1 . b3) 'nor' (c2 . b3) ) & dom b2 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b2 implies b2 . b3 = (c1 . b3) 'nor' (c2 . b3) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Function;
assume that E1: dom c3 = (dom c1) /\ (dom c2)
and E2: for b1 being set holds
( b1 in dom c3 implies c3 . b1 = (c1 . b1) 'nor' (c2 . b1) )
and E3: dom c4 = (dom c1) /\ (dom c2)
and E4: for b1 being set holds
( b1 in dom c4 implies c4 . b1 = (c1 . b1) 'nor' (c2 . b1) ) ;
for b1 being set holds
( b1 in dom c3 implies c3 . b1 = c4 . b1 )
proof
let c5 be set ;
assume c5 in dom c3 ;
then ( c3 . c5 = (c1 . c5) 'nor' (c2 . c5) & c4 . c5 = (c1 . c5) 'nor' (c2 . c5) ) by E1, E2, E3, E4;
hence c3 . c5 = c4 . c5 ;
end;
hence c3 = c4 by E1, E3, FUNCT_1:9;
end;
commutativity
for b1 being Function
for b2, b3 being boolean-valued Function holds
( ( dom b1 = (dom b2) /\ (dom b3) & for b4 being set holds
( b4 in dom b1 implies b1 . b4 = (b2 . b4) 'nor' (b3 . b4) ) ) implies ( ( dom b1 = (dom b3) /\ (dom b2) & for b4 being set holds
( b4 in dom b1 implies b1 . b4 = (b3 . b4) 'nor' (b2 . b4) ) ) ) ) ;
end;

:: deftheorem E1 defines 'nand' BVFUNC26:def 1 :
for b1, b2 being boolean-valued Function
for b3 being Function holds
( b3 = b1 'nand' b2 iff ( dom b3 = (dom b1) /\ (dom b2) & for b4 being set holds
( b4 in dom b3 implies b3 . b4 = (b1 . b4) 'nand' (b2 . b4) ) ) );

:: deftheorem E2 defines 'nor' BVFUNC26:def 2 :
for b1, b2 being boolean-valued Function
for b3 being Function holds
( b3 = b1 'nor' b2 iff ( dom b3 = (dom b1) /\ (dom b2) & for b4 being set holds
( b4 in dom b3 implies b3 . b4 = (b1 . b4) 'nor' (b2 . b4) ) ) );

registration
let c1, c2 be boolean-valued Function;
cluster a1 'nand' a2 -> boolean-valued ;
coherence
c1 'nand' c2 is boolean-valued
proof
let c3 be set ; :: uses TARSKI:def 3,VALUAT_1:def 2
assume c3 in rng (c1 'nand' c2) ;
then consider c4 being set such that
E3: c4 in dom (c1 'nand' c2)
and E4: c3 = (c1 'nand' c2) . c4 by FUNCT_1:def 5;
c3 = (c1 . c4) 'nand' (c2 . c4) by E3, E4, E1;
then ( c3 = FALSE or c3 = TRUE ) by MARGREL1:39;
hence c3 in BOOLEAN ;
end;
cluster a1 'nor' a2 -> boolean-valued ;
coherence
c1 'nor' c2 is boolean-valued
proof
let c3 be set ; :: uses TARSKI:def 3,VALUAT_1:def 2
assume c3 in rng (c1 'nor' c2) ;
then consider c4 being set such that
E3: c4 in dom (c1 'nor' c2)
and E4: c3 = (c1 'nor' c2) . c4 by FUNCT_1:def 5;
c3 = (c1 . c4) 'nor' (c2 . c4) by E3, E4, E2;
then ( c3 = FALSE or c3 = TRUE ) by MARGREL1:39;
hence c3 in BOOLEAN ;
end;
end;

definition
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
redefine func 'nand' as a2 'nand' a3 -> Element of Funcs a1,BOOLEAN means :E3: :: BVFUNC26:def 3
for b1 being Element of a1 holds a4 . b1 = (a2 . b1) 'nand' (a3 . b1);
coherence
c2 'nand' c3 is Element of Funcs c1,BOOLEAN
proof
E3: ex b1 being Function st
( c2 = b1 & dom b1 = c1 & rng b1 c= BOOLEAN ) by FUNCT_2:def 2;
ex b1 being Function st
( c3 = b1 & dom b1 = c1 & rng b1 c= BOOLEAN ) by FUNCT_2:def 2;
then E4: dom (c2 'nand' c3) = c1 /\ c1 by E3, E1
.= c1 ;
rng (c2 'nand' c3) c= BOOLEAN by VALUAT_1:def 2;
hence c2 'nand' c3 is Element of Funcs c1,BOOLEAN by E4, FUNCT_2:def 2;
end;
compatibility
for b1 being Element of Funcs c1,BOOLEAN holds
( b1 = c2 'nand' c3 iff for b2 being Element of c1 holds b1 . b2 = (c2 . b2) 'nand' (c3 . b2) )
proof
let c4 be Element of Funcs c1,BOOLEAN ;
hereby
assume E3: c4 = c2 'nand' c3 ;
let c5 be Element of c1;
E4: dom c2 = c1 by FUNCT_2:def 1;
dom c3 = c1 by FUNCT_2:def 1;
then dom (c2 'nand' c3) = c1 /\ c1 by E4, E1
.= c1 ;
hence c4 . c5 = (c2 . c5) 'nand' (c3 . c5) by E3, E1;
end; assume E3: for b1 being Element of c1 holds c4 . b1 = (c2 . b1) 'nand' (c3 . b1) ;
E4: dom c4 = c1 by FUNCT_2:def 1;
E5: dom c3 = c1 by FUNCT_2:def 1;
E6: dom c4 = c1 /\ c1 by FUNCT_2:def 1
.= (dom c2) /\ (dom c3) by E5, FUNCT_2:def 1 ;
for b1 being set holds
( b1 in dom c4 implies c4 . b1 = (c2 . b1) 'nand' (c3 . b1) ) by E3, E4;
hence c4 = c2 'nand' c3 by E6, E1;
end;
redefine func 'nor' as a2 'nor' a3 -> Element of Funcs a1,BOOLEAN means :E4: :: BVFUNC26:def 4
for b1 being Element of a1 holds a4 . b1 = (a2 . b1) 'nor' (a3 . b1);
coherence
c2 'nor' c3 is Element of Funcs c1,BOOLEAN
proof
E3: ex b1 being Function st
( c2 = b1 & dom b1 = c1 & rng b1 c= BOOLEAN ) by FUNCT_2:def 2;
ex b1 being Function st
( c3 = b1 & dom b1 = c1 & rng b1 c= BOOLEAN ) by FUNCT_2:def 2;
then E4: dom (c2 'nor' c3) = c1 /\ c1 by E3, E2
.= c1 ;
rng (c2 'nor' c3) c= BOOLEAN by VALUAT_1:def 2;
hence c2 'nor' c3 is Element of Funcs c1,BOOLEAN by E4, FUNCT_2:def 2;
end;
compatibility
for b1 being Element of Funcs c1,BOOLEAN holds
( b1 = c2 'nor' c3 iff for b2 being Element of c1 holds b1 . b2 = (c2 . b2) 'nor' (c3 . b2) )
proof
let c4 be Element of Funcs c1,BOOLEAN ;
hereby
assume E3: c4 = c2 'nor' c3 ;
let c5 be Element of c1;
E4: dom c2 = c1 by FUNCT_2:def 1;
dom c3 = c1 by FUNCT_2:def 1;
then dom (c2 'nor' c3) = c1 /\ c1 by E4, E2
.= c1 ;
hence c4 . c5 = (c2 . c5) 'nor' (c3 . c5) by E3, E2;
end; assume E3: for b1 being Element of c1 holds c4 . b1 = (c2 . b1) 'nor' (c3 . b1) ;
E4: dom c4 = c1 by FUNCT_2:def 1;
E5: dom c3 = c1 by FUNCT_2:def 1;
E6: dom c4 = c1 /\ c1 by FUNCT_2:def 1
.= (dom c2) /\ (dom c3) by E5, FUNCT_2:def 1 ;
for b1 being set holds
( b1 in dom c4 implies c4 . b1 = (c2 . b1) 'nor' (c3 . b1) ) by E3, E4;
hence c4 = c2 'nor' c3 by E6, E2;
end;
end;

:: deftheorem E3 defines 'nand' BVFUNC26:def 3 :
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( b4 = b2 'nand' b3 iff for b5 being Element of b1 holds b4 . b5 = (b2 . b5) 'nand' (b3 . b5) );

:: deftheorem E4 defines 'nor' BVFUNC26:def 4 :
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( b4 = b2 'nor' b3 iff for b5 being Element of b1 holds b4 . b5 = (b2 . b5) 'nor' (b3 . b5) );

definition
let c1 be non empty set ;
let c2, c3 be Element of BVF c1;
redefine func 'nand' as a2 'nand' a3 -> Element of BVF a1;
coherence
c2 'nand' c3 is Element of BVF c1
proof
reconsider c4 = c2, c5 = c3 as Element of Funcs c1,BOOLEAN by BVFUNC_1:def 4;
c4 'nand' c5 is Element of Funcs c1,BOOLEAN ;
hence c2 'nand' c3 is Element of BVF c1 by BVFUNC_1:def 4;
end;
redefine func 'nor' as a2 'nor' a3 -> Element of BVF a1;
coherence
c2 'nor' c3 is Element of BVF c1
proof
reconsider c4 = c2, c5 = c3 as Element of Funcs c1,BOOLEAN by BVFUNC_1:def 4;
c4 'nor' c5 is Element of Funcs c1,BOOLEAN ;
hence c2 'nor' c3 is Element of BVF c1 by BVFUNC_1:def 4;
end;
end;

theorem E5: :: BVFUNC26:1
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'nand' b3 = 'not' (b2 '&' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E6: for b1 being Element of c1 holds (c2 'nand' c3) . b1 = ('not' (c2 '&' c3)) . b1
proof
let c4 be Element of c1;
thus ('not' (c2 '&' c3)) . c4 = 'not' ((c2 '&' c3) . c4) by VALUAT_1:def 5
.= 'not' ((c2 . c4) '&' (c3 . c4)) by VALUAT_1:def 6
.= 'not' ('not' ((c2 . c4) 'nand' (c3 . c4))) by BINARI_5:4
.= (c2 . c4) 'nand' (c3 . c4) by MARGREL1:40
.= (c2 'nand' c3) . c4 by E3 ;
end;
consider c4 being Function such that
E7: ( c2 'nand' c3 = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
consider c5 being Function such that
E8: ( 'not' (c2 '&' c3) = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in c1 implies c4 . b1 = c5 . b1 ) by E6, E7, E8;
hence c2 'nand' c3 = 'not' (c2 '&' c3) by E7, E8, FUNCT_1:9;
end;

theorem E6: :: BVFUNC26:2
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'nor' b3 = 'not' (b2 'or' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E7: for b1 being Element of c1 holds (c2 'nor' c3) . b1 = ('not' (c2 'or' c3)) . b1
proof
let c4 be Element of c1;
thus ('not' (c2 'or' c3)) . c4 = 'not' ((c2 'or' c3) . c4) by VALUAT_1:def 5
.= 'not' ((c2 . c4) 'or' (c3 . c4)) by BVFUNC_1:def 7
.= 'not' ('not' ((c2 . c4) 'nor' (c3 . c4))) by BINARI_5:13
.= (c2 . c4) 'nor' (c3 . c4) by MARGREL1:40
.= (c2 'nor' c3) . c4 by E4 ;
end;
consider c4 being Function such that
E8: ( c2 'nor' c3 = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
consider c5 being Function such that
E9: ( 'not' (c2 'or' c3) = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in c1 implies c4 . b1 = c5 . b1 ) by E7, E8, E9;
hence c2 'nor' c3 = 'not' (c2 'or' c3) by E8, E9, FUNCT_1:9;
end;

theorem E7: :: BVFUNC26:3
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds (I_el b1) 'nand' b2 = 'not' b2
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
(I_el c1) 'nand' c2 = 'not' ((I_el c1) '&' c2) by E5;
hence (I_el c1) 'nand' c2 = 'not' c2 by BVFUNC_1:9;
end;

theorem E8: :: BVFUNC26:4
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds (O_el b1) 'nand' b2 = I_el b1
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
E9: (O_el c1) 'nand' c2 = 'not' ((O_el c1) '&' c2) by E5;
(O_el c1) '&' c2 = O_el c1 by BVFUNC_1:8;
hence (O_el c1) 'nand' c2 = I_el c1 by E9, BVFUNC_1:5;
end;

theorem :: BVFUNC26:5
for b1 being non empty set holds
( (O_el b1) 'nand' (O_el b1) = I_el b1 & (O_el b1) 'nand' (I_el b1) = I_el b1 & (I_el b1) 'nand' (I_el b1) = O_el b1 )
proof
let c1 be non empty set ;
thus (O_el c1) 'nand' (O_el c1) = I_el c1 by E8;
thus (O_el c1) 'nand' (I_el c1) = I_el c1 by E8;
thus (I_el c1) 'nand' (I_el c1) = 'not' (I_el c1) by E7
.= O_el c1 by BVFUNC_1:5 ;
end;

theorem :: BVFUNC26:6
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds
( b2 'nand' b2 = 'not' b2 & 'not' (b2 'nand' b2) = b2 )
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
c2 'nand' c2 = 'not' (c2 '&' c2) by E5
.= 'not' c2 by BVFUNC_1:6 ;
hence ( c2 'nand' c2 = 'not' c2 & 'not' (c2 'nand' c2) = c2 ) by BVFUNC_1:4;
end;

theorem :: BVFUNC26:7
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds 'not' (b2 'nand' b3) = b2 '&' b3
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
'not' (c2 'nand' c3) = 'not' ('not' (c2 '&' c3)) by E5;
hence 'not' (c2 'nand' c3) = c2 '&' c3 by BVFUNC_1:4;
end;

theorem :: BVFUNC26:8
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds
( b2 'nand' ('not' b2) = I_el b1 & 'not' (b2 'nand' ('not' b2)) = O_el b1 )
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
c2 'nand' ('not' c2) = 'not' (c2 '&' ('not' c2)) by E5
.= 'not' (O_el c1) by BVFUNC_4:5
.= I_el c1 by BVFUNC_1:5 ;
hence ( c2 'nand' ('not' c2) = I_el c1 & 'not' (c2 'nand' ('not' c2)) = O_el c1 ) by BVFUNC_1:5;
end;

theorem E9: :: BVFUNC26:9
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'nand' (b3 '&' b4) = 'not' ((b2 '&' b3) '&' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
c2 'nand' (c3 '&' c4) = 'not' (c2 '&' (c3 '&' c4)) by E5;
hence c2 'nand' (c3 '&' c4) = 'not' ((c2 '&' c3) '&' c4) by BVFUNC_1:7;
end;

theorem E10: :: BVFUNC26:10
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'nand' (b3 '&' b4) = (b2 '&' b3) 'nand' b4
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
(c2 '&' c3) 'nand' c4 = 'not' ((c2 '&' c3) '&' c4) by E5;
hence c2 'nand' (c3 '&' c4) = (c2 '&' c3) 'nand' c4 by E9;
end;

theorem E11: :: BVFUNC26:11
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'nand' (b3 'or' b4) = ('not' (b2 '&' b3)) '&' ('not' (b2 '&' b4))
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
thus c2 'nand' (c3 'or' c4) = 'not' (c2 '&' (c3 'or' c4)) by E5
.= 'not' ((c2 '&' c3) 'or' (c2 '&' c4)) by BVFUNC_1:15
.= ('not' (c2 '&' c3)) '&' ('not' (c2 '&' c4)) by BVFUNC_1:16 ;
end;

theorem :: BVFUNC26:12
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'nand' (b3 'xor' b4) = (b2 '&' b3) 'eqv' (b2 '&' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
thus c2 'nand' (c3 'xor' c4) = 'not' (c2 '&' (c3 'xor' c4)) by E5
.= 'not' ((c2 '&' c3) 'xor' (c2 '&' c4)) by BVFUNC25:11
.= 'not' ('not' ((c2 '&' c3) 'eqv' (c2 '&' c4))) by BVFUNC_8:12
.= (c2 '&' c3) 'eqv' (c2 '&' c4) by BVFUNC_1:4 ;
end;

theorem :: BVFUNC26:13
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( b2 'nand' (b3 'nand' b4) = ('not' b2) 'or' (b3 '&' b4) & b2 'nand' (b3 'nand' b4) = b2 'imp' (b3 '&' b4) )
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
c2 'nand' (c3 'nand' c4) = 'not' (c2 '&' (c3 'nand' c4)) by E5
.= 'not' (c2 '&' ('not' (c3 '&' c4))) by E5
.= ('not' c2) 'or' ('not' ('not' (c3 '&' c4))) by BVFUNC_1:17
.= ('not' c2) 'or' (c3 '&' c4) by BVFUNC_1:4 ;
hence ( c2 'nand' (c3 'nand' c4) = ('not' c2) 'or' (c3 '&' c4) & c2 'nand' (c3 'nand' c4) = c2 'imp' (c3 '&' c4) ) by BVFUNC_4:8;
end;

theorem :: BVFUNC26:14
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( b2 'nand' (b3 'nor' b4) = (('not' b2) 'or' b3) 'or' b4 & b2 'nand' (b3 'nor' b4) = b2 'imp' (b3 'or' b4) )
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E12: c2 'nand' (c3 'nor' c4) = 'not' (c2 '&' (c3 'nor' c4)) by E5
.= 'not' (c2 '&' ('not' (c3 'or' c4))) by E6
.= ('not' c2) 'or' ('not' ('not' (c3 'or' c4))) by BVFUNC_1:17
.= ('not' c2) 'or' (c3 'or' c4) by BVFUNC_1:4
.= (('not' c2) 'or' c3) 'or' c4 by BVFUNC_1:11 ;
c2 'nand' (c3 'nor' c4) = ('not' c2) 'or' (c3 'or' c4) by E12, BVFUNC_1:11;
hence ( c2 'nand' (c3 'nor' c4) = (('not' c2) 'or' c3) 'or' c4 & c2 'nand' (c3 'nor' c4) = c2 'imp' (c3 'or' c4) ) by E12, BVFUNC_4:8;
end;

theorem :: BVFUNC26:15
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'nand' (b3 'eqv' b4) = b2 'imp' (b3 'xor' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
c2 'nand' (c3 'eqv' c4) = 'not' (c2 '&' (c3 'eqv' c4)) by E5
.= ('not' c2) 'or' ('not' (c3 'eqv' c4)) by BVFUNC_1:17
.= ('not' c2) 'or' ('not' ('not' (c3 'xor' c4))) by BVFUNC25:12
.= ('not' c2) 'or' (c3 'xor' c4) by BVFUNC_1:4 ;
hence c2 'nand' (c3 'eqv' c4) = c2 'imp' (c3 'xor' c4) by BVFUNC_4:8;
end;

theorem :: BVFUNC26:16
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'nand' (b2 '&' b3) = b2 'nand' b3
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
c2 'nand' (c2 '&' c3) = (c2 '&' c2) 'nand' c3 by E10;
hence c2 'nand' (c2 '&' c3) = c2 'nand' c3 by BVFUNC_1:6;
end;

theorem :: BVFUNC26:17
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'nand' (b2 'or' b3) = ('not' b2) '&' ('not' (b2 '&' b3))
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
thus c2 'nand' (c2 'or' c3) = ('not' (c2 '&' c2)) '&' ('not' (c2 '&' c3)) by E11
.= ('not' c2) '&' ('not' (c2 '&' c3)) by BVFUNC_1:6 ;
end;

theorem :: BVFUNC26:18
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'nand' (b2 'eqv' b3) = b2 'imp' (b2 'xor' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
c2 'nand' (c2 'eqv' c3) = 'not' (c2 '&' (c2 'eqv' c3)) by E5
.= ('not' c2) 'or' ('not' (c2 'eqv' c3)) by BVFUNC_1:17
.= ('not' c2) 'or' ('not' ('not' (c2 'xor' c3))) by BVFUNC25:12
.= ('not' c2) 'or' (c2 'xor' c3) by BVFUNC_1:4 ;
hence c2 'nand' (c2 'eqv' c3) = c2 'imp' (c2 'xor' c3) by BVFUNC_4:8;
end;

theorem :: BVFUNC26:19
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds
( b2 'nand' (b2 'nand' b3) = ('not' b2) 'or' b3 & b2 'nand' (b2 'nand' b3) = b2 'imp' b3 )
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
c2 'nand' (c2 'nand' c3) = 'not' (c2 '&' (c2 'nand' c3)) by E5
.= 'not' (c2 '&' ('not' (c2 '&' c3))) by E5
.= ('not' c2) 'or' ('not' ('not' (c2 '&' c3))) by BVFUNC_1:17
.= ('not' c2) 'or' (c2 '&' c3) by BVFUNC_1:4
.= (('not' c2) 'or' c2) '&' (('not' c2) 'or' c3) by BVFUNC_1:14
.= (I_el c1) '&' (('not' c2) 'or' c3) by BVFUNC_4:6
.= ('not' c2) 'or' c3 by BVFUNC_1:9 ;
hence ( c2 'nand' (c2 'nand' c3) = ('not' c2) 'or' c3 & c2 'nand' (c2 'nand' c3) = c2 'imp' c3 ) by BVFUNC_4:8;
end;

theorem :: BVFUNC26:20
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'nand' (b2 'nor' b3) = I_el b1
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
thus c2 'nand' (c2 'nor' c3) = 'not' (c2 '&' (c2 'nor' c3)) by E5
.= 'not' (c2 '&' ('not' (c2 'or' c3))) by E6
.= ('not' c2) 'or' ('not' ('not' (c2 'or' c3))) by BVFUNC_1:17
.= ('not' c2) 'or' (c2 'or' c3) by BVFUNC_1:4
.= (('not' c2) 'or' c2) 'or' c3 by BVFUNC_1:11
.= (I_el c1) 'or' c3 by BVFUNC_4:6
.= I_el c1 by BVFUNC_1:13 ;
end;

theorem :: BVFUNC26:21
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'nand' (b2 'eqv' b3) = ('not' b2) 'or' ('not' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
thus c2 'nand' (c2 'eqv' c3) = 'not' (c2 '&' (c2 'eqv' c3)) by E5
.= 'not' (c2 '&' ('not' (c2 'xor' c3))) by BVFUNC25:12
.= ('not' c2) 'or' ('not' ('not' (c2 'xor' c3))) by BVFUNC_1:17
.= ('not' c2) 'or' (c2 'xor' c3) by BVFUNC_1:4
.= ('not' c2) 'or' ((c2 'or' c3) '&' (('not' c2) 'or' ('not' c3))) by BVFUNC_8:13
.= (('not' c2) 'or' (c2 'or' c3)) '&' (('not' c2) 'or' (('not' c2) 'or' ('not' c3))) by BVFUNC_1:14
.= ((('not' c2) 'or' c2) 'or' c3) '&' (('not' c2) 'or' (('not' c2) 'or' ('not' c3))) by BVFUNC_1:11
.= ((I_el c1) 'or' c3) '&' (('not' c2) 'or' (('not' c2) 'or' ('not' c3))) by BVFUNC_4:6
.= (I_el c1) '&' (('not' c2) 'or' (('not' c2) 'or' ('not' c3))) by BVFUNC_1:13
.= ('not' c2) 'or' (('not' c2) 'or'<