:: Propositional Calculus for Boolean Valued Functions, I :: by Shunichi Kobayashi and Yatsuka Nakamura :: :: Received March 13, 1999 :: Copyright (c) 1999-2017 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, SUBSET_1, MARGREL1, BVFUNC_1, XBOOLEAN, FUNCT_1; notations TARSKI, XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1, FUNCT_1, FUNCT_2, BVFUNC_1; constructors BVFUNC_1, NUMBERS; registrations XBOOLEAN, MARGREL1; requirements SUBSET, BOOLE, NUMERALS; definitions FUNCT_2; equalities XBOOLEAN; theorems MARGREL1, BINARITH, BVFUNC_1, XBOOLEAN; begin ::Chap. 1 Propositional Calculus reserve Y for non empty set; theorem for a,b being Function of Y,BOOLEAN holds a=I_el(Y) & b=I_el(Y) iff (a '&' b)=I_el(Y) proof let a,b be Function of Y,BOOLEAN; now assume A1: a '&' b=I_el(Y); per cases; suppose a=I_el(Y) & b=I_el(Y); hence a=I_el(Y) & b=I_el(Y); end; suppose a=I_el(Y) & b<>I_el(Y); hence a=I_el(Y) & b=I_el(Y) by A1,BVFUNC_1:6; end; suppose a<>I_el(Y) & b=I_el(Y); hence a=I_el(Y) & b=I_el(Y) by A1,BVFUNC_1:6; end; suppose A2: a<>I_el(Y) & b<>I_el(Y); for x being Element of Y holds a.x=TRUE proof let x be Element of Y; (a '&' b).x=TRUE by A1,BVFUNC_1:def 11; then a.x '&' b.x=TRUE by MARGREL1:def 20; hence thesis by MARGREL1:12; end; hence a=I_el(Y) & b=I_el(Y) by A2,BVFUNC_1:def 11; end; end; hence thesis; end; theorem Th2: for b being Function of Y,BOOLEAN st (I_el(Y) 'imp' b)=I_el (Y) holds b=I_el(Y) proof set a=I_el(Y); let b be Function of Y,BOOLEAN; assume A1: a 'imp' b=I_el(Y); for x being Element of Y holds b.x=TRUE proof let x be Element of Y; (a 'imp' b).x=TRUE by A1,BVFUNC_1:def 11; then a.x=TRUE & ('not' a.x) 'or' b.x=TRUE by BVFUNC_1:def 8,def 11; then FALSE 'or' b.x=TRUE by MARGREL1:11; hence thesis by BINARITH:3; end; hence thesis by BVFUNC_1:def 11; end; theorem for a,b being Function of Y,BOOLEAN st a=I_el(Y) holds (a 'or' b )=I_el(Y) proof let a,b be Function of Y,BOOLEAN; assume A1: a=I_el(Y); for x being Element of Y holds (a 'or' b).x=TRUE proof let x be Element of Y; a.x=TRUE by A1,BVFUNC_1:def 11; then (a 'or' b).x =TRUE 'or' b.x by BVFUNC_1:def 4 .=TRUE by BINARITH:10; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem for a,b being Function of Y,BOOLEAN st b=I_el(Y) holds (a 'imp' b)=I_el(Y) proof let a,b be Function of Y,BOOLEAN; assume A1: b=I_el(Y); for x being Element of Y holds (a 'imp' b).x=TRUE proof let x be Element of Y; b.x=TRUE by A1,BVFUNC_1:def 11; then (a 'imp' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem for a,b being Function of Y,BOOLEAN st ('not' a)=I_el(Y) holds ( a 'imp' b)=I_el(Y) proof let a,b be Function of Y,BOOLEAN; assume A1: 'not' a=I_el(Y); for x being Element of Y holds (a 'imp' b).x=TRUE proof let x be Element of Y; ('not' a).x=TRUE by A1,BVFUNC_1:def 11; then 'not' a.x=TRUE by MARGREL1:def 19; then (a 'imp' b).x =TRUE 'or' b.x by BVFUNC_1:def 8 .=TRUE by BINARITH:10; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem for a being Function of Y,BOOLEAN holds 'not' (a '&' 'not' a)= I_el(Y) proof let a be Function of Y,BOOLEAN; let x be Element of Y; thus ('not' (a '&' 'not' a)).x = 'not' (a '&' 'not' a).x by MARGREL1:def 19 .= 'not' (a.x '&' ('not' a).x) by MARGREL1:def 20 .= 'not' (a.x '&' 'not' a.x) by MARGREL1:def 19 .= TRUE by XBOOLEAN:102 .= I_el(Y).x by BVFUNC_1:def 11; end; theorem :: Identity law for a being Function of Y,BOOLEAN holds a 'imp' a = I_el Y proof let a be Function of Y,BOOLEAN; let x be Element of Y; A1: (a 'imp' a).x = ('not' a.x) 'or' a.x & (I_el Y).x=TRUE by BVFUNC_1:def 8 ,def 11; A2: 'not' FALSE=TRUE by MARGREL1:11; now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence thesis by A1,BINARITH:10; end; case a.x=FALSE; hence thesis by A2,A1,BINARITH:10; end; end; hence thesis; end; theorem for a,b being Function of Y,BOOLEAN holds (a 'imp' b)=I_el(Y) iff ('not' b 'imp' 'not' a)=I_el(Y) proof let a,b be Function of Y,BOOLEAN; A1: now assume A2: ('not' b 'imp' 'not' a)=I_el(Y); for x being Element of Y holds (a 'imp' b).x=TRUE proof let x be Element of Y; ('not' b 'imp' 'not' a).x=TRUE by A2,BVFUNC_1:def 11; then ('not' ('not' b).x) 'or' ('not' a).x=TRUE by BVFUNC_1:def 8; then ('not' 'not' b.x) 'or' ('not' a).x=TRUE by MARGREL1:def 19; then A3: ('not' 'not' b.x) 'or' 'not' a.x=TRUE by MARGREL1:def 19; A4: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3; now per cases by A3,A4,BINARITH:3; case ('not' a.x)=TRUE; then (a 'imp' b).x =TRUE 'or' b.x by BVFUNC_1:def 8 .=TRUE by BINARITH:10; hence thesis; end; case b.x=TRUE; then (a 'imp' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; hence thesis; end; end; hence thesis; end; hence a 'imp' b=I_el(Y) by BVFUNC_1:def 11; end; now assume A5: (a 'imp' b)=I_el(Y); for x being Element of Y holds ('not' b 'imp' 'not' a).x=TRUE proof let x be Element of Y; (a 'imp' b).x=TRUE by A5,BVFUNC_1:def 11; then A6: ('not' a.x) 'or' b.x=TRUE by BVFUNC_1:def 8; A7: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3; now per cases by A6,A7,BINARITH:3; case A8: ('not' a.x)=TRUE; ('not' b 'imp' 'not' a).x =('not' ('not' b).x) 'or' ('not' a).x by BVFUNC_1:def 8 .=('not' ('not' b).x) 'or' TRUE by A8,MARGREL1:def 19 .=TRUE by BINARITH:10; hence thesis; end; case A9: b.x=TRUE; ('not' b).x='not' b.x by MARGREL1:def 19; then ('not' b 'imp' 'not' a).x =('not' 'not' b.x) 'or' ('not' a).x by BVFUNC_1:def 8 .=TRUE by A9,BINARITH:10; hence thesis; end; end; hence thesis; end; hence 'not' b 'imp' 'not' a=I_el(Y) by BVFUNC_1:def 11; end; hence thesis by A1; end; theorem for a,b,c being Function of Y,BOOLEAN st (a 'imp' b)=I_el(Y) & ( b 'imp' c)=I_el(Y) holds (a 'imp' c)=I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; assume that A1: (a 'imp' b)=I_el(Y) and A2: (b 'imp' c)=I_el(Y); for x being Element of Y holds (a 'imp' c).x=TRUE proof let x be Element of Y; A3: ('not' b.x)=TRUE or ('not' b.x)=FALSE by XBOOLEAN:def 3; A4: (a 'imp' c).x=('not' a.x) 'or' c.x by BVFUNC_1:def 8; (b 'imp' c).x=TRUE by A2,BVFUNC_1:def 11; then A5: ('not' b.x) 'or' c.x=TRUE by BVFUNC_1:def 8; (a 'imp' b).x=TRUE by A1,BVFUNC_1:def 11; then A6: ('not' a.x) 'or' b.x=TRUE by BVFUNC_1:def 8; A7: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3; now per cases by A6,A7,A5,A3,BINARITH:3; case ('not' a.x)=TRUE & ('not' b.x)=TRUE; hence thesis by A4,BINARITH:10; end; case ('not' a.x)=TRUE & c.x=TRUE; hence thesis by A4; end; case b.x=TRUE & ('not' b.x)=TRUE; hence thesis by MARGREL1:11; end; case b.x=TRUE & c.x=TRUE; hence thesis by A4,BINARITH:10; end; end; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem for a,b being Function of Y,BOOLEAN st (a 'imp' b)=I_el(Y) & (a 'imp' 'not' b)=I_el(Y) holds 'not' a=I_el(Y) proof let a,b be Function of Y,BOOLEAN; assume that A1: (a 'imp' b)=I_el(Y) and A2: (a 'imp' 'not' b)=I_el(Y); for x being Element of Y holds ('not' a).x=TRUE proof let x be Element of Y; (a 'imp' b).x=TRUE by A1,BVFUNC_1:def 11; then A3: ('not' a.x) 'or' b.x=TRUE by BVFUNC_1:def 8; (a 'imp' 'not' b).x=TRUE by A2,BVFUNC_1:def 11; then A4: ('not' a.x) 'or' ('not' b).x=TRUE by BVFUNC_1:def 8; A5: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3; now per cases by A3,A5,A4,BINARITH:3; case ('not' a.x)=TRUE & ('not' a.x)=TRUE; hence thesis by MARGREL1:def 19; end; case ('not' a.x)=TRUE & ('not' b).x=TRUE; hence thesis by MARGREL1:def 19; end; case b.x=TRUE & ('not' a.x)=TRUE; hence thesis by MARGREL1:def 19; end; case A6: b.x=TRUE & ('not' b).x=TRUE; then 'not' b.x=TRUE by MARGREL1:def 19; hence thesis by A6,MARGREL1:11; end; end; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem for a being Function of Y,BOOLEAN holds ('not' a 'imp' a) 'imp' a = I_el(Y) proof let a be Function of Y,BOOLEAN; let x be Element of Y; A1: 'not' ('not' ('not' a).x 'or' a.x) = 'not' (a.x 'or' a.x) by MARGREL1:def 19 .= 'not' a.x; A2: ('not' a 'imp' a 'imp' a).x =('not' ('not' a 'imp' a).x) 'or' a.x by BVFUNC_1:def 8 .='not' a.x 'or' a.x by A1,BVFUNC_1:def 8; A3: (I_el Y).x=TRUE by BVFUNC_1:def 11; now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence thesis by A2,A3,BINARITH:10; end; case a.x=FALSE; then ('not' a 'imp' a 'imp' a).x =TRUE 'or' FALSE by A2,MARGREL1:11 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; end; hence thesis; end; theorem for a,b,c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ( 'not' (b '&' c) 'imp' 'not' (a '&' c)) =I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; let x be Element of Y; A1: ((a 'imp' b) 'imp' ('not' (b '&' c) 'imp' 'not' (a '&' c))).x = 'not' (a 'imp' b).x 'or' ('not' (b '&' c) 'imp' 'not' (a '&' c)).x by BVFUNC_1:def 8 .= 'not' (a 'imp' b).x 'or' (('not' ('not' (b '&' c)).x) 'or' ('not' ( a '&' c)).x) by BVFUNC_1:def 8; A2: ('not' (a '&' c)).x =(('not' a) 'or' ('not' c)).x by BVFUNC_1:14 .=('not' a).x 'or' ('not' c).x by BVFUNC_1:def 4 .='not' a.x 'or' ('not' c).x by MARGREL1:def 19 .='not' a.x 'or' 'not' c.x by MARGREL1:def 19; now per cases by XBOOLEAN:def 3; case c.x=TRUE; hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10; end; case c.x=FALSE; then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' c.x 'or' c.x)=TRUE; end; end; then ('not' a.x 'or' ('not' c.x 'or' c.x)) =TRUE by BINARITH:10; then A3: (('not' a.x 'or' 'not' c.x) 'or' b.x) '&' ('not' a.x 'or' ('not' c.x 'or' c.x)) = (('not' a.x 'or' 'not' c.x) 'or' b.x) by MARGREL1:14; A4: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; A5: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; 'not' ('not' (b '&' c)).x ='not' 'not' (b '&' c).x by MARGREL1:def 19 .=b.x '&' c.x by MARGREL1:def 20; then A6: ('not' ('not' (b '&' c)).x) 'or' ('not' (a '&' c)).x =(('not' a.x 'or' 'not' c.x) 'or' b.x) '&' (('not' a.x 'or' 'not' c.x) 'or' c.x) by A2, XBOOLEAN:9 .=(('not' a.x 'or' 'not' c.x) 'or' b.x) '&' ('not' a.x 'or' ('not' c.x 'or' c.x)) by BINARITH:11; 'not' (a 'imp' b).x ='not' (('not' a.x) 'or' b.x) by BVFUNC_1:def 8 .=a.x '&' 'not' b.x; then 'not' (a 'imp' b).x 'or' (('not' ('not' (b '&' c)).x) 'or' ('not' (a '&' c)).x) =((('not' a.x 'or' 'not' c.x) 'or' b.x) 'or' a.x) '&' ((('not' a.x 'or' 'not' c.x) 'or' b.x) 'or' 'not' b.x) by A6,A3,XBOOLEAN:9 .=((('not' a.x 'or' 'not' c.x) 'or' b.x) 'or' a.x) '&' (('not' a.x 'or' 'not' c.x) 'or' (b.x 'or' 'not' b.x)) by BINARITH:11 .=((('not' c.x 'or' 'not' a.x) 'or' a.x) 'or' b.x) '&' (('not' a.x 'or' 'not' c.x) 'or' (b.x 'or' 'not' b.x)) by BINARITH:11 .=(('not' c.x 'or' ('not' a.x 'or' a.x)) 'or' b.x) '&' (('not' a.x 'or' 'not' c.x) 'or' (b.x 'or' 'not' b.x)) by BINARITH:11; then 'not' (a 'imp' b).x 'or' (('not' ('not' (b '&' c)).x) 'or' ('not' (a '&' c)).x) =(TRUE 'or' b.x) '&' (('not' a.x 'or' 'not' c.x) 'or' TRUE) by A4,A5,BINARITH:10 .=TRUE '&' (('not' a.x 'or' 'not' c.x) 'or' TRUE) by BINARITH:10 .=TRUE '&' TRUE by BINARITH:10 .=TRUE; hence thesis by A1,BVFUNC_1:def 11; end; theorem for a,b,c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (( b 'imp' c) 'imp' (a 'imp' c))=I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; let x be Element of Y; A1: ((a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c))).x =('not' (a 'imp' b).x) 'or' ((b 'imp' c) 'imp' (a 'imp' c)).x by BVFUNC_1:def 8 .=('not' (a 'imp' b).x) 'or' ('not' (b 'imp' c).x 'or' (a 'imp' c).x) by BVFUNC_1:def 8; A2: 'not' (b 'imp' c).x ='not' ('not' b.x 'or' c.x) by BVFUNC_1:def 8 .=b.x '&' 'not' c.x; A3: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; A4: (a 'imp' c).x ='not' a.x 'or' c.x by BVFUNC_1:def 8; A5: now per cases by XBOOLEAN:def 3; case c.x=TRUE; hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10; end; case c.x=FALSE; then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' c.x 'or' c.x)=TRUE; end; end; A6: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; 'not' (a 'imp' b).x ='not' ('not' a.x 'or' b.x) by BVFUNC_1:def 8 .=a.x '&' 'not' b.x; then ('not' (a 'imp' b).x) 'or' ('not' (b 'imp' c).x 'or' (a 'imp' c).x ) =(((b.x '&' 'not' c.x) 'or' ('not' a.x 'or' c.x)) 'or' a.x) '&' (((b.x '&' 'not' c.x) 'or' ('not' a.x 'or' c.x)) 'or' 'not' b.x) by A2,A4,XBOOLEAN:9 .=((b.x '&' 'not' c.x) 'or' ((c.x 'or' 'not' a.x) 'or' a.x)) '&' (((b. x '&' 'not' c.x) 'or' ('not' a.x 'or' c.x)) 'or' 'not' b.x) by BINARITH:11 .=((b.x '&' 'not' c.x) 'or' (c.x 'or' ('not' a.x 'or' a.x))) '&' ((( 'not' a.x 'or' c.x) 'or' (b.x '&' 'not' c.x)) 'or' 'not' b.x) by BINARITH:11 .=((b.x '&' 'not' c.x) 'or' (c.x 'or' ('not' a.x 'or' a.x))) '&' (( 'not' a.x 'or' c.x) 'or' (('not' c.x '&' b.x) 'or' 'not' b.x)) by BINARITH:11 .=((b.x '&' 'not' c.x) 'or' (c.x 'or' ('not' a.x 'or' a.x))) '&' (( 'not' a.x 'or' c.x) 'or' (('not' b.x 'or' 'not' c.x) '&' ('not' b.x 'or' b.x))) by XBOOLEAN:9 .=((b.x '&' 'not' c.x) 'or' TRUE) '&' (('not' a.x 'or' c.x) 'or' (( 'not' b.x 'or' 'not' c.x) '&' TRUE)) by A3,A6,BINARITH:10 .=TRUE '&' (('not' a.x 'or' c.x) 'or' (('not' b.x 'or' 'not' c.x) '&' TRUE)) by BINARITH:10 .=(('not' a.x 'or' c.x) 'or' (TRUE '&' ('not' b.x 'or' 'not' c.x))) by MARGREL1:14 .=('not' a.x 'or' c.x) 'or' ('not' c.x 'or' 'not' b.x) by MARGREL1:14 .=(('not' a.x 'or' c.x) 'or' 'not' c.x) 'or' 'not' b.x by BINARITH:11 .=('not' a.x 'or' TRUE) 'or' 'not' b.x by A5,BINARITH:11 .=TRUE 'or' 'not' b.x by BINARITH:10 .=TRUE by BINARITH:10; hence thesis by A1,BVFUNC_1:def 11; end; theorem Th14: for a,b,c being Function of Y,BOOLEAN st (a 'imp' b)=I_el( Y) holds (b 'imp' c) 'imp' (a 'imp' c)=I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; assume A1: a 'imp' b=I_el(Y); for x being Element of Y holds ((b 'imp' c) 'imp' (a 'imp' c)).x=TRUE proof let x be Element of Y; A2: ((b 'imp' c) 'imp' (a 'imp' c)).x =('not' (b 'imp' c).x) 'or' (a 'imp' c).x by BVFUNC_1:def 8 .='not' ('not' b.x 'or' c.x) 'or' (a 'imp' c).x by BVFUNC_1:def 8 .=('not' a.x 'or' c.x) 'or' (b.x '&' 'not' c.x) by BVFUNC_1:def 8; A3: now per cases by XBOOLEAN:def 3; case c.x=TRUE; hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10; end; case c.x=FALSE; then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' c.x 'or' c.x)=TRUE; end; end; (a 'imp' b).x=TRUE by A1,BVFUNC_1:def 11; then A4: 'not' a.x 'or' b.x=TRUE by BVFUNC_1:def 8; A5: 'not' a.x=TRUE or 'not' a.x=FALSE by XBOOLEAN:def 3; now per cases by A4,A5,BINARITH:3; case 'not' a.x=TRUE; then ((b 'imp' c) 'imp' (a 'imp' c)).x =TRUE 'or' (b.x '&' 'not' c.x) by A2,BINARITH:10 .=TRUE by BINARITH:10; hence thesis; end; case b.x=TRUE; then ((b 'imp' c) 'imp' (a 'imp' c)).x =('not' a.x 'or' c.x) 'or' 'not' c.x by A2,MARGREL1:14 .='not' a.x 'or' TRUE by A3,BINARITH:11 .=TRUE by BINARITH:10; hence thesis; end; end; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem Th15: for a,b being Function of Y,BOOLEAN holds b 'imp' (a 'imp' b) =I_el(Y) proof let a,b be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; (b 'imp' (a 'imp' b)).x =('not' b.x) 'or' (a 'imp' b).x by BVFUNC_1:def 8 .=('not' b.x) 'or' (b.x 'or' 'not' a.x) by BVFUNC_1:def 8 .=TRUE 'or' 'not' a.x by A1,BINARITH:11 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem for a,b,c being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' c ) 'imp' (b 'imp' c)=I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; b 'imp' (a 'imp' b) =I_el(Y) by Th15; hence thesis by Th14; end; theorem for a,b being Function of Y,BOOLEAN holds b 'imp' ((b 'imp' a) 'imp' a)=I_el(Y) proof let a,b be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; A2: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; (b 'imp' ((b 'imp' a) 'imp' a)).x = 'not' b.x 'or' ((b 'imp' a) 'imp' a).x by BVFUNC_1:def 8 .= 'not' b.x 'or' ('not' (b 'imp' a).x 'or' a.x) by BVFUNC_1:def 8 .= 'not' b.x 'or' ('not' ('not' b.x 'or' a.x) 'or' a.x) by BVFUNC_1:def 8 .= 'not' b.x 'or' ((a.x 'or' b.x) '&' TRUE) by A2,XBOOLEAN:9 .= 'not' b.x 'or' (a.x 'or' b.x) by MARGREL1:14 .= 'not' b.x 'or' b.x 'or' a.x by BINARITH:11 .=TRUE by A1,BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem :: Contraposition for a,b,c being Function of Y,BOOLEAN holds (c 'imp' (b 'imp' a) ) 'imp' (b 'imp' (c 'imp' a))=I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; A2: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; A3: now per cases by XBOOLEAN:def 3; case c.x=TRUE; hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10; end; case c.x=FALSE; then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' c.x 'or' c.x)=TRUE; end; end; ((c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a))).x =('not' (c 'imp' (b 'imp' a)).x) 'or' (b 'imp' (c 'imp' a)).x by BVFUNC_1:def 8 .=('not' ('not' c.x 'or' (b 'imp' a).x)) 'or' (b 'imp' (c 'imp' a)).x by BVFUNC_1:def 8 .=('not' ('not' c.x 'or' ('not' b.x 'or' a.x))) 'or' (b 'imp' (c 'imp' a)).x by BVFUNC_1:def 8 .=('not' ('not' c.x 'or' ('not' b.x 'or' a.x))) 'or' ('not' b.x 'or' ( c 'imp' a).x) by BVFUNC_1:def 8 .=((c.x '&' ('not' 'not' b.x '&' 'not' a.x))) 'or' ('not' b.x 'or' ( 'not' c.x 'or' a.x)) by BVFUNC_1:def 8 .=(('not' c.x 'or' a.x) 'or' 'not' b.x) 'or' (b.x '&' (c.x '&' 'not' a .x)) by MARGREL1:16 .=((('not' c.x 'or' a.x) 'or' 'not' b.x) 'or' b.x) '&' ((('not' c.x 'or' a.x) 'or' 'not' b.x) 'or' (c.x '&' 'not' a.x)) by XBOOLEAN:9 .=(('not' c.x 'or' a.x) 'or' TRUE) '&' ((('not' c.x 'or' a.x) 'or' 'not' b.x) 'or' (c.x '&' 'not' a.x)) by A1,BINARITH:11 .=TRUE '&' ((('not' c.x 'or' a.x) 'or' 'not' b.x) 'or' (c.x '&' 'not' a.x)) by BINARITH:10 .=((('not' c.x 'or' a.x) 'or' 'not' b.x) 'or' (c.x '&' 'not' a.x)) by MARGREL1:14 .=(((a.x 'or' 'not' b.x) 'or' 'not' c.x) 'or' (c.x '&' 'not' a.x)) by BINARITH:11 .=((a.x 'or' 'not' b.x) 'or' ('not' c.x 'or' (c.x '&' 'not' a.x))) by BINARITH:11 .=((a.x 'or' 'not' b.x) 'or' (TRUE '&' ('not' c.x 'or' 'not' a.x))) by A3 ,XBOOLEAN:9 .=('not' b.x 'or' a.x) 'or' ('not' c.x 'or' 'not' a.x) by MARGREL1:14 .=(('not' b.x 'or' a.x) 'or' 'not' a.x) 'or' 'not' c.x by BINARITH:11 .=('not' b.x 'or' TRUE) 'or' 'not' c.x by A2,BINARITH:11 .=TRUE 'or' 'not' c.x by BINARITH:10 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem for a,b,c being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' (( a 'imp' b) 'imp' (a 'imp' c))=I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; A2: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; A3: now per cases by XBOOLEAN:def 3; case c.x=TRUE; hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10; end; case c.x=FALSE; then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' c.x 'or' c.x)=TRUE; end; end; ((b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))).x ='not' (b 'imp' c).x 'or' ((a 'imp' b) 'imp' (a 'imp' c)).x by BVFUNC_1:def 8 .='not' (b 'imp' c).x 'or' ('not' (a 'imp' b).x 'or' (a 'imp' c).x) by BVFUNC_1:def 8 .='not' ('not' b.x 'or' c.x) 'or' ('not' (a 'imp' b).x 'or' (a 'imp' c ).x) by BVFUNC_1:def 8 .='not' ('not' b.x 'or' c.x) 'or' ('not' ('not' a.x 'or' b.x) 'or' (a 'imp' c).x) by BVFUNC_1:def 8 .=(b.x '&' 'not' c.x) 'or' (('not' 'not' a.x '&' 'not' b.x) 'or' ( 'not' a.x 'or' c.x)) by BVFUNC_1:def 8 .=(((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) 'or' 'not' c.x) '&' (((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) 'or' b.x) by XBOOLEAN:9 .=((a.x '&' 'not' b.x) 'or' (('not' a.x 'or' c.x) 'or' 'not' c.x)) '&' (((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) 'or' b.x) by BINARITH:11 .=((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' TRUE)) '&' (((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) 'or' b.x) by A3,BINARITH:11 .=((a.x '&' 'not' b.x) 'or' TRUE) '&' (((a.x '&' 'not' b.x) 'or' ( 'not' a.x 'or' c.x)) 'or' b.x) by BINARITH:10 .=TRUE '&' (((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) 'or' b.x) by BINARITH:10 .=(('not' b.x '&' a.x) 'or' ('not' a.x 'or' c.x)) 'or' b.x by MARGREL1:14 .=((('not' a.x 'or' c.x) 'or' 'not' b.x) '&' (('not' a.x 'or' c.x) 'or' a.x)) 'or' b.x by XBOOLEAN:9 .=((('not' a.x 'or' c.x) 'or' 'not' b.x) '&' (c.x 'or' ('not' a.x 'or' a.x))) 'or' b.x by BINARITH:11 .=((('not' a.x 'or' c.x) 'or' 'not' b.x) '&' TRUE) 'or' b.x by A1, BINARITH:10 .=(('not' a.x 'or' c.x) 'or' 'not' b.x) 'or' b.x by MARGREL1:14 .=('not' a.x 'or' c.x) 'or' TRUE by A2,BINARITH:11 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem :: A Hilbert axiom for a,b,c being Function of Y,BOOLEAN holds (b 'imp' (b 'imp' c) ) 'imp' (b 'imp' c)=I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; A2: now per cases by XBOOLEAN:def 3; case c.x=TRUE; hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10; end; case c.x=FALSE; then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' c.x 'or' c.x)=TRUE; end; end; ((b 'imp' (b 'imp' c)) 'imp' (b 'imp' c)).x ='not' (b 'imp' (b 'imp' c)).x 'or' (b 'imp' c).x by BVFUNC_1:def 8 .='not' ('not' b.x 'or' (b 'imp' c).x) 'or' (b 'imp' c).x by BVFUNC_1:def 8 .='not' ('not' b.x 'or' ('not' b.x 'or' c.x)) 'or' (b 'imp' c).x by BVFUNC_1:def 8 .=(b.x '&' ('not' 'not' b.x '&' 'not' c.x)) 'or' ('not' b.x 'or' c.x) by BVFUNC_1:def 8 .=((b.x '&' b.x) '&' 'not' c.x) 'or' ('not' b.x 'or' c.x) by MARGREL1:16 .=((c.x 'or' 'not' b.x) 'or' b.x) '&' (('not' b.x 'or' c.x) 'or' 'not' c.x) by XBOOLEAN:9 .=(c.x 'or' TRUE) '&' (('not' b.x 'or' c.x) 'or' 'not' c.x) by A1, BINARITH:11 .=TRUE '&' (('not' b.x 'or' c.x) 'or' 'not' c.x) by BINARITH:10 .=(('not' b.x 'or' c.x) 'or' 'not' c.x) by MARGREL1:14 .='not' b.x 'or' TRUE by A2,BINARITH:11 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem Th21: :: Frege's law for a,b,c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))=I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; A2: now per cases by XBOOLEAN:def 3; case c.x=TRUE; hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10; end; case c.x=FALSE; then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' c.x 'or' c.x)=TRUE; end; end; A3: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; ((a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))).x = 'not' (a 'imp' (b 'imp' c)).x 'or' ((a 'imp' b) 'imp' (a 'imp' c)).x by BVFUNC_1:def 8 .='not' ('not' a.x 'or' (b 'imp' c).x) 'or' ((a 'imp' b) 'imp' (a 'imp' c)).x by BVFUNC_1:def 8 .='not' ('not' a.x 'or' ('not' b.x 'or' c.x)) 'or' ((a 'imp' b) 'imp' (a 'imp' c)).x by BVFUNC_1:def 8 .='not' ('not' a.x 'or' ('not' b.x 'or' c.x)) 'or' ('not' (a 'imp' b). x 'or' (a 'imp' c).x) by BVFUNC_1:def 8 .='not' ('not' a.x 'or' ('not' b.x 'or' c.x)) 'or' ('not' ('not' a.x 'or' b.x) 'or' (a 'imp' c).x) by BVFUNC_1:def 8 .=('not' 'not' a.x '&' ('not' 'not' b.x '&' 'not' c.x)) 'or' (('not' 'not' a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) by BVFUNC_1:def 8 .=(a.x '&' (b.x '&' 'not' c.x)) 'or' (((c.x 'or' 'not' a.x) 'or' a.x) '&' ((c.x 'or' 'not' a.x) 'or' 'not' b.x)) by XBOOLEAN:9 .=(a.x '&' (b.x '&' 'not' c.x)) 'or' ((c.x 'or' TRUE) '&' ((c.x 'or' 'not' a.x) 'or' 'not' b.x)) by A1,BINARITH:11 .=(a.x '&' (b.x '&' 'not' c.x)) 'or' (TRUE '&' ((c.x 'or' 'not' a.x) 'or' 'not' b.x)) by BINARITH:10 .=((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' (a.x '&' (b.x '&' 'not' c .x)) by MARGREL1:14 .=(((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' a.x) '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' (b.x '&' 'not' c.x)) by XBOOLEAN:9 .=(((c.x 'or' 'not' a.x) 'or' a.x) 'or' 'not' b.x) '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' (b.x '&' 'not' c.x)) by BINARITH:11 .=((c.x 'or' TRUE) 'or' 'not' b.x) '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' (b.x '&' 'not' c.x)) by A1,BINARITH:11 .=(TRUE 'or' 'not' b.x) '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' (b.x '&' 'not' c.x)) by BINARITH:10 .=TRUE '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' (b.x '&' 'not' c.x)) by BINARITH:10 .=(((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' (b.x '&' 'not' c.x)) by MARGREL1:14 .=(((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' b.x) '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' 'not' c.x) by XBOOLEAN:9 .=((c.x 'or' 'not' a.x) 'or' TRUE) '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' 'not' c.x) by A3,BINARITH:11 .=TRUE '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' 'not' c.x) by BINARITH:10 .=(('not' b.x 'or' (c.x 'or' 'not' a.x)) 'or' 'not' c.x) by MARGREL1:14 .=((('not' b.x 'or' 'not' a.x) 'or' c.x) 'or' 'not' c.x) by BINARITH:11 .=(('not' b.x 'or' 'not' a.x) 'or' TRUE) by A2,BINARITH:11 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem for a,b being Function of Y,BOOLEAN holds a=I_el(Y) implies (a 'imp' b) 'imp' b=I_el(Y) proof let a,b be Function of Y,BOOLEAN; assume A1: a=I_el(Y); for x being Element of Y holds ((a 'imp' b) 'imp' b).x=TRUE proof let x be Element of Y; A2: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; A3: a.x=TRUE by A1,BVFUNC_1:def 11; ((a 'imp' b) 'imp' b).x ='not' (a 'imp' b).x 'or' b.x by BVFUNC_1:def 8 .='not' ('not' a.x 'or' b.x) 'or' b.x by BVFUNC_1:def 8 .=(b.x 'or' TRUE) '&' TRUE by A3,A2,XBOOLEAN:9 .=b.x 'or' TRUE by MARGREL1:14 .=TRUE by BINARITH:10; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem for a,b,c being Function of Y,BOOLEAN holds c 'imp' (b 'imp' a)= I_el(Y) implies b 'imp' (c 'imp' a)=I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; assume A1: c 'imp' (b 'imp' a)=I_el(Y); for x being Element of Y holds (b 'imp' (c 'imp' a)).x=TRUE proof let x be Element of Y; (c 'imp' (b 'imp' a)).x=TRUE by A1,BVFUNC_1:def 11; then 'not' c.x 'or' (b 'imp' a).x=TRUE by BVFUNC_1:def 8; then A2: 'not' c.x 'or' ('not' b.x 'or' a.x)=TRUE by BVFUNC_1:def 8; (b 'imp' (c 'imp' a)).x ='not' b.x 'or' (c 'imp' a).x by BVFUNC_1:def 8 .='not' b.x 'or' ('not' c.x 'or' a.x) by BVFUNC_1:def 8 .=TRUE by A2,BINARITH:11; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem for a,b,c being Function of Y,BOOLEAN holds c 'imp' (b 'imp' a)= I_el(Y) & b=I_el(Y) implies c 'imp' a=I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; assume that A1: c 'imp' (b 'imp' a)=I_el(Y) and A2: b=I_el(Y); for x being Element of Y holds (c 'imp' a).x=TRUE proof let x be Element of Y; (c 'imp' (b 'imp' a)).x=TRUE by A1,BVFUNC_1:def 11; then 'not' c.x 'or' (b 'imp' a).x=TRUE by BVFUNC_1:def 8; then A3: 'not' c.x 'or' ('not' b.x 'or' a.x)=TRUE by BVFUNC_1:def 8; 'not' c.x 'or' (FALSE 'or' a.x)=TRUE by A3,A2,BVFUNC_1:def 11,MARGREL1:11; then 'not' c.x 'or' a.x=TRUE by BINARITH:3; hence thesis by BVFUNC_1:def 8; end; hence thesis by BVFUNC_1:def 11; end; theorem Th25: for a being Function of Y,BOOLEAN holds I_el Y 'imp' (I_el Y 'imp' a)=I_el Y implies a=I_el Y proof let a be Function of Y,BOOLEAN; assume I_el Y 'imp' (I_el Y 'imp' a)=I_el(Y); then I_el Y 'imp' a=I_el(Y) by Th2; hence thesis by Th2; end; theorem for b,c being Function of Y,BOOLEAN holds b 'imp' (b 'imp' c)= I_el(Y) implies b 'imp' c = I_el(Y) proof let b,c be Function of Y,BOOLEAN; assume A1: b 'imp' (b 'imp' c)=I_el(Y); for x being Element of Y holds (b 'imp' c).x=TRUE proof let x be Element of Y; A2: (b 'imp' c).x='not' b.x 'or' c.x by BVFUNC_1:def 8; (b 'imp' (b 'imp' c)).x=TRUE by A1,BVFUNC_1:def 11; then 'not' b.x 'or' (b 'imp' c).x=TRUE by BVFUNC_1:def 8; then 'not' b.x 'or' ('not' b.x 'or' c.x)=TRUE by BVFUNC_1:def 8; then A3: ('not' b.x 'or' 'not' b.x) 'or' c.x=TRUE by BINARITH:11; A4: 'not' b.x=TRUE or 'not' b.x=FALSE by XBOOLEAN:def 3; now per cases by A3,A4,BINARITH:3; case 'not' b.x=TRUE; hence thesis by A2,BINARITH:10; end; case c.x=TRUE; hence thesis by A2,BINARITH:10; end; end; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem for a,b,c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c) ) = I_el(Y) implies (a 'imp' b) 'imp' (a 'imp' c) = I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; assume A1: a 'imp' (b 'imp' c)=I_el(Y); for x being Element of Y holds ((a 'imp' b) 'imp' (a 'imp' c)).x=TRUE proof let x be Element of Y; A2: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; (a 'imp' (b 'imp' c)).x=TRUE by A1,BVFUNC_1:def 11; then 'not' a.x 'or' (b 'imp' c).x=TRUE by BVFUNC_1:def 8; then A3: 'not' a.x 'or' ('not' b.x 'or' c.x)=TRUE by BVFUNC_1:def 8; ((a 'imp' b) 'imp' (a 'imp' c)).x ='not' (a 'imp' b).x 'or' (a 'imp' c).x by BVFUNC_1:def 8 .='not' ('not' a.x 'or' b.x) 'or' (a 'imp' c).x by BVFUNC_1:def 8 .=('not' 'not' a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x) by BVFUNC_1:def 8 .=(('not' a.x 'or' c.x) 'or' a.x) '&' (('not' a.x 'or' c.x) 'or' 'not' b.x) by XBOOLEAN:9 .=TRUE '&' (('not' a.x 'or' c.x) 'or' a.x) by A3,BINARITH:11 .=(c.x 'or' 'not' a.x) 'or' a.x by MARGREL1:14 .=c.x 'or' TRUE by A2,BINARITH:11 .=TRUE by BINARITH:10; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem for a,b,c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c) ) = I_el(Y) & a 'imp' b = I_el(Y) implies a 'imp' c = I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; assume a 'imp' (b 'imp' c)=I_el(Y) & a 'imp' b = I_el(Y); then I_el Y 'imp' (I_el Y 'imp' (a 'imp' c))=I_el Y by Th21; hence thesis by Th25; end; theorem for a,b,c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c) ) = I_el(Y) & a 'imp' b = I_el(Y) & a = I_el(Y) implies c = I_el(Y) proof let a,b,c be Function of Y,BOOLEAN; assume that A1: (a 'imp' (b 'imp' c)) = I_el(Y) and A2: a 'imp' b = I_el(Y) and A3: a = I_el(Y); for x being Element of Y holds c.x=TRUE proof let x be Element of Y; (a 'imp' (b 'imp' c)).x=TRUE by A1,BVFUNC_1:def 11; then 'not' a.x 'or' (b 'imp' c).x=TRUE by BVFUNC_1:def 8; then A4: 'not' a.x 'or' ('not' b.x 'or' c.x)=TRUE by BVFUNC_1:def 8; (a 'imp' b).x=TRUE by A2,BVFUNC_1:def 11; then 'not' a.x 'or' b.x=TRUE by BVFUNC_1:def 8; then FALSE 'or' b.x=TRUE by A3,BVFUNC_1:def 11,MARGREL1:11; then b.x=TRUE by BINARITH:3; then FALSE 'or' ('not' TRUE 'or' c.x)=TRUE by A4,A3,BVFUNC_1:def 11,MARGREL1:11; then FALSE 'or' (FALSE 'or' c.x)=TRUE by MARGREL1:11; then (FALSE 'or' c.x)=TRUE by BINARITH:3; hence thesis by BINARITH:3; end; hence thesis by BVFUNC_1:def 11; end; theorem for a,b,c,d being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c ) = I_el(Y) & a 'imp' (c 'imp' d) = I_el(Y) implies a 'imp' (b 'imp' d) = I_el( Y) proof let a,b,c,d be Function of Y,BOOLEAN; assume that A1: a 'imp' (b 'imp' c) = I_el(Y) and A2: a 'imp' (c 'imp' d) = I_el(Y); for x being Element of Y holds (a 'imp' (b 'imp' d)).x=TRUE proof let x be Element of Y; A3: (a 'imp' (b 'imp' d)).x ='not' a.x 'or' (b 'imp' d).x by BVFUNC_1:def 8 .='not' a.x 'or' ('not' b.x 'or' (d).x) by BVFUNC_1:def 8; (a 'imp' (c 'imp' d)).x=TRUE by A2,BVFUNC_1:def 11; then 'not' a.x 'or' (c 'imp' d).x=TRUE by BVFUNC_1:def 8; then A4: 'not' a.x 'or' ('not' c.x 'or' (d).x)=TRUE by BVFUNC_1:def 8; (a 'imp' (b 'imp' c)).x=TRUE by A1,BVFUNC_1:def 11; then 'not' a.x 'or' (b 'imp' c).x=TRUE by BVFUNC_1:def 8; then A5: 'not' a.x 'or' ('not' b.x 'or' c.x)=TRUE by BVFUNC_1:def 8; A6: 'not' a.x=TRUE or 'not' a.x=FALSE by XBOOLEAN:def 3; now per cases by A5,A6,A4,BINARITH:3; case 'not' a.x=TRUE & 'not' a.x=TRUE; hence thesis by A3,BINARITH:10; end; case 'not' a.x=TRUE & ('not' c.x 'or' (d).x)=TRUE; hence thesis by A3,BINARITH:10; end; case ('not' b.x 'or' c.x)=TRUE & 'not' a.x=TRUE; hence thesis by A3,BINARITH:10; end; case A7: ('not' b.x 'or' c.x)=TRUE & ('not' c.x 'or' (d).x)=TRUE; A8: 'not' c.x=TRUE or 'not' c.x=FALSE by XBOOLEAN:def 3; A9: 'not' b.x=TRUE or 'not' b.x=FALSE by XBOOLEAN:def 3; now per cases by A7,A9,A8,BINARITH:3; case 'not' b.x=TRUE & 'not' c.x=TRUE; then (a 'imp' (b 'imp' d)).x ='not' a.x 'or' TRUE by A3,BINARITH:10 .=TRUE by BINARITH:10; hence thesis; end; case 'not' b.x=TRUE & (d).x=TRUE; hence thesis by A3,BINARITH:10; end; case c.x=TRUE & 'not' c.x=TRUE; hence thesis by MARGREL1:11; end; case c.x=TRUE & (d).x=TRUE; then (a 'imp' (b 'imp' d)).x ='not' a.x 'or' TRUE by A3,BINARITH:10 .=TRUE by BINARITH:10; hence thesis; end; end; hence thesis; end; end; hence thesis; end; hence thesis by BVFUNC_1:def 11; end; theorem for a,b being Function of Y,BOOLEAN holds ('not' a 'imp' 'not' b ) 'imp' (b 'imp' a) = I_el(Y) proof let a,b be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; A2: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; (('not' a 'imp' 'not' b) 'imp' (b 'imp' a)).x ='not' ('not' a 'imp' 'not' b).x 'or' (b 'imp' a).x by BVFUNC_1:def 8 .='not' ('not' ('not' a).x 'or' ('not' b).x) 'or' (b 'imp' a).x by BVFUNC_1:def 8 .=('not' 'not' ('not' a).x '&' 'not' ('not' b).x) 'or' ('not' b.x 'or' a.x) by BVFUNC_1:def 8 .=(('not' b.x 'or' a.x) 'or' ('not' a).x) '&' (('not' b.x 'or' a.x) 'or' 'not' ('not' b).x) by XBOOLEAN:9 .=('not' b.x 'or' (a.x 'or' ('not' a).x)) '&' (('not' b.x 'or' a.x) 'or' 'not' ('not' b).x) by BINARITH:11 .=('not' b.x 'or' TRUE) '&' (('not' b.x 'or' a.x) 'or' 'not' ('not' b) .x) by A1,MARGREL1:def 19 .=TRUE '&' (('not' b.x 'or' a.x) 'or' 'not' ('not' b).x) by BINARITH:10 .=((a.x 'or' 'not' b.x) 'or' 'not' ('not' b).x) by MARGREL1:14 .=(a.x 'or' ('not' b.x 'or' 'not' ('not' b).x)) by BINARITH:11 .=(a.x 'or' TRUE) by A2,MARGREL1:def 19 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem for a,b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ( 'not' b 'imp' 'not' a)=I_el(Y) proof let a,b be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; A2: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; ((a 'imp' b) 'imp' ('not' b 'imp' 'not' a)).x ='not' (a 'imp' b).x 'or' ('not' b 'imp' 'not' a).x by BVFUNC_1:def 8 .='not' ('not' a.x 'or' b.x) 'or' ('not' b 'imp' 'not' a).x by BVFUNC_1:def 8 .=('not' 'not' a.x '&' 'not' b.x) 'or' ('not' ('not' b).x 'or' ('not' a).x) by BVFUNC_1:def 8 .=(a.x '&' 'not' b.x) 'or' ('not' 'not' b.x 'or' ('not' a).x) by MARGREL1:def 19 .=(b.x 'or' 'not' a.x) 'or' (a.x '&' 'not' b.x) by MARGREL1:def 19 .=((b.x 'or' 'not' a.x) 'or' a.x) '&' ((b.x 'or' 'not' a.x) 'or' 'not' b.x) by XBOOLEAN:9 .=(b.x 'or' TRUE) '&' ((b.x 'or' 'not' a.x) 'or' 'not' b.x) by A1, BINARITH:11 .=TRUE '&' ((b.x 'or' 'not' a.x) 'or' 'not' b.x) by BINARITH:10 .=(('not' a.x 'or' b.x) 'or' 'not' b.x) by MARGREL1:14 .=('not' a.x 'or' TRUE) by A2,BINARITH:11 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem for a,b being Function of Y,BOOLEAN holds (a 'imp' 'not' b) 'imp' (b 'imp' 'not' a)=I_el(Y) proof let a,b be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; A2: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; ((a 'imp' 'not' b) 'imp' (b 'imp' 'not' a)).x ='not' (a 'imp' 'not' b ).x 'or' (b 'imp' 'not' a).x by BVFUNC_1:def 8 .='not' ('not' a.x 'or' ('not' b).x) 'or' (b 'imp' 'not' a).x by BVFUNC_1:def 8 .=('not' 'not' a.x '&' 'not' ('not' b).x) 'or' ('not' b.x 'or' ('not' a).x) by BVFUNC_1:def 8 .=(a.x '&' 'not' 'not' b.x) 'or' ('not' b.x 'or' ('not' a).x) by MARGREL1:def 19 .=('not' b.x 'or' 'not' a.x) 'or' (a.x '&' b.x) by MARGREL1:def 19 .=(('not' b.x 'or' 'not' a.x) 'or' a.x) '&' (('not' b.x 'or' 'not' a.x ) 'or' b.x) by XBOOLEAN:9 .=('not' b.x 'or' TRUE) '&' (('not' b.x 'or' 'not' a.x) 'or' b.x) by A1, BINARITH:11 .=TRUE '&' (('not' b.x 'or' 'not' a.x) 'or' b.x) by BINARITH:10 .=(('not' a.x 'or' 'not' b.x) 'or' b.x) by MARGREL1:14 .=('not' a.x 'or' TRUE) by A2,BINARITH:11 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem for a,b being Function of Y,BOOLEAN holds ('not' a 'imp' b) 'imp' ('not' b 'imp' a)=I_el(Y) proof let a,b be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; A2: now per cases by XBOOLEAN:def 3; case b.x=TRUE; hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10; end; case b.x=FALSE; then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' b.x 'or' b.x)=TRUE; end; end; (('not' a 'imp' b) 'imp' ('not' b 'imp' a)).x ='not' ('not' a 'imp' b ).x 'or' ('not' b 'imp' a).x by BVFUNC_1:def 8 .='not' ('not' ('not' a).x 'or' b.x) 'or' ('not' b 'imp' a).x by BVFUNC_1:def 8 .=('not' 'not' ('not' a).x '&' 'not' b.x) 'or' ('not' ('not' b).x 'or' a.x) by BVFUNC_1:def 8 .=('not' a.x '&' 'not' b.x) 'or' ('not' ('not' b).x 'or' a.x) by MARGREL1:def 19 .=(b.x 'or' a.x) 'or' ('not' a.x '&' 'not' b.x) by MARGREL1:def 19 .=((b.x 'or' a.x) 'or' 'not' a.x) '&' ((b.x 'or' a.x) 'or' 'not' b.x) by XBOOLEAN:9 .=(b.x 'or' TRUE) '&' ((b.x 'or' a.x) 'or' 'not' b.x) by A1,BINARITH:11 .=TRUE '&' ((b.x 'or' a.x) 'or' 'not' b.x) by BINARITH:10 .=((a.x 'or' b.x) 'or' 'not' b.x) by MARGREL1:14 .=(a.x 'or' TRUE) by A2,BINARITH:11 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem for a being Function of Y,BOOLEAN holds (a 'imp' 'not' a) 'imp' 'not' a=I_el(Y) proof let a be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; ((a 'imp' 'not' a) 'imp' 'not' a).x ='not' (a 'imp' 'not' a).x 'or' ( 'not' a).x by BVFUNC_1:def 8 .='not' ('not' a.x 'or' ('not' a).x) 'or' ('not' a).x by BVFUNC_1:def 8 .=(a.x '&' 'not' 'not' a.x) 'or' ('not' a).x by MARGREL1:def 19 .=TRUE by A1,MARGREL1:def 19; hence thesis by BVFUNC_1:def 11; end; theorem for a,b being Function of Y,BOOLEAN holds 'not' a 'imp' (a 'imp' b)=I_el(Y) proof let a,b be Function of Y,BOOLEAN; let x be Element of Y; A1: now per cases by XBOOLEAN:def 3; case a.x=TRUE; hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10; end; case a.x=FALSE; then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11 .=TRUE by BINARITH:10; hence ('not' a.x 'or' a.x)=TRUE; end; end; ('not' a 'imp' (a 'imp' b)).x ='not' ('not' a).x 'or' (a 'imp' b).x by BVFUNC_1:def 8 .='not' ('not' a).x 'or' ('not' a.x 'or' b.x) by BVFUNC_1:def 8 .=a.x 'or' ('not' a.x 'or' b.x) by MARGREL1:def 19 .=TRUE 'or' b.x by A1,BINARITH:11 .=TRUE by BINARITH:10; hence thesis by BVFUNC_1:def 11; end; theorem ::De'Morgan for a,b,c being Function of Y,BOOLEAN holds 'not' (a '&' b '&' c )=('not' a) 'or' ('not' b) 'or' ('not' c) proof let a,b,c be Function of Y,BOOLEAN; 'not' (a '&' b '&' c) ='not' (a '&' b) 'or' ('not' c) by BVFUNC_1:14 .=('not' a) 'or' ('not' b) 'or' ('not' c) by BVFUNC_1:14; hence thesis; end; theorem ::De'Morgan for a,b,c being Function of Y,BOOLEAN holds 'not' (a 'or' b 'or' c)=('not' a) '&' ('not' b) '&' ('not' c) proof let a,b,c be Function of Y,BOOLEAN; 'not' (a 'or' b 'or' c) ='not' (a 'or' b) '&' ('not' c) by BVFUNC_1:13 .=('not' a) '&' ('not' b) '&' ('not' c) by BVFUNC_1:13; hence thesis; end; theorem ::Distributive for a,b,c,d being Function of Y,BOOLEAN holds a 'or' (b '&' c '&' d) = (a 'or' b) '&' (a 'or' c) '&' (a 'or' d) proof let a,b,c,d be Function of Y,BOOLEAN; a 'or' (b '&' c '&' d) =(a 'or' (b '&' c)) '&' (a 'or' d) by BVFUNC_1:11 .=((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d) by BVFUNC_1:11; hence thesis; end; theorem ::Distributive for a,b,c,d being Function of Y,BOOLEAN holds a '&' (b 'or' c 'or' d) = (a '&' b) 'or' (a '&' c) 'or' (a '&' d) proof let a,b,c,d be Function of Y,BOOLEAN; a '&' (b 'or' c 'or' d) =(a '&' (b 'or' c)) 'or' (a '&' d) by BVFUNC_1:12 .=(a '&' b) 'or' (a '&' c) 'or' (a '&' d) by BVFUNC_1:12; hence thesis; end;