:: 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;