:: Propositional Calculus for Boolean Valued Functions, {VII} :: by Shunichi Kobayashi :: :: Received February 6, 2003 :: Copyright (c) 2003-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, MARGREL1, XBOOLEAN, BVFUNC_1, PARTIT1, FUNCT_1, SUBSET_1, RELAT_1, TARSKI; notations TARSKI, XBOOLE_0, SUBSET_1, XBOOLEAN, RELAT_1, FUNCT_1, FUNCT_2, BVFUNC_1, MARGREL1; constructors BVFUNC_1, RELSET_1; registrations XBOOLE_0, FUNCT_2, XBOOLEAN, MARGREL1, RELSET_1; requirements SUBSET, BOOLE; definitions TARSKI, FUNCT_2, MARGREL1; theorems BVFUNC_1, BVFUNC_4, BVFUNC_5, BVFUNC_6, FUNCT_1, FUNCT_2, MARGREL1, XBOOLEAN, PARTFUN1; schemes FUNCT_1; begin reserve Y for non empty set, a,b,c,d for Function of Y,BOOLEAN; theorem Th1: 'not' (a 'imp' b) = a '&' 'not' b proof thus 'not' (a 'imp' b)='not' ('not' a 'or' b) by BVFUNC_4:8 .='not' 'not' a '&' 'not' b by BVFUNC_1:13 .=a '&' 'not' b; end; theorem Th2: a 'imp' b = 'not' b 'imp' 'not' a proof (a 'imp' b) 'imp' ('not' b 'imp' 'not' a)=I_el(Y) by BVFUNC_5:32; then A1: a 'imp' b '<' 'not' b 'imp' 'not' a by BVFUNC_1:16; ('not' b 'imp' 'not' a) 'imp' (a 'imp' b)=I_el(Y) by BVFUNC_5:31; then ('not' b 'imp' 'not' a) '<' (a 'imp' b) by BVFUNC_1:16; hence thesis by A1,BVFUNC_1:15; end; theorem a 'eqv' b = 'not' a 'eqv' 'not' b proof thus 'not' a 'eqv' 'not' b =('not' a 'imp' 'not' b) '&' ('not' b 'imp' 'not' a) by BVFUNC_4:7 .=(b 'imp' a) '&' ('not' b 'imp' 'not' a) by Th2 .=(b 'imp' a) '&' (a 'imp' b) by Th2 .=a 'eqv' b by BVFUNC_4:7; end; theorem Th4: a 'imp' b = a 'imp' (a '&' b) proof a 'imp' (a '&' b)='not' a 'or' (a '&' b) by BVFUNC_4:8 .=('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 thesis by BVFUNC_4:8; end; theorem a 'eqv' b = (a 'or' b) 'imp' (a '&' b) proof thus (a 'or' b) 'imp' (a '&' b) =(a 'imp' (a '&' b)) '&' (b 'imp' (a '&' b)) by BVFUNC_6:51 .=(a 'imp' b) '&' (b 'imp' (a '&' b)) by Th4 .=(a 'imp' b) '&' (b 'imp' a) by Th4 .=a 'eqv' b by BVFUNC_4:7; end; theorem a 'eqv' 'not' a = O_el(Y) proof thus a 'eqv' 'not' a =(a 'imp' 'not' a) '&' ('not' a 'imp' a) by BVFUNC_4:7 .=('not' a 'or' 'not' a) '&' ('not' a 'imp' a) by BVFUNC_4:8 .='not' a '&' ('not' 'not' a 'or' a) by BVFUNC_4:8 .=O_el(Y) by BVFUNC_4:5; end; theorem a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c) proof thus a 'imp' (b 'imp' c) ='not' a 'or' (b 'imp' c) by BVFUNC_4:8 .='not' a 'or' ('not' b 'or' c) by BVFUNC_4:8 .='not' b 'or' ('not' a 'or' c) by BVFUNC_1:8 .='not' b 'or' (a 'imp' c) by BVFUNC_4:8 .=b 'imp' (a 'imp' c) by BVFUNC_4:8; end; theorem a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c) proof thus (a 'imp' b) 'imp' (a 'imp' c) =(a 'imp' b) 'imp' ('not' a 'or' c) by BVFUNC_4:8 .='not' (a 'imp' b) 'or' ('not' a 'or' c) by BVFUNC_4:8 .='not' ('not' a 'or' b) 'or' ('not' a 'or' c) by BVFUNC_4:8 .=('not' 'not' a '&' 'not' b) 'or' ('not' a 'or' c) by BVFUNC_1:13 .=((a '&' 'not' b) 'or' 'not' a) 'or' c by BVFUNC_1:8 .=((a 'or' 'not' a) '&' ('not' b 'or' 'not' a)) 'or' c by BVFUNC_1:11 .=(I_el(Y) '&' ('not' b 'or' 'not' a)) 'or' c by BVFUNC_4:6 .=('not' a 'or' 'not' b) 'or' c by BVFUNC_1:6 .='not' a 'or' ('not' b 'or' c) by BVFUNC_1:8 .='not' a 'or' (b 'imp' c) by BVFUNC_4:8 .=a 'imp' (b 'imp' c) by BVFUNC_4:8; end; theorem a 'eqv' b = a 'xor' 'not' b proof 'not' (a 'xor' b) = 'not' 'not' (a 'eqv' b) by BVFUNC_6:85; hence thesis by BVFUNC_6:90; end; theorem Th11: a '&' (b 'xor' c) = a '&' b 'xor' a '&' c proof A1: a '&' b 'xor' a '&' c =('not' (a '&' b) '&' (a '&' c)) 'or' ((a '&' b) '&' 'not' (a '&' c)) by BVFUNC_4:9 .=(('not' a 'or' 'not' b) '&' (a '&' c)) 'or' ((a '&' b) '&' 'not' (a '&' c)) by BVFUNC_1:14 .=((a '&' c) '&' ('not' a 'or' 'not' b)) 'or' ((a '&' b) '&' ('not' a 'or' 'not' c)) by BVFUNC_1:14 .=(((a '&' c) '&' 'not' a) 'or' ((a '&' c) '&' 'not' b)) 'or' ((a '&' b) '&' ('not' a 'or' 'not' c)) by BVFUNC_1:12 .=(((a '&' c) '&' 'not' a) 'or' ((a '&' c) '&' 'not' b)) 'or' (((a '&' b ) '&' 'not' a) 'or' ((a '&' b) '&' 'not' c)) by BVFUNC_1:12 .=((a '&' c) '&' 'not' a) 'or' (((a '&' c) '&' 'not' b) 'or' (((a '&' b) '&' 'not' c) 'or' ((a '&' b) '&' 'not' a))) by BVFUNC_1:8 .=((a '&' c) '&' 'not' a) 'or' ((((a '&' c) '&' 'not' b) 'or' ((a '&' b) '&' 'not' c)) 'or' ((a '&' b) '&' 'not' a)) by BVFUNC_1:8 .=(((a '&' c) '&' 'not' a) 'or' ((a '&' b) '&' 'not' a)) 'or' (((a '&' c ) '&' 'not' b) 'or' ((a '&' b) '&' 'not' c)) by BVFUNC_1:8; A2: ((c '&' a) '&' 'not' a) 'or' ((b '&' a) '&' 'not' a) =(c '&' (a '&' 'not' a)) 'or' ((b '&' a) '&' 'not' a) by BVFUNC_1:4 .=(c '&' (a '&' 'not' a)) 'or' (b '&' (a '&' 'not' a)) by BVFUNC_1:4 .=(c '&' O_el(Y)) 'or' (b '&' (a '&' 'not' a)) by BVFUNC_4:5 .=(c '&' O_el(Y)) 'or' (b '&' O_el(Y)) by BVFUNC_4:5 .=O_el(Y) 'or' (b '&' O_el(Y)) by BVFUNC_1:5 .=O_el(Y) 'or' O_el(Y) by BVFUNC_1:5 .=O_el(Y); a '&' (b 'xor' c) =a '&' (('not' b '&' c) 'or' (b '&' 'not' c)) by BVFUNC_4:9 .=(a '&' ('not' b '&' c)) 'or' (a '&' (b '&' 'not' c)) by BVFUNC_1:12 .=((a '&' c) '&' 'not' b) 'or' (a '&' (b '&' 'not' c)) by BVFUNC_1:4 .=((a '&' c) '&' 'not' b) 'or' ((a '&' b) '&' 'not' c) by BVFUNC_1:4; hence thesis by A1,A2,BVFUNC_1:9; end; theorem Th12: a 'eqv' b = 'not' (a 'xor' b) proof 'not' (a 'xor' b) = 'not' 'not' (a 'eqv' b) by BVFUNC_6:85; hence thesis; end; theorem Th13: a 'xor' a = O_el(Y) proof thus a 'xor' a =('not' a '&' a) 'or' (a '&' 'not' a) by BVFUNC_4:9 .=O_el(Y) by BVFUNC_4:5; end; theorem Th14: a 'xor' 'not' a = I_el(Y) proof thus a 'xor' 'not' a =('not' a '&' 'not' a) 'or' (a '&' 'not' 'not' a) by BVFUNC_4:9 .=I_el(Y) by BVFUNC_4:6; end; theorem Red1: (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a proof (a 'imp' b) 'imp' (b 'imp' a) =('not' a 'or' b) 'imp' (b 'imp' a) by BVFUNC_4:8 .=('not' a 'or' b) 'imp' ('not' b 'or' a) by BVFUNC_4:8 .='not' ('not' a 'or' b) 'or' ('not' b 'or' a) by BVFUNC_4:8 .=('not' 'not' a '&' 'not' b) 'or' ('not' b 'or' a) by BVFUNC_1:13 .=((a '&' 'not' b) 'or' 'not' b) 'or' a by BVFUNC_1:8 .=((a 'or' 'not' b) '&' ('not' b 'or' 'not' b)) 'or' a by BVFUNC_1:11 .=((a 'or' 'not' b) 'or' a) '&' ('not' b 'or' a) by BVFUNC_1:11 .=('not' b 'or' (a 'or' a)) '&' ('not' b 'or' a) by BVFUNC_1:8 .=('not' b 'or' a); hence thesis by BVFUNC_4:8; end; registration let Y,a,b; reduce (a 'imp' b) 'imp' (b 'imp' a) to b 'imp' a; reducibility by Red1; end; theorem Th15: (a 'or' b) '&' ('not' a 'or' 'not' b) = ('not' a '&' b) 'or' (a '&' 'not' b) proof a 'xor' b = ('not' a '&' b) 'or' (a '&' 'not' b) by BVFUNC_4:9; hence thesis by BVFUNC_6:86; end; theorem Th16: (a '&' b) 'or' ('not' a '&' 'not' b) = ('not' a 'or' b) '&' (a 'or' 'not' b) proof thus (a '&' b) 'or' ('not' a '&' 'not' b) =('not' a 'or' b) '&' ('not' 'not' a 'or' 'not' b) by Th15 .=('not' a 'or' b) '&' (a 'or' 'not' b); end; theorem a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c proof A1: (a 'xor' b) 'xor' c =(('not' a '&' b) 'or' (a '&' 'not' b)) 'xor' c by BVFUNC_4:9 .=('not' (('not' a '&' b) 'or' (a '&' 'not' b)) '&' c) 'or' ((('not' a '&' b) 'or' (a '&' 'not' b)) '&' 'not' c) by BVFUNC_4:9 .=(('not' ('not' a '&' b) '&' 'not' (a '&' 'not' b)) '&' c) 'or' ((( 'not' a '&' b) 'or' (a '&' 'not' b)) '&' 'not' c) by BVFUNC_1:13 .=((('not' 'not' a 'or' 'not' b) '&' 'not' (a '&' 'not' b)) '&' c) 'or' ((('not' a '&' b) 'or' (a '&' 'not' b)) '&' 'not' c) by BVFUNC_1:14 .=(((a 'or' 'not' b) '&' ('not' a 'or' 'not' 'not' b)) '&' c) 'or' ((( 'not' a '&' b) 'or' (a '&' 'not' b)) '&' 'not' c) by BVFUNC_1:14 .=(((a 'or' 'not' b) '&' ('not' a 'or' b)) '&' c) 'or' (('not' a '&' b '&' 'not' c) 'or' (a '&' 'not' b '&' 'not' c)) by BVFUNC_1:12 .=(((a '&' b) 'or' ('not' a '&' 'not' b)) '&' c) 'or' (('not' a '&' b '&' 'not' c) 'or' (a '&' 'not' b '&' 'not' c)) by Th16 .=((a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' c)) 'or' (('not' a '&' b '&' 'not' c) 'or' (a '&' 'not' b '&' 'not' c)) by BVFUNC_1:12 .=(a '&' b '&' c) 'or' ((a '&' 'not' b '&' 'not' c) 'or' ('not' a '&' b '&' 'not' c)) 'or' ('not' a '&' 'not' b '&' c) by BVFUNC_1:8 .=(a '&' b '&' c) 'or' (a '&' 'not' b '&' 'not' c) 'or' ('not' a '&' b '&' 'not' c) 'or' ('not' a '&' 'not' b '&' c) by BVFUNC_1:8; a 'xor' (b 'xor' c) =('not' a '&' (b 'xor' c)) 'or' (a '&' 'not' (b 'xor' c)) by BVFUNC_4:9 .=('not' a '&' (('not' b '&' c) 'or' (b '&' 'not' c))) 'or' (a '&' 'not' (b 'xor' c)) by BVFUNC_4:9 .=('not' a '&' (('not' b '&' c) 'or' (b '&' 'not' c))) 'or' (a '&' 'not' (('not' b '&' c) 'or' (b '&' 'not' c))) by BVFUNC_4:9 .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c))) 'or' (a '&' 'not' (('not' b '&' c) 'or' (b '&' 'not' c))) by BVFUNC_1:12 .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c))) 'or' (a '&' (('not' ('not' b '&' c)) '&' ('not' (b '&' 'not' c)))) by BVFUNC_1:13 .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c))) 'or' (a '&' ((('not' 'not' b 'or' 'not' c)) '&' ('not' (b '&' 'not' c)))) by BVFUNC_1:14 .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c))) 'or' (a '&' ((b 'or' 'not' c) '&' (('not' b 'or' 'not' 'not' c)))) by BVFUNC_1:14 .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c))) 'or' (a '&' ((b '&' c) 'or' ('not' b '&' 'not' c))) by Th16 .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c))) 'or' ((a '&' (b '&' c)) 'or' (a '&' ('not' b '&' 'not' c))) by BVFUNC_1:12 .=(('not' a '&' 'not' b '&' c) 'or' ('not' a '&' (b '&' 'not' c))) 'or' ((a '&' (b '&' c)) 'or' (a '&' ('not' b '&' 'not' c))) by BVFUNC_1:4 .=(('not' a '&' 'not' b '&' c) 'or' ('not' a '&' b '&' 'not' c)) 'or' (( a '&' (b '&' c)) 'or' (a '&' ('not' b '&' 'not' c))) by BVFUNC_1:4 .=(('not' a '&' 'not' b '&' c) 'or' ('not' a '&' b '&' 'not' c)) 'or' (( a '&' b '&' c) 'or' (a '&' ('not' b '&' 'not' c))) by BVFUNC_1:4 .=((a '&' b '&' c) 'or' (a '&' 'not' b '&' 'not' c)) 'or' (('not' a '&' b '&' 'not' c) 'or' ('not' a '&' 'not' b '&' c)) by BVFUNC_1:4 .=(a '&' b '&' c) 'or' (a '&' 'not' b '&' 'not' c) 'or' ('not' a '&' b '&' 'not' c) 'or' ('not' a '&' 'not' b '&' c) by BVFUNC_1:8; hence thesis by A1; end; theorem a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c proof A1: (a 'eqv' b) 'eqv' c =((a 'eqv' b) 'imp' c) '&' (c 'imp' (a 'eqv' b)) by BVFUNC_4:7 .=(((a 'imp' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' (a 'eqv' b)) by BVFUNC_4:7 .=(((a 'imp' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:7 .=((('not' a 'or' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8 .=((('not' a 'or' b) '&' ('not' b 'or' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8 .=('not' (('not' a 'or' b) '&' ('not' b 'or' a)) 'or' c) '&' (c 'imp' (( a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8 .=('not' (('not' a 'or' b) '&' ('not' b 'or' a)) 'or' c) '&' ('not' c 'or' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8 .=('not' (('not' a 'or' b) '&' ('not' b 'or' a)) 'or' c) '&' ('not' c 'or' (('not' a 'or' b) '&' (b 'imp' a))) by BVFUNC_4:8 .=('not' (('not' a 'or' b) '&' ('not' b 'or' a)) 'or' c) '&' ('not' c 'or' (('not' a 'or' b) '&' ('not' b 'or' a))) by BVFUNC_4:8 .=(('not' ('not' a 'or' b) 'or' 'not' ('not' b 'or' a)) 'or' c) '&' ( 'not' c 'or' (('not' a 'or' b) '&' ('not' b 'or' a))) by BVFUNC_1:14 .=((('not' 'not' a '&' 'not' b) 'or' 'not' ('not' b 'or' a)) 'or' c) '&' ('not' c 'or' (('not' a 'or' b) '&' ('not' b 'or' a))) by BVFUNC_1:13 .=(((a '&' 'not' b) 'or' ('not' 'not' b '&' 'not' a)) 'or' c) '&' ('not' c 'or' (('not' a 'or' b) '&' ('not' b 'or' a))) by BVFUNC_1:13 .=(((a 'or' b) '&' ('not' a 'or' 'not' b)) 'or' c) '&' ('not' c 'or' (( 'not' a 'or' b) '&' ('not' b 'or' a))) by Th15 .=(((a 'or' b) 'or' c) '&' (('not' a 'or' 'not' b) 'or' c)) '&' ('not' c 'or' (('not' a 'or' b) '&' ('not' b 'or' a))) by BVFUNC_1:11 .=((a 'or' b 'or' c) '&' ('not' a 'or' 'not' b 'or' c)) '&' ((a 'or' 'not' b 'or' 'not' c) '&' ('not' a 'or' b 'or' 'not' c)) by BVFUNC_1:11 .=(a 'or' b 'or' c) '&' ((a 'or' 'not' b 'or' 'not' c) '&' ('not' a 'or' b 'or' 'not' c)) '&' ('not' a 'or' 'not' b 'or' c) by BVFUNC_1:4 .=(a 'or' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c) '&' ('not' a 'or' b 'or' 'not' c) '&' ('not' a 'or' 'not' b 'or' c) by BVFUNC_1:4; a 'eqv' (b 'eqv' c) =(a 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' a) by BVFUNC_4:7 .=(a 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' ((b 'eqv' c) 'imp' a) by BVFUNC_4:7 .=(a 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:7 .=('not' a 'or' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8 .=('not' a 'or' (('not' b 'or' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8 .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8 .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' b 'or' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8 .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' b 'or' c) '&' ('not' c 'or' b)) 'imp' a) by BVFUNC_4:8 .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ('not' (( 'not' b 'or' c) '&' ('not' c 'or' b)) 'or' a) by BVFUNC_4:8 .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (('not' ( 'not' b 'or' c)) 'or' ('not' ('not' c 'or' b)) 'or' a) by BVFUNC_1:14 .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' 'not' b '&' 'not' c)) 'or' ('not' ('not' c 'or' b)) 'or' a) by BVFUNC_1:13 .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (((b '&' 'not' c)) 'or' (('not' 'not' c '&' 'not' b)) 'or' a) by BVFUNC_1:13 .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (((b 'or' c ) '&' ('not' b 'or' 'not' c)) 'or' a) by Th15 .=(('not' a 'or' ('not' b 'or' c)) '&' ('not' a 'or' ('not' c 'or' b))) '&' (((b 'or' c) '&' ('not' b 'or' 'not' c)) 'or' a) by BVFUNC_1:11 .=(('not' a 'or' 'not' b 'or' c) '&' ('not' a 'or' (b 'or' 'not' c))) '&' (((b 'or' c) '&' ('not' b 'or' 'not' c)) 'or' a) by BVFUNC_1:8 .=(('not' a 'or' 'not' b 'or' c) '&' ('not' a 'or' b 'or' 'not' c)) '&' (((b 'or' c) '&' ('not' b 'or' 'not' c)) 'or' a) by BVFUNC_1:8 .=(('not' a 'or' 'not' b 'or' c) '&' ('not' a 'or' b 'or' 'not' c)) '&' ((a 'or' (b 'or' c)) '&' (a 'or' ('not' b 'or' 'not' c))) by BVFUNC_1:11 .=(('not' a 'or' 'not' b 'or' c) '&' ('not' a 'or' b 'or' 'not' c)) '&' ((a 'or' b 'or' c) '&' (a 'or' ('not' b 'or' 'not' c))) by BVFUNC_1:8 .=(('not' a 'or' 'not' b 'or' c) '&' ('not' a 'or' b 'or' 'not' c)) '&' ((a 'or' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c)) by BVFUNC_1:8 .=((a 'or' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c)) '&' ('not' a 'or' b 'or' 'not' c) '&' ('not' a 'or' 'not' b 'or' c) by BVFUNC_1:4; hence thesis by A1; end; theorem 'not' 'not' a 'imp' a = I_el(Y) by BVFUNC_5:7; theorem ((a 'imp' b) '&' a) 'imp' b = I_el(Y) proof ((a 'imp' b) '&' a) 'imp' b = (a '&' b) 'imp' b by BVFUNC_6:56; hence thesis by BVFUNC_6:40; end; theorem Th21: a 'imp' ('not' a 'imp' a) = I_el(Y) proof a 'imp' ('not' a 'imp' a) ='not' a 'or' ('not' a 'imp' a) by BVFUNC_4:8 .='not' a 'or' ('not' 'not' a 'or' a) by BVFUNC_4:8 .='not' a 'or' a; hence thesis by BVFUNC_4:6; end; theorem ('not' a 'imp' a) 'eqv' a = I_el(Y) proof ('not' a 'imp' a) 'eqv' a = (('not' a 'imp' a) 'imp' a) '&' (a 'imp' ( 'not' a 'imp' a)) by BVFUNC_4:7 .= I_el(Y) '&' (a 'imp' ('not' a 'imp' a)) by BVFUNC_5:11 .= (a 'imp' ('not' a 'imp' a)) by BVFUNC_1:6; hence thesis by Th21; end; theorem a 'or' (a 'imp' b) = I_el(Y) proof a 'or' (a 'imp' b) =a 'or' ('not' a 'or' b) by BVFUNC_4:8 .=(a 'or' 'not' a) 'or' b by BVFUNC_1:8 .=I_el(Y) 'or' b by BVFUNC_4:6; hence thesis by BVFUNC_1:10; end; theorem (a 'imp' b) 'or' (c 'imp' a) = I_el(Y) proof (a 'imp' b) 'or' (c 'imp' a) =('not' a 'or' b) 'or' (c 'imp' a) by BVFUNC_4:8 .=('not' a 'or' b) 'or' ('not' c 'or' a) by BVFUNC_4:8 .='not' c 'or' (a 'or' ('not' a 'or' b)) by BVFUNC_1:8 .='not' c 'or' ((a 'or' 'not' a) 'or' b) by BVFUNC_1:8 .='not' c 'or' (I_el(Y) 'or' b) by BVFUNC_4:6 .='not' c 'or' I_el(Y) by BVFUNC_1:10; hence thesis by BVFUNC_1:10; end; theorem (a 'imp' b) 'or' ('not' a 'imp' b) = I_el(Y) proof (a 'imp' b) 'or' ('not' a 'imp' b) =('not' a 'or' b) 'or' ('not' a 'imp' b) by BVFUNC_4:8 .=('not' a 'or' b) 'or' ('not' 'not' a 'or' b) by BVFUNC_4:8 .=b 'or' ('not' a 'or' (a 'or' b)) by BVFUNC_1:8 .=b 'or' (('not' a 'or' a) 'or' b) by BVFUNC_1:8 .=b 'or' (I_el(Y) 'or' b) by BVFUNC_4:6 .=b 'or' I_el(Y) by BVFUNC_1:10; hence thesis by BVFUNC_1:10; end; theorem (a 'imp' b) 'or' (a 'imp' 'not' b) = I_el(Y) proof (a 'imp' b) 'or' (a 'imp' 'not' b) =('not' a 'or' b) 'or' (a 'imp' 'not' b) by BVFUNC_4:8 .=('not' a 'or' b) 'or' ('not' a 'or' 'not' b) by BVFUNC_4:8 .='not' a 'or' (b 'or' ('not' b 'or' 'not' a)) by BVFUNC_1:8 .='not' a 'or' ((b 'or' 'not' b) 'or' 'not' a) by BVFUNC_1:8 .='not' a 'or' (I_el(Y) 'or' 'not' a) by BVFUNC_4:6 .='not' a 'or' I_el(Y) by BVFUNC_1:10; hence thesis by BVFUNC_1:10; end; theorem 'not' a 'imp' ('not' b 'eqv' (b 'imp' a)) = I_el(Y) proof 'not' a 'imp' ('not' b 'eqv' (b 'imp' a)) ='not' 'not' a 'or' ('not' b 'eqv' (b 'imp' a)) by BVFUNC_4:8 .=a 'or' (('not' b 'imp' (b 'imp' a)) '&' ((b 'imp' a) 'imp' 'not' b)) by BVFUNC_4:7 .=a 'or' (('not' 'not' b 'or' (b 'imp' a)) '&' ((b 'imp' a) 'imp' 'not' b)) by BVFUNC_4:8 .=a 'or' ((b 'or' ('not' b 'or' a)) '&' ((b 'imp' a) 'imp' 'not' b)) by BVFUNC_4:8 .=a 'or' (((b 'or' 'not' b) 'or' a) '&' ((b 'imp' a) 'imp' 'not' b)) by BVFUNC_1:8 .=a 'or' ((I_el(Y) 'or' a) '&' ((b 'imp' a) 'imp' 'not' b)) by BVFUNC_4:6 .=a 'or' (I_el(Y) '&' ((b 'imp' a) 'imp' 'not' b)) by BVFUNC_1:10 .=a 'or' ((b 'imp' a) 'imp' 'not' b) by BVFUNC_1:6 .=a 'or' (('not' b 'or' a) 'imp' 'not' b) by BVFUNC_4:8 .=a 'or' ('not' ('not' b 'or' a) 'or' 'not' b) by BVFUNC_4:8 .=a 'or' (('not' 'not' b '&' 'not' a) 'or' 'not' b) by BVFUNC_1:13 .=a 'or' ((b 'or' 'not' b) '&' ('not' a 'or' 'not' b)) by BVFUNC_1:11 .=a 'or' (I_el(Y) '&' ('not' a 'or' 'not' b)) by BVFUNC_4:6 .=a 'or' ('not' a 'or' 'not' b) by BVFUNC_1:6 .=(a 'or' 'not' a) 'or' 'not' b by BVFUNC_1:8 .=I_el(Y) 'or' 'not' b by BVFUNC_4:6; hence thesis by BVFUNC_1:10; end; theorem (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el(Y) proof (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) ='not' (a 'imp' b) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_4:8 .='not' ('not' a 'or' b) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_4:8 .=('not' 'not' a '&' 'not' b) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_1:13 .=(a '&' 'not' b) 'or' ('not' ((a 'imp' c) 'imp' b) 'or' b) by BVFUNC_4:8 .=(a '&' 'not' b) 'or' ('not' (('not' a 'or' c) 'imp' b) 'or' b) by BVFUNC_4:8 .=(a '&' 'not' b) 'or' ('not' ('not' ('not' a 'or' c) 'or' b) 'or' b) by BVFUNC_4:8 .=(a '&' 'not' b) 'or' ('not' (('not' 'not' a '&' 'not' c) 'or' b) 'or' b) by BVFUNC_1:13 .=(a '&' 'not' b) 'or' (('not' (a '&' 'not' c) '&' 'not' b) 'or' b) by BVFUNC_1:13 .=(a '&' 'not' b) 'or' ((('not' a 'or' 'not' 'not' c) '&' 'not' b) 'or' b) by BVFUNC_1:14 .=(a '&' 'not' b) 'or' ((('not' a 'or' c) 'or' b) '&' ('not' b 'or' b)) by BVFUNC_1:11 .=(a '&' 'not' b) 'or' ((('not' a 'or' c) 'or' b) '&' I_el(Y)) by BVFUNC_4:6 .=(a '&' 'not' b) 'or' (('not' a 'or' c) 'or' b) by BVFUNC_1:6 .=((a '&' 'not' b) 'or' b) 'or' ('not' a 'or' c) by BVFUNC_1:8 .=((a 'or' b) '&' ('not' b 'or' b)) 'or' ('not' a 'or' c) by BVFUNC_1:11 .=((a 'or' b) '&' I_el(Y)) 'or' ('not' a 'or' c) by BVFUNC_4:6 .=(a 'or' b) 'or' ('not' a 'or' c) by BVFUNC_1:6 .=b 'or' (a 'or' ('not' a 'or' c)) by BVFUNC_1:8 .=b 'or' ((a 'or' 'not' a) 'or' c) by BVFUNC_1:8 .=b 'or' (I_el(Y) 'or' c) by BVFUNC_4:6 .=b 'or' I_el(Y) by BVFUNC_1:10; hence thesis by BVFUNC_1:10; end; theorem a 'imp' b = a 'eqv' (a '&' b) proof a 'eqv' (a '&' b) =(a 'imp' (a '&' b)) '&' ((a '&' b) 'imp' a) by BVFUNC_4:7 .=('not' a 'or' (a '&' b)) '&' ((a '&' b) 'imp' a) by BVFUNC_4:8 .=('not' a 'or' (a '&' b)) '&' ('not' (a '&' b) 'or' a) by BVFUNC_4:8 .=(('not' a 'or' a) '&' ('not' a 'or' b)) '&' ('not' (a '&' b) 'or' a) by BVFUNC_1:11 .=(I_el(Y) '&' ('not' a 'or' b)) '&' ('not' (a '&' b) 'or' a) by BVFUNC_4:6 .=('not' a 'or' b) '&' ('not' (a '&' b) 'or' a) by BVFUNC_1:6 .=('not' a 'or' b) '&' (('not' a 'or' 'not' b) 'or' a) by BVFUNC_1:14 .=('not' a 'or' b) '&' ('not' b 'or' ('not' a 'or' a)) by BVFUNC_1:8 .=('not' a 'or' b) '&' ('not' b 'or' I_el(Y)) by BVFUNC_4:6 .=('not' a 'or' b) '&' I_el(Y) by BVFUNC_1:10 .='not' a 'or' b by BVFUNC_1:6; hence thesis by BVFUNC_4:8; end; theorem a 'imp' b=I_el(Y) & b 'imp' a=I_el(Y) iff a=b proof (a 'eqv' b)=I_el(Y) iff (a 'imp' b)=I_el(Y) & (b 'imp' a)=I_el(Y) by BVFUNC_4:10; hence thesis by BVFUNC_1:17; end; theorem a = 'not' a 'imp' a proof ('not' a 'imp' a) 'imp' a = I_el(Y) by BVFUNC_5:11; then A1: ('not' a 'imp' a) '<' a by BVFUNC_1:16; a 'imp' ('not' a 'imp' a) = I_el(Y) by Th21; then a '<' ('not' a 'imp' a) by BVFUNC_1:16; hence thesis by A1,BVFUNC_1:15; end; theorem Th32: a 'imp' ((a 'imp' b) 'imp' a) = I_el(Y) proof thus a 'imp' ((a 'imp' b) 'imp' a) ='not' a 'or' ((a 'imp' b) 'imp' a) by BVFUNC_4:8 .='not' a 'or' ('not' (a 'imp' b) 'or' a) by BVFUNC_4:8 .='not' a 'or' ('not' ('not' a 'or' b) 'or' a) by BVFUNC_4:8 .='not' a 'or' (('not' 'not' a '&' 'not' b) 'or' a) by BVFUNC_1:13 .=('not' a 'or' a) 'or' (a '&' 'not' b) by BVFUNC_1:8 .=I_el(Y) 'or' (a '&' 'not' b) by BVFUNC_4:6 .=I_el(Y) by BVFUNC_1:10; end; theorem a = (a 'imp' b) 'imp' a proof ((a 'imp' b) 'imp' a) 'imp' a = I_el(Y) by BVFUNC_6:100; then A1: ((a 'imp' b) 'imp' a) '<' a by BVFUNC_1:16; a 'imp' ((a 'imp' b) 'imp' a) = I_el(Y) by Th32; then a '<' ((a 'imp' b) 'imp' a) by BVFUNC_1:16; hence thesis by A1,BVFUNC_1:15; end; theorem a = (b 'imp' a) '&' ('not' b 'imp' a) proof a=(a 'or' b) '&' (a 'or' 'not' b) by BVFUNC_6:80 .=(a 'or' 'not' 'not' b) '&' (b 'imp' a) by BVFUNC_4:8 .=('not' b 'imp' a) '&' (b 'imp' a) by BVFUNC_4:8; hence thesis; end; theorem a '&' b = 'not' (a 'imp' 'not' b) proof 'not'( a 'imp' 'not' b) 'imp' (a '&' b)=I_el(Y) by BVFUNC_6:35; then A1: 'not'( a 'imp' 'not' b) '<' (a '&' b) by BVFUNC_1:16; (a '&' b) 'imp' 'not'( a 'imp' 'not' b)=I_el(Y) by BVFUNC_6:34; then (a '&' b) '<' 'not'( a 'imp' 'not' b) by BVFUNC_1:16; hence thesis by A1,BVFUNC_1:15; end; theorem a 'or' b = 'not' a 'imp' b proof thus 'not' a 'imp' b ='not' 'not' a 'or' b by BVFUNC_4:8 .=a 'or' b; end; theorem a 'or' b = (a 'imp' b) 'imp' b proof thus (a 'imp' b) 'imp' b ='not' (a 'imp' b) 'or' b by BVFUNC_4:8 .='not' ('not' a 'or' b) 'or' b by BVFUNC_4:8 .=('not' 'not' a '&' 'not' b) 'or' b by BVFUNC_1:13 .=(a 'or' b) '&' ('not' b 'or' b) by BVFUNC_1:11 .=(a 'or' b) '&' I_el(Y) by BVFUNC_4:6 .= a 'or' b by BVFUNC_1:6; end; theorem (a 'imp' b) 'imp' (a 'imp' a) = I_el(Y) proof thus (a 'imp' b) 'imp' (a 'imp' a)=(a 'imp' b) 'imp' I_el(Y) by BVFUNC_5:7 .=I_el(Y) by BVFUNC_6:62; end; theorem (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el ( Y ) proof thus (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = 'not' (a 'imp' (b 'imp' c)) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) by BVFUNC_4:8 .='not' ('not' a 'or' (b 'imp' c)) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) by BVFUNC_4:8 .='not' ('not' a 'or' ('not' b 'or' c)) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) by BVFUNC_4:8 .='not' ('not' a 'or' ('not' b 'or' c)) 'or' ('not' (d 'imp' b) 'or' (a 'imp' (d 'imp' c))) by BVFUNC_4:8 .='not' ('not' a 'or' ('not' b 'or' c)) 'or' ('not' ('not' d 'or' b) 'or' (a 'imp' (d 'imp' c))) by BVFUNC_4:8 .='not' ('not' a 'or' ('not' b 'or' c)) 'or' ('not' ('not' d 'or' b) 'or' ('not' a 'or' (d 'imp' c))) by BVFUNC_4:8 .='not' ('not' a 'or' ('not' b 'or' c)) 'or' ('not' ('not' d 'or' b) 'or' ('not' a 'or' ('not' d 'or' c))) by BVFUNC_4:8 .=('not' 'not' a '&' 'not' ('not' b 'or' c)) 'or' ('not' ('not' d 'or' b ) 'or' ('not' a 'or' ('not' d 'or' c))) by BVFUNC_1:13 .=('not' 'not' a '&' ('not' 'not' b '&' 'not' c)) 'or' ('not' ('not' d 'or' b) 'or' ('not' a 'or' ('not' d 'or' c))) by BVFUNC_1:13 .=(a '&' ('not' 'not' b '&' 'not' c)) 'or' (('not' 'not' d '&' 'not' b) 'or' ('not' a 'or' ('not' d 'or' c))) by BVFUNC_1:13 .=(a '&' (b '&' 'not' c)) 'or' (((d '&' 'not' b) 'or' 'not' a) 'or' ( 'not' d 'or' c)) by BVFUNC_1:8 .=((a '&' (b '&' 'not' c)) 'or' ('not' a 'or' (d '&' 'not' b))) 'or' ( 'not' d 'or' c) by BVFUNC_1:8 .=(((a '&' (b '&' 'not' c)) 'or' 'not' a) 'or' (d '&' 'not' b)) 'or' ( 'not' d 'or' c) by BVFUNC_1:8 .=(((a 'or' 'not' a) '&' ((b '&' 'not' c) 'or' 'not' a)) 'or' (d '&' 'not' b)) 'or' ('not' d 'or' c) by BVFUNC_1:11 .=((I_el(Y) '&' ((b '&' 'not' c) 'or' 'not' a)) 'or' (d '&' 'not' b)) 'or' ('not' d 'or' c) by BVFUNC_4:6 .=(((b '&' 'not' c) 'or' 'not' a) 'or' (d '&' 'not' b)) 'or' ('not' d 'or' c) by BVFUNC_1:6 .=((b '&' 'not' c) 'or' 'not' a) 'or' ((d '&' 'not' b) 'or' ('not' d 'or' c)) by BVFUNC_1:8 .=((b '&' 'not' c) 'or' 'not' a) 'or' ((('not' b '&' d) 'or' 'not' d) 'or' c) by BVFUNC_1:8 .=((b '&' 'not' c) 'or' 'not' a) 'or' ((('not' b 'or' 'not' d) '&' (d 'or' 'not' d)) 'or' c) by BVFUNC_1:11 .=((b '&' 'not' c) 'or' 'not' a) 'or' ((('not' b 'or' 'not' d) '&' I_el( Y)) 'or' c) by BVFUNC_4:6 .=((b '&' 'not' c) 'or' 'not' a) 'or' (('not' b 'or' 'not' d) 'or' c) by BVFUNC_1:6 .='not' a 'or' (('not' c '&' b) 'or' (('not' b 'or' 'not' d) 'or' c)) by BVFUNC_1:8 .='not' a 'or' ((('not' c '&' b) 'or' ('not' b 'or' 'not' d)) 'or' c) by BVFUNC_1:8 .='not' a 'or' (((('not' c '&' b) 'or' 'not' b) 'or' 'not' d) 'or' c) by BVFUNC_1:8 .='not' a 'or' (((('not' c 'or' 'not' b) '&' (b 'or' 'not' b)) 'or' 'not' d) 'or' c) by BVFUNC_1:11 .='not' a 'or' (((('not' c 'or' 'not' b) '&' I_el(Y)) 'or' 'not' d) 'or' c) by BVFUNC_4:6 .='not' a 'or' ((('not' b 'or' 'not' c) 'or' 'not' d) 'or' c) by BVFUNC_1:6 .='not' a 'or' (('not' b 'or' ('not' c 'or' 'not' d)) 'or' c) by BVFUNC_1:8 .='not' a 'or' ('not' b 'or' (('not' d 'or' 'not' c) 'or' c)) by BVFUNC_1:8 .='not' a 'or' ('not' b 'or' ('not' d 'or' ('not' c 'or' c))) by BVFUNC_1:8 .='not' a 'or' ('not' b 'or' ('not' d 'or' I_el(Y))) by BVFUNC_4:6 .='not' a 'or' ('not' b 'or' I_el(Y)) by BVFUNC_1:10 .='not' a 'or' I_el(Y) by BVFUNC_1:10 .=I_el(Y) by BVFUNC_1:10; end; theorem (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el(Y) proof thus (((a 'imp' b) '&' a) '&' c) 'imp' b =((('not' a 'or' b) '&' a) '&' c) 'imp' b by BVFUNC_4:8 .=((('not' a '&' a) 'or' (b '&' a)) '&' c) 'imp' b by BVFUNC_1:12 .=((O_el(Y) 'or' (b '&' a)) '&' c) 'imp' b by BVFUNC_4:5 .=((b '&' a) '&' c) 'imp' b by BVFUNC_1:9 .='not' ((b '&' a) '&' c) 'or' b by BVFUNC_4:8 .=('not' (b '&' a) 'or' 'not' c) 'or' b by BVFUNC_1:14 .=(('not' b 'or' 'not' a) 'or' 'not' c) 'or' b by BVFUNC_1:14 .=(b 'or' ('not' b 'or' 'not' a)) 'or' 'not' c by BVFUNC_1:8 .=((b 'or' 'not' b) 'or' 'not' a) 'or' 'not' c by BVFUNC_1:8 .=(I_el(Y) 'or' 'not' a) 'or' 'not' c by BVFUNC_4:6 .=I_el(Y) 'or' 'not' c by BVFUNC_1:10 .=I_el(Y)by BVFUNC_1:10; end; theorem (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el(Y) proof thus (b 'imp' c) 'imp' ((a '&' b) 'imp' c) ='not' (b 'imp' c) 'or' ((a '&' b ) 'imp' c) by BVFUNC_4:8 .='not' ('not' b 'or' c) 'or' ((a '&' b) 'imp' c) by BVFUNC_4:8 .='not' ('not' b 'or' c) 'or' ('not' (a '&' b) 'or' c) by BVFUNC_4:8 .=('not' 'not' b '&' 'not' c) 'or' ('not' (a '&' b) 'or' c) by BVFUNC_1:13 .=(b '&' 'not' c) 'or' (('not' a 'or' 'not' b) 'or' c) by BVFUNC_1:14 .=((b '&' 'not' c) 'or' c) 'or' ('not' a 'or' 'not' b) by BVFUNC_1:8 .=((b 'or' c) '&' ('not' c 'or' c)) 'or' ('not' a 'or' 'not' b) by BVFUNC_1:11 .=((b 'or' c) '&' I_el(Y)) 'or' ('not' a 'or' 'not' b) by BVFUNC_4:6 .=('not' a 'or' 'not' b) 'or' (b 'or' c) by BVFUNC_1:6 .=(('not' a 'or' 'not' b) 'or' b) 'or' c by BVFUNC_1:8 .=('not' a 'or' ('not' b 'or' b)) 'or' c by BVFUNC_1:8 .=('not' a 'or' I_el(Y)) 'or' c by BVFUNC_4:6 .=I_el(Y) 'or' c by BVFUNC_1:10 .=I_el(Y) by BVFUNC_1:10; end; theorem ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el(Y) proof ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) =('not' (a '&' b) 'or' c) 'imp' ((a '&' b) 'imp' (c '&' b)) by BVFUNC_4:8 .='not' ('not' (a '&' b) 'or' c) 'or' ((a '&' b) 'imp' (c '&' b)) by BVFUNC_4:8 .='not' ('not' (a '&' b) 'or' c) 'or' ('not' (a '&' b) 'or' (c '&' b)) by BVFUNC_4:8 .=('not' 'not' (a '&' b) '&' 'not' c) 'or' ('not' (a '&' b) 'or' (c '&' b)) by BVFUNC_1:13 .=((a '&' b) '&' 'not' c) 'or' (('not' a 'or' 'not' b) 'or' (c '&' b)) by BVFUNC_1:14 .=((a '&' b) '&' 'not' c) 'or' ('not' a 'or' ('not' b 'or' (b '&' c))) by BVFUNC_1:8 .=((a '&' b) '&' 'not' c) 'or' ('not' a 'or' (('not' b 'or' b) '&' ( 'not' b 'or' c))) by BVFUNC_1:11 .=((a '&' b) '&' 'not' c) 'or' ('not' a 'or' (I_el(Y) '&' ('not' b 'or' c))) by BVFUNC_4:6 .=((a '&' b) '&' 'not' c) 'or' ('not' a 'or' ('not' b 'or' c)) by BVFUNC_1:6 .=(((a '&' b) '&' 'not' c) 'or' 'not' a) 'or' ('not' b 'or' c) by BVFUNC_1:8 .=(((a '&' b) 'or' 'not' a) '&' ('not' c 'or' 'not' a)) 'or' ('not' b 'or' c) by BVFUNC_1:11 .=(((a 'or' 'not' a) '&' (b 'or' 'not' a)) '&' ('not' c 'or' 'not' a)) 'or' ('not' b 'or' c) by BVFUNC_1:11 .=((I_el(Y) '&' (b 'or' 'not' a)) '&' ('not' c 'or' 'not' a)) 'or' ( 'not' b 'or' c) by BVFUNC_4:6 .=((b 'or' 'not' a) '&' ('not' c 'or' 'not' a)) 'or' ('not' b 'or' c) by BVFUNC_1:6 .=(((b 'or' 'not' a) '&' ('not' c 'or' 'not' a)) 'or' c) 'or' 'not' b by BVFUNC_1:8 .=(((b 'or' 'not' a) 'or' c) '&' (('not' c 'or' 'not' a) 'or' c)) 'or' 'not' b by BVFUNC_1:11 .=(((b 'or' 'not' a) 'or' c) '&' ('not' a 'or' ('not' c 'or' c))) 'or' 'not' b by BVFUNC_1:8 .=(((b 'or' 'not' a) 'or' c) '&' ('not' a 'or' I_el(Y))) 'or' 'not' b by BVFUNC_4:6 .=(((b 'or' 'not' a) 'or' c) '&' I_el(Y)) 'or' 'not' b by BVFUNC_1:10 .=((b 'or' 'not' a) 'or' c) 'or' 'not' b by BVFUNC_1:6 .=('not' b 'or' (b 'or' 'not' a)) 'or' c by BVFUNC_1:8 .=(('not' b 'or' b) 'or' 'not' a) 'or' c by BVFUNC_1:8 .=(I_el(Y) 'or' 'not' a) 'or' c by BVFUNC_4:6 .=I_el(Y) 'or' c by BVFUNC_1:10; hence thesis by BVFUNC_1:10; end; theorem (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el(Y) by BVFUNC_1:16,BVFUNC_6:112; theorem (a 'imp' b) '&' (a '&' c) 'imp' (b '&' c) = I_el(Y) proof (a 'imp' b) '&' (a '&' c) 'imp' (b '&' c) =((a 'imp' b) '&' a) '&' c 'imp' (b '&' c) by BVFUNC_1:4 .=(a '&' b) '&' c 'imp' (b '&' c) by BVFUNC_6:56 .=a '&' (b '&' c) 'imp' (b '&' c) by BVFUNC_1:4; hence thesis by BVFUNC_6:38; end; theorem a '&' (a 'imp' b) '&' (b 'imp' c) '<' c proof (a '&' (a 'imp' b) '&' (b 'imp' c)) 'imp' c ='not' (a '&' (a 'imp' b) '&' (b 'imp' c)) 'or' c by BVFUNC_4:8 .='not' (a '&' b '&' (b 'imp' c)) 'or' c by BVFUNC_6:56 .='not' (a '&' (b '&' (b 'imp' c))) 'or' c by BVFUNC_1:4 .='not' (a '&' (b '&' c)) 'or' c by BVFUNC_6:56 .='not' ((a '&' b) '&' c) 'or' c by BVFUNC_1:4 .=('not' (a '&' b) 'or' 'not' c) 'or' c by BVFUNC_1:14 .='not' (a '&' b) 'or' ('not' c 'or' c) by BVFUNC_1:8 .='not' (a '&' b) 'or' I_el(Y) by BVFUNC_4:6 .= I_el(Y) by BVFUNC_1:10; hence thesis by BVFUNC_1:16; end; theorem (a 'or' b) '&' (a 'imp' c) '&' (b 'imp' c) '<' ('not' a 'imp' (b 'or' c)) proof (a 'or' b) '&' (a 'imp' c) '&' (b 'imp' c) 'imp' ('not' a 'imp' (b 'or' c ) ) ='not' ((a 'or' b) '&' (a 'imp' c) '&' (b 'imp' c)) 'or' ('not' a 'imp' ( b 'or' c)) by BVFUNC_4:8 .='not' ((a 'or' b) '&' ('not' a 'or' c) '&' (b 'imp' c)) 'or' ('not' a 'imp' (b 'or' c)) by BVFUNC_4:8 .='not' ((a 'or' b) '&' ('not' a 'or' c) '&' ('not' b 'or' c)) 'or' ( 'not' a 'imp' (b 'or' c)) by BVFUNC_4:8 .='not' ((a 'or' b) '&' ('not' a 'or' c) '&' ('not' b 'or' c)) 'or' ( 'not' 'not' a 'or' (b 'or' c)) by BVFUNC_4:8 .=('not' ((a 'or' b) '&' ('not' a 'or' c)) 'or' 'not' ('not' b 'or' c)) 'or' ('not' 'not' a 'or' (b 'or' c)) by BVFUNC_1:14 .=('not' ((a 'or' b) '&' ('not' a 'or' c)) 'or' ('not' 'not' b '&' 'not' c)) 'or' ('not' 'not' a 'or' (b 'or' c)) by BVFUNC_1:13 .=(('not' (a 'or' b) 'or' 'not' ('not' a 'or' c)) 'or' (b '&' 'not' c)) 'or' ('not' 'not' a 'or' (b 'or' c)) by BVFUNC_1:14 .=((('not' a '&' 'not' b) 'or' 'not' ('not' a 'or' c)) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:13 .=((('not' a '&' 'not' b) 'or' ('not' 'not' a '&' 'not' c)) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:13 .=((('not' a 'or' (a '&' 'not' c)) '&' ('not' b 'or' (a '&' 'not' c))) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:11 .=(((('not' a 'or' a) '&' ('not' a 'or' 'not' c)) '&' ('not' b 'or' (a '&' 'not' c))) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:11 .=(((I_el(Y) '&' ('not' a 'or' 'not' c)) '&' ('not' b 'or' (a '&' 'not' c))) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_4:6 .=((('not' a 'or' 'not' c) '&' ('not' b 'or' (a '&' 'not' c))) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:6 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (('not' a 'or' 'not' c) '&' (a '&' 'not' c))) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:12 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' ((('not' a 'or' 'not' c) '&' a) '&' 'not' c)) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:4 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' ((('not' a '&' a) 'or' ( 'not' c '&' a)) '&' 'not' c)) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:12 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' ((O_el(Y) 'or' ('not' c '&' a)) '&' 'not' c)) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_4:5 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (('not' c '&' a) '&' 'not' c)) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:9 .=((('not' c '&' a) '&' 'not' c) 'or' ((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:8 .=((('not' c '&' a) '&' 'not' c) 'or' ((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c))) 'or' (c 'or' (a 'or' b)) by BVFUNC_1:8 .=((((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' (( 'not' c '&' a) '&' 'not' c)) 'or' c) 'or' (a 'or' b) by BVFUNC_1:8 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' ((( 'not' c '&' a) '&' 'not' c) 'or' c)) 'or' (a 'or' b) by BVFUNC_1:8 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' ((( 'not' c '&' a) 'or' c) '&' ('not' c 'or' c))) 'or' (a 'or' b) by BVFUNC_1:11 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' ((( 'not' c '&' a) 'or' c) '&' I_el(Y))) 'or' (a 'or' b) by BVFUNC_4:6 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' ((( 'not' c '&' a) 'or' c))) 'or' (a 'or' b) by BVFUNC_1:6 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' ((( 'not' c 'or' c) '&' (a 'or' c)))) 'or' (a 'or' b) by BVFUNC_1:11 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' (( I_el(Y) '&' (a 'or' c)))) 'or' (a 'or' b) by BVFUNC_4:6 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' (a 'or' c)) 'or' (a 'or' b) by BVFUNC_1:6 .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' ((b '&' 'not' c) 'or' (c 'or' a))) 'or' (a 'or' b) by BVFUNC_1:8 .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' (((b '&' 'not' c) 'or' c) 'or' a)) 'or' (a 'or' b) by BVFUNC_1:8 .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' (((b 'or' c) '&' ('not' c 'or' c)) 'or' a)) 'or' (a 'or' b) by BVFUNC_1:11 .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' (((b 'or' c) '&' I_el(Y)) 'or' a)) 'or' (a 'or' b) by BVFUNC_4:6 .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' ((b 'or' c)'or' a)) 'or' (a 'or' b) by BVFUNC_1:6 .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b 'or' (c 'or' a))) 'or' ( a 'or' b) by BVFUNC_1:8 .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' b) 'or' (c 'or' a)) 'or' ( a 'or' b) by BVFUNC_1:8 .=(((('not' a 'or' 'not' c) 'or' b) '&' ('not' b 'or' b)) 'or' (c 'or' a )) 'or' (a 'or' b) by BVFUNC_1:11 .=(((('not' a 'or' 'not' c) 'or' b) '&' I_el(Y)) 'or' (c 'or' a)) 'or' ( a 'or' b) by BVFUNC_4:6 .=((('not' a 'or' 'not' c) 'or' b) 'or' (c 'or' a)) 'or' (a 'or' b) by BVFUNC_1:6 .=(((('not' a 'or' 'not' c) 'or' b) 'or' c) 'or' a) 'or' (a 'or' b) by BVFUNC_1:8 .=(((('not' a 'or' 'not' c) 'or' c) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_1:8 .=((('not' a 'or' ('not' c 'or' c)) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_1:8 .=((('not' a 'or' I_el(Y)) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_4:6 .=((I_el(Y) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_1:10 .=(I_el(Y) 'or' a) 'or' (a 'or' b) by BVFUNC_1:10 .=I_el(Y) 'or' (a 'or' b) by BVFUNC_1:10 .= I_el(Y) by BVFUNC_1:10; hence thesis by BVFUNC_1:16; end; begin :: from BVFUNC26 reserve Y for non empty set, a,b,c for Function of Y,BOOLEAN; definition let p,q be boolean-valued Function; func p 'nand' q -> Function means :Def1: dom it = dom p /\ dom q & for x being set st x in dom it holds it.x = (p.x) 'nand' (q.x); existence proof deffunc F(object) = (p.\$1) 'nand' (q.\$1); consider s being Function such that A1: dom s = dom p /\ dom q & for x being object st x in dom p /\ dom q holds s.x = F(x) from FUNCT_1:sch 3; take s; thus thesis by A1; end; uniqueness proof let s1,s2 be Function such 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); for x being object st x in dom s1 holds s1.x = s2.x proof let x be object; assume A6: x in dom s1; then s1.x = (p.x) 'nand' (q.x) by A3; hence thesis by A2,A4,A5,A6; end; hence thesis by A2,A4,FUNCT_1:2; end; commutativity; func p 'nor' q -> Function means :Def2: dom it = dom p /\ dom q & for x being set st x in dom it holds it.x = (p.x) 'nor' (q.x); existence proof deffunc F(object) = (p.\$1) 'nor' (q.\$1); consider s being Function such that A7: dom s = dom p /\ dom q & for x being object st x in dom p /\ dom q holds s.x = F(x) from FUNCT_1:sch 3; take s; thus thesis by A7; end; uniqueness proof let s1,s2 be Function such 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); for x being object st x in dom s1 holds s1.x = s2.x proof let x be object; assume A12: x in dom s1; then s1.x = (p.x) 'nor' (q.x) by A9; hence thesis by A8,A10,A11,A12; end; hence thesis by A8,A10,FUNCT_1:2; end; commutativity; end; registration let p,q be boolean-valued Function; cluster p 'nand' q -> boolean-valued; coherence proof let x be object; assume x in rng (p 'nand' q); then consider y being object 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 thesis; end; cluster p 'nor' q -> boolean-valued; coherence proof let x be object; assume x in rng(p 'nor' q); then consider y being object 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 thesis; end; end; definition let A be non empty set; let p,q be Function of A,BOOLEAN; redefine func p 'nand' q -> Function of A,BOOLEAN means :Def3: for x being Element of A holds it.x = (p.x) 'nand' (q.x); coherence 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 thesis by A1,FUNCT_2:2; end; compatibility proof let IT be Function of A,BOOLEAN; A2: dom IT = A by FUNCT_2:def 1; hereby assume A3: IT = p 'nand' q; let x be Element of A; 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; 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); then for x being set st x in dom IT holds IT.x = (p.x) 'nand' (q.x) by A2; hence thesis by A5,Def1; end; redefine func p 'nor' q -> Function of A,BOOLEAN means :Def4: for x being Element of A holds it.x = (p.x) 'nor' (q.x); coherence 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 thesis by A6,FUNCT_2:2; end; compatibility proof let IT be Function of A,BOOLEAN; A7: dom IT = A by FUNCT_2:def 1; hereby assume A8: IT = p 'nor' q; let x be Element of A; 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; 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); then for x being set st x in dom IT holds IT.x = (p.x) 'nor' (q.x) by A7; hence thesis by A10,Def2; end; end; definition let Y; let a,b be Function of Y,BOOLEAN; redefine func a 'nand' b -> Function of Y,BOOLEAN; coherence proof a 'nand' b is Function of Y,BOOLEAN; hence thesis; end; redefine func a 'nor' b -> Function of Y,BOOLEAN; coherence proof a 'nor' b is Function of Y,BOOLEAN; hence thesis; end; end; theorem th1: a 'nand' b = 'not' (a '&' b) proof let x be Element of Y; 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; end; theorem Th2: a 'nor' b = 'not' (a 'or' b) proof let x be Element of Y; 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; end; theorem Th3: I_el(Y) 'nand' a = 'not' a proof I_el(Y) 'nand' a = 'not' (I_el(Y) '&' a) by th1; hence thesis by BVFUNC_1:6; end; theorem Th4: O_el(Y) 'nand' a = I_el(Y) proof O_el(Y) 'nand' a = 'not' (O_el(Y) '&' a) & O_el(Y) '&' a = O_el(Y) by th1, BVFUNC_1:5; hence thesis by BVFUNC_1:2; end; theorem 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 thus O_el(Y) 'nand' O_el(Y) = I_el(Y) by Th4; thus O_el(Y) 'nand' I_el(Y) = I_el(Y) by Th4; thus I_el(Y) 'nand' I_el(Y) = 'not' I_el(Y) by Th3 .= O_el(Y) by BVFUNC_1:2; end; theorem a 'nand' a = 'not' a & 'not' (a 'nand' a) = a proof a 'nand' a = 'not' (a '&' a) by th1 .= 'not' a; hence thesis; end; theorem 'not' (a 'nand' b) = a '&' b proof 'not' (a 'nand' b) = 'not' 'not' (a '&' b) by th1; hence thesis; end; theorem a 'nand' 'not' a = I_el(Y) & 'not' (a 'nand' 'not' a) = O_el(Y) proof 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 thesis by BVFUNC_1:2; end; theorem Th9: a 'nand' (b '&' c) = 'not' (a '&' b '&' c) proof a 'nand' (b '&' c) = 'not' (a '&' (b '&' c)) by th1; hence thesis by BVFUNC_1:4; end; theorem Th10: a 'nand' (b '&' c) = (a '&' b) 'nand' c proof (a '&' b) 'nand' c = 'not' (a '&' b '&' c) by th1; hence thesis by Th9; end; theorem th11: a 'nand' (b 'or' c) = 'not' (a '&' b) '&' 'not' (a '&' c) proof 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; end; theorem a 'nand' (b 'xor' c) = (a '&' b) 'eqv' (a '&' c) proof thus a 'nand' (b 'xor' c) = 'not' (a '&' (b 'xor' c)) by th1 .= 'not' ((a '&' b) 'xor' (a '&' c)) by Th11 .= 'not' 'not' ((a '&' b) 'eqv' (a '&' c)) by BVFUNC_6:85 .= (a '&' b) 'eqv' (a '&' c); end; theorem a 'nand' (b 'nand' c) = 'not' a 'or' (b '&' c) & a 'nand' (b 'nand' c) = a 'imp' (b '&' c) proof 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 thesis by BVFUNC_4:8; end; theorem a 'nand' (b 'nor' c) = 'not' a 'or' b 'or' c & a 'nand' (b 'nor' c) = a 'imp' (b 'or' c) proof 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 thesis by A1,BVFUNC_4:8; end; theorem a 'nand' (b 'eqv' c) = a 'imp' (b 'xor' c) proof 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 Th12 .= ('not' a) 'or' (b 'xor' c); hence thesis by BVFUNC_4:8; end; theorem a 'nand' (a '&' b) = a 'nand' b proof a 'nand' (a '&' b) = (a '&' a) 'nand' b by Th10; hence thesis; end; theorem a 'nand' (a 'or' b) = 'not' a '&' 'not' (a '&' b) proof thus a 'nand' (a 'or' b) = 'not' (a '&' a) '&' 'not' (a '&' b) by th11 .= 'not' a '&' 'not' (a '&' b); end; theorem a 'nand' (a 'eqv' b) = a 'imp' (a 'xor' b) proof 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 Th12 .= 'not' a 'or' (a 'xor' b); hence thesis by BVFUNC_4:8; end; theorem a 'nand' (a 'nand' b) = 'not' a 'or' b & a 'nand' (a 'nand' b) = a 'imp' b proof 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 thesis by BVFUNC_4:8; end; theorem a 'nand' (a 'nor' b) = I_el(Y) proof 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; end; theorem a 'nand' (a 'eqv' b) = 'not' a 'or' 'not' b proof thus a 'nand' (a 'eqv' b) = 'not' (a '&' (a 'eqv' b)) by th1 .= 'not' (a '&' 'not' (a 'xor' b)) by Th12 .= ('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_6:86 .= (('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; end; theorem a '&' b = (a 'nand' b) 'nand' (a 'nand' b) proof 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); end; theorem (a 'nand' b) 'nand' (a 'nand' c) = a '&' (b 'or' c) proof 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; end; theorem Th24: a 'nand' (b 'imp' c) = ('not' a 'or' b) '&' 'not' (a '&' c) proof 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); end; theorem a 'nand' (a 'imp' b) = 'not' (a '&' b) proof 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; end; theorem Th26: I_el(Y) 'nor' a = O_el(Y) proof 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; end; theorem Th27: O_el(Y) 'nor' a = 'not' a proof thus O_el(Y) 'nor' a = 'not' (O_el(Y) 'or' a) by Th2 .= 'not' a by BVFUNC_1:9; end; theorem 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 thus O_el(Y) 'nor' O_el(Y) = 'not' O_el(Y) by Th27 .= I_el(Y) by BVFUNC_1:2; thus O_el(Y) 'nor' I_el(Y) = O_el(Y) by Th26; thus thesis by Th26; end; theorem a 'nor' a = 'not' a & 'not' (a 'nor' a) = a proof a 'nor' a = 'not' (a 'or' a) by Th2 .= 'not' a; hence thesis; end; theorem 'not' (a 'nor' b) = a 'or' b proof 'not' (a 'nor' b) = 'not' 'not' (a 'or' b) by Th2; hence thesis; end; theorem a 'nor' 'not' a = O_el(Y) & 'not' (a 'nor' 'not' a) = I_el(Y) proof 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 thesis by BVFUNC_1:2; end; theorem 'not' a '&' (a 'xor' b) = 'not' a '&' b proof 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; end; theorem Th33: a 'nor' (b '&' c) = 'not' (a 'or' b) 'or' 'not' (a 'or' c) proof a 'nor' (b '&' c) = 'not' (a 'or' (b '&' c)) by Th2 .= 'not' ((a 'or' b) '&' (a 'or' c)) by BVFUNC_1:11; hence thesis by BVFUNC_1:14; end; theorem Th34: a 'nor' (b 'or' c) = 'not' (a 'or' b 'or' c) proof thus a 'nor' (b 'or' c) = 'not' (a 'or' (b 'or' c)) by Th2 .= 'not' (a 'or' b 'or' c) by BVFUNC_1:8; end; theorem Th35: a 'nor' (b 'eqv' c) = ('not' a) '&' (b 'xor' c) proof 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 Th12 .= ('not' a) '&' (b 'xor' c); end; theorem Th36: a 'nor' (b 'imp' c) = 'not' a '&' b '&' 'not' c proof 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 Th1 .= 'not' a '&' b '&' 'not' c by BVFUNC_1:4; end; theorem Th37: a 'nor' (b 'nand' c) = 'not' a '&' b '&' c proof 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; end; theorem Th38: a 'nor' (b 'nor' c) = 'not' a '&' (b 'or' c) proof 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); end; theorem a 'nor' (a '&' b) = 'not' (a '&' (a 'or' b)) proof 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; end; theorem a 'nor' (a 'or' b) = 'not' (a 'or' b) proof thus a 'nor' (a 'or' b) = 'not' (a 'or' a 'or' b) by Th34 .= 'not' (a 'or' b); end; theorem a 'nor' (a 'eqv' b) = 'not' a '&' b proof 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; end; theorem a 'nor' (a 'imp' b) = O_el(Y) proof 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; end; theorem a 'nor' (a 'nand' b) = O_el(Y) proof 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; end; theorem a 'nor' (a 'nor' b) = 'not' a '&' b proof 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; end; theorem O_el(Y) 'eqv' O_el(Y) = I_el(Y) proof thus O_el(Y) 'eqv' O_el(Y) = 'not' (O_el(Y) 'xor' O_el(Y)) by Th12 .= 'not' O_el(Y) by Th13 .= I_el(Y) by BVFUNC_1:2; end; theorem O_el(Y) 'eqv' I_el(Y) = O_el(Y) proof thus O_el(Y) 'eqv' I_el(Y) = 'not' (O_el(Y) 'xor' I_el(Y)) by Th12 .= 'not' (O_el(Y) 'xor' 'not' O_el(Y)) by BVFUNC_1:2 .= 'not' I_el(Y) by Th14 .= O_el(Y) by BVFUNC_1:2; end; theorem I_el(Y) 'eqv' I_el(Y) = I_el(Y) proof thus I_el(Y) 'eqv' I_el(Y) = 'not' (I_el(Y) 'xor' I_el(Y)) by Th12 .= 'not' 'not' I_el(Y) by BVFUNC_6:87 .= I_el(Y); end; theorem a 'eqv' a = I_el(Y) & 'not' (a 'eqv' a) = O_el(Y) proof a 'eqv' a = 'not' (a 'xor' a) by Th12 .= 'not' O_el(Y) by Th13 .= I_el(Y) by BVFUNC_1:2; hence thesis by BVFUNC_1:2; end; theorem a 'eqv' (a 'or' b) = a 'or' 'not' b proof thus a 'eqv' (a 'or' b) = 'not' (a 'xor' (a 'or' b)) by Th12 .= '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; end; theorem Th50: a '&' (b 'nand' c) = (a '&' 'not' b) 'or' (a '&' 'not' c) proof 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; end; theorem Th51: a 'or' (b 'nand' c) = a 'or' 'not' b 'or' 'not' c proof 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; end; theorem Th52: a 'xor' (b 'nand' c) = ('not' a '&' 'not' (b '&' c)) 'or' (a '&' b '&' c) proof 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; end; theorem Th53: a 'eqv' (b 'nand' c) = (a '&' 'not' (b '&' c)) 'or' ('not' a '&' b '&' c) proof 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_6:92 .=(a '&' 'not' (b '&' c)) 'or' ('not' a '&' b '&' c) by BVFUNC_1:4; end; theorem Th54: a 'imp' (b 'nand' c) = 'not' (a '&' b '&' c) proof 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; end; theorem a 'nor' (b 'nand' c) = 'not' (a 'or' 'not' b 'or' 'not' c) proof 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; end; theorem a '&' (a 'nand' b) = a '&' 'not' b proof 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; end; theorem a 'or' (a 'nand' b) = I_el(Y) proof 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; end; theorem a 'xor' (a 'nand' b) = 'not' a 'or' b proof 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; end; theorem a 'eqv' (a 'nand' b) = a '&' 'not' b proof 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; end; theorem a 'imp' (a 'nand' b) = 'not' (a '&' b) proof thus a 'imp' (a 'nand' b) ='not' (a '&' a '&' b) by Th54 .='not' (a '&' b); end; theorem Th61: a '&' (b 'nor' c) = a '&' 'not' b '&' 'not' c proof 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; end; theorem Th62: a 'or' (b 'nor' c) = (a 'or' 'not' b) '&' (a 'or' 'not' c) proof 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; end; theorem Th63: a 'xor' (b 'nor' c) = (a 'or' 'not' (b 'or' c)) '&' ('not' a 'or' b 'or' c) proof 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_6:86 .=(a 'or' 'not' (b 'or' c)) '&' ('not' a 'or' b 'or' c) by BVFUNC_1:8; end; theorem Th64: a 'eqv' (b 'nor' c) = (a 'or' b 'or' c) '&' ('not' a 'or' 'not' (b 'or' c)) proof 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_6:91 .=(a 'or' b 'or' c) '&' ('not' a 'or' 'not' (b 'or' c)) by BVFUNC_1:8; end; theorem Th65: a 'imp' (b 'nor' c) = 'not' (a '&' (b 'or' c)) proof 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; end; theorem a 'nand' (b 'nor' c) = 'not' a 'or' b 'or' c proof 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; end; theorem a '&' (a 'nor' b) = O_el(Y) proof thus a '&' (a 'nor' b) =a '&' 'not' a '&' 'not' b by Th61 .=O_el(Y) '&' 'not' b by BVFUNC_4:5 .=O_el(Y) by BVFUNC_1:5; end; theorem a 'or' (a 'nor' b) = a 'or' 'not' b proof thus a 'or' (a 'nor' b) =(a 'or' 'not' a) '&' (a 'or' 'not' b) by Th62 .=I_el(Y) '&' (a 'or' 'not' b) by BVFUNC_4:6 .=a 'or' 'not' b by BVFUNC_1:6; end; theorem a 'xor' (a 'nor' b) = a 'or' 'not' b proof thus a 'xor' (a 'nor' b) =(a 'or' 'not' (a 'or' b)) '&' ('not' a 'or' a 'or' b) by Th63 .=(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; end; theorem a 'eqv' (a 'nor' b) = 'not' a '&' b proof thus a 'eqv' (a 'nor' b) =(a 'or' a 'or' b) '&' ('not' a 'or' 'not' (a 'or' b)) by Th64 .=((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; end; theorem a 'imp' (a 'nor' b) = 'not' (a 'or' a '&' b) proof thus a 'imp' (a 'nor' b) ='not' (a '&' (a 'or' b)) by Th65 .='not' (a '&' a 'or' a '&' b) by BVFUNC_1:12 .='not' (a 'or' a '&' b); end;