Copyright (c) 1999 Association of Mizar Users
environ vocabulary FUNCT_2, MARGREL1, BVFUNC_1, ZF_LANG, FUNCT_1, RELAT_1, PARTIT1; notation TARSKI, XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, RELAT_1, FUNCT_1, FRAENKEL, BINARITH, BVFUNC_1; constructors BINARITH, BVFUNC_1; clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL; requirements SUBSET, BOOLE; definitions BVFUNC_1; theorems FUNCT_1, FUNCT_2, MARGREL1, BINARITH, BVFUNC_1, BVFUNC_4, VALUAT_1; begin ::Chap. 1 Propositional Calculus reserve Y for non empty set; theorem for a,b being Element of Funcs(Y,BOOLEAN) holds (a 'imp' b) '&' ('not' a 'imp' b) = b proof let a,b be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj((a 'imp' b) '&' ('not' a 'imp' b),x) = Pj(b,x) proof let x be Element of Y; A2:Pj((a 'imp' b) '&' ('not' a 'imp' b),x) =Pj(a 'imp' b,x) '&' Pj('not' a 'imp' b,x) by VALUAT_1:def 6 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj('not' a 'imp' b,x) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj('not' a,x) 'or' Pj(b,x)) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' 'not' Pj(a,x) 'or' Pj(b,x)) by VALUAT_1:def 5 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' (Pj(a,x) 'or' Pj(b,x)) by MARGREL1:40; now per cases by MARGREL1:39; case Pj(a,x)=TRUE; then Pj((a 'imp' b) '&' ('not' a 'imp' b),x) =(FALSE 'or' Pj(b,x)) '&' (TRUE 'or' Pj(b,x)) by A2,MARGREL1:41 .=(FALSE 'or' Pj(b,x)) '&' TRUE by BINARITH:19 .=TRUE '&' Pj(b,x) by BINARITH:7 .=Pj(b,x) by MARGREL1:50; hence thesis; case Pj(a,x)=FALSE; then Pj((a 'imp' b) '&' ('not' a 'imp' b),x) =(TRUE 'or' Pj(b,x)) '&' (FALSE 'or' Pj(b,x)) by A2,MARGREL1:41 .=TRUE '&' (FALSE 'or' Pj(b,x)) by BINARITH:19 .=TRUE '&' Pj(b,x) by BINARITH:7 .=Pj(b,x) by MARGREL1:50; hence thesis; end; hence thesis; end; consider k3 being Function such that A3: ((a 'imp' b) '&' ('not' a 'imp' b))=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A4: b=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A3,A4; hence ((a 'imp' b) '&' ('not' a 'imp' b))=b by A3,A4,FUNCT_1:9; end; theorem for a,b being Element of Funcs(Y,BOOLEAN) holds (a 'imp' b) '&' (a 'imp' 'not' b) = 'not' a proof let a,b be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj((a 'imp' b) '&' (a 'imp' 'not' b),x) = Pj('not' a,x) proof let x be Element of Y; A2:Pj((a 'imp' b) '&' (a 'imp' 'not' b),x) =Pj(a 'imp' b,x) '&' Pj(a 'imp' 'not' b,x) by VALUAT_1:def 6 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj(a 'imp' 'not' b,x) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(a,x) 'or' Pj('not' b,x)) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(a,x) 'or' 'not' Pj(b,x)) by VALUAT_1:def 5; now per cases by MARGREL1:39; case Pj(b,x)=TRUE; then Pj((a 'imp' b) '&' (a 'imp' 'not' b),x) =('not' Pj(a,x) 'or' TRUE) '&' ('not' Pj(a,x) 'or' FALSE) by A2,MARGREL1:41 .=('not' Pj(a,x) 'or' TRUE) '&' 'not' Pj(a,x) by BINARITH:7 .=TRUE '&' 'not' Pj(a,x) by BINARITH:19 .='not' Pj(a,x) by MARGREL1:50 .=Pj('not' a,x) by VALUAT_1:def 5; hence thesis; case Pj(b,x)=FALSE; then Pj((a 'imp' b) '&' (a 'imp' 'not' b),x) =('not' Pj(a,x) 'or' FALSE) '&' ('not' Pj(a,x) 'or' TRUE) by A2,MARGREL1:41 .='not' Pj(a,x) '&' ('not' Pj(a,x) 'or' TRUE) by BINARITH:7 .=TRUE '&' 'not' Pj(a,x) by BINARITH:19 .='not' Pj(a,x) by MARGREL1:50 .=Pj('not' a,x) by VALUAT_1:def 5; hence thesis; end; hence thesis; end; consider k3 being Function such that A3: ((a 'imp' b) '&' (a 'imp' 'not' b))=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A4: 'not' a=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A3,A4; hence ((a 'imp' b) '&' (a 'imp' 'not' b))='not' a by A3,A4,FUNCT_1:9; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds a 'imp' (b 'or' c) = (a 'imp' b) 'or' (a 'imp' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj(a 'imp' (b 'or' c),x) = Pj((a 'imp' b) 'or' (a 'imp' c),x) proof let x be Element of Y; Pj((a 'imp' b) 'or' (a 'imp' c),x) =Pj(a 'imp' b,x) 'or' Pj(a 'imp' c,x) by BVFUNC_1:def 7 .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' Pj(a 'imp' c,x) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' ('not' Pj(a,x) 'or' Pj(c,x)) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' ('not' Pj(a,x) 'or' Pj(b,x))) 'or' Pj(c,x) by BINARITH:20 .=(('not' Pj(a,x) 'or' 'not' Pj(a,x)) 'or' Pj(b,x)) 'or' Pj(c,x) by BINARITH:20 .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' Pj(c,x) by BINARITH:21 .='not' Pj(a,x) 'or' (Pj(b,x) 'or' Pj(c,x)) by BINARITH:20 .='not' Pj(a,x) 'or' Pj(b 'or' c,x) by BVFUNC_1:def 7 .=Pj(a 'imp' (b 'or' c),x) by BVFUNC_1:def 11; hence thesis; end; consider k3 being Function such that A2: (a 'imp' (b 'or' c))=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: (a 'imp' b) 'or' (a 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence (a 'imp' (b 'or' c))=(a 'imp' b) 'or' (a 'imp' c) by A2,A3,FUNCT_1:9; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds a 'imp' (b '&' c) = (a 'imp' b) '&' (a 'imp' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj(a 'imp' (b '&' c),x) = Pj((a 'imp' b) '&' (a 'imp' c),x) proof let x be Element of Y; Pj((a 'imp' b) '&' (a 'imp' c),x) =Pj(a 'imp' b,x) '&' Pj(a 'imp' c,x) by VALUAT_1:def 6 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj(a 'imp' c,x) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(a,x) 'or' Pj(c,x)) by BVFUNC_1:def 11 .='not' Pj(a,x) 'or' (Pj(b,x) '&' Pj(c,x)) by BINARITH:23 .='not' Pj(a,x) 'or' (Pj(b '&' c,x)) by VALUAT_1:def 6 .=Pj(a 'imp' (b '&' c),x) by BVFUNC_1:def 11; hence thesis; end; consider k3 being Function such that A2: (a 'imp' (b '&' c))=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: (a 'imp' b) '&' (a 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence (a 'imp' (b '&' c))=(a 'imp' b) '&' (a 'imp' c) by A2,A3,FUNCT_1:9; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a 'or' b) 'imp' c = (a 'imp' c) '&' (b 'imp' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj((a 'or' b) 'imp' c,x) = Pj((a 'imp' c) '&' (b 'imp' c),x) proof let x be Element of Y; Pj((a 'imp' c) '&' (b 'imp' c),x) =Pj(a 'imp' c,x) '&' Pj(b 'imp' c,x) by VALUAT_1:def 6 .=('not' Pj(a,x) 'or' Pj(c,x)) '&' Pj(b 'imp' c,x) by BVFUNC_1:def 11 .=(Pj(c,x) 'or' 'not' Pj(a,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x)) by BVFUNC_1:def 11 .=Pj(c,x) 'or' ('not' Pj(a,x) '&' 'not' Pj(b,x)) by BINARITH:23 .='not'( Pj(a,x) 'or' Pj(b,x)) 'or' Pj(c,x) by BINARITH:10 .='not' Pj(a 'or' b,x) 'or' Pj(c,x) by BVFUNC_1:def 7 .=Pj((a 'or' b) 'imp' c,x) by BVFUNC_1:def 11; hence thesis; end; consider k3 being Function such that A2: ((a 'or' b) 'imp' c)=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: (a 'imp' c) '&' (b 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence ((a 'or' b) 'imp' c)=(a 'imp' c) '&' (b 'imp' c) by A2,A3,FUNCT_1:9; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a '&' b) 'imp' c = (a 'imp' c) 'or' (b 'imp' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj((a '&' b) 'imp' c,x) = Pj((a 'imp' c) 'or' (b 'imp' c),x) proof let x be Element of Y; Pj((a 'imp' c) 'or' (b 'imp' c),x) =Pj(a 'imp' c,x) 'or' Pj(b 'imp' c,x) by BVFUNC_1:def 7 .=('not' Pj(a,x) 'or' Pj(c,x)) 'or' Pj(b 'imp' c,x) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' Pj(c,x)) 'or' ('not' Pj(b,x) 'or' Pj(c,x)) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' (Pj(c,x) 'or' 'not' Pj(b,x))) 'or' Pj(c,x) by BINARITH:20 .=(('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' Pj(c,x)) 'or' Pj(c,x) by BINARITH:20 .=('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' (Pj(c,x) 'or' Pj(c,x)) by BINARITH:20 .=('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' Pj(c,x) by BINARITH:21 .='not'( Pj(a,x) '&' Pj(b,x)) 'or' Pj(c,x) by BINARITH:9 .='not' Pj(a '&' b,x) 'or' Pj(c,x) by VALUAT_1:def 6 .=Pj((a '&' b) 'imp' c,x) by BVFUNC_1:def 11; hence thesis; end; consider k3 being Function such that A2: ((a '&' b) 'imp' c)=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: (a 'imp' c) 'or' (b 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence ((a '&' b) 'imp' c)=(a 'imp' c) 'or' (b 'imp' c) by A2,A3,FUNCT_1:9; end; theorem Th7: for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a '&' b) 'imp' c = a 'imp' (b 'imp' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj((a '&' b) 'imp' c,x) = Pj(a 'imp' (b 'imp' c),x) proof let x be Element of Y; Pj(a 'imp' (b 'imp' c),x) ='not' Pj(a,x) 'or' Pj(b 'imp' c,x) by BVFUNC_1:def 11 .='not' Pj(a,x) 'or' ('not' Pj(b,x) 'or' Pj(c,x)) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' Pj(c,x) by BINARITH:20 .='not'( Pj(a,x) '&' Pj(b,x)) 'or' Pj(c,x) by BINARITH:9 .='not' Pj(a '&' b,x) 'or' Pj(c,x) by VALUAT_1:def 6 .=Pj((a '&' b) 'imp' c,x) by BVFUNC_1:def 11; hence thesis; end; consider k3 being Function such that A2: ((a '&' b) 'imp' c)=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: a 'imp' (b 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence ((a '&' b) 'imp' c)=a 'imp' (b 'imp' c) by A2,A3,FUNCT_1:9; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a '&' b) 'imp' c = a 'imp' ('not' b 'or' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj((a '&' b) 'imp' c,x) = Pj(a 'imp' ('not' b 'or' c),x) proof let x be Element of Y; Pj(a 'imp' ('not' b 'or' c),x) =Pj(a 'imp' (b 'imp' c),x) by BVFUNC_4:8; hence thesis by Th7; end; consider k3 being Function such that A2: ((a '&' b) 'imp' c)=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: a 'imp' ('not' b 'or' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence ((a '&' b) 'imp' c)=a 'imp' ('not' b 'or' c) by A2,A3,FUNCT_1:9; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds a 'imp' (b 'or' c) = (a '&' 'not' b) 'imp' c proof let a,b,c be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj(a 'imp' (b 'or' c),x) = Pj((a '&' 'not' b) 'imp' c,x) proof let x be Element of Y; Pj((a '&' 'not' b) 'imp' c,x) ='not' Pj(a '&' 'not' b,x) 'or' Pj(c,x) by BVFUNC_1:def 11 .='not'( Pj(a,x) '&' Pj('not' b,x)) 'or' Pj(c,x) by VALUAT_1:def 6 .=('not' Pj(a,x) 'or' 'not' Pj('not' b,x)) 'or' Pj(c,x) by BINARITH:9 .=('not' Pj(a,x) 'or' 'not' 'not' Pj(b,x)) 'or' Pj(c,x) by VALUAT_1:def 5 .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' Pj(c,x) by MARGREL1:40 .='not' Pj(a,x) 'or' (Pj(b,x) 'or' Pj(c,x)) by BINARITH:20 .='not' Pj(a,x) 'or' Pj(b 'or' c,x) by BVFUNC_1:def 7 .=Pj(a 'imp' (b 'or' c),x) by BVFUNC_1:def 11; hence thesis; end; consider k3 being Function such that A2: (a 'imp' (b 'or' c))=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: (a '&' 'not' b) 'imp' c =k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence (a 'imp' (b 'or' c))=(a '&' 'not' b) 'imp' c by A2,A3,FUNCT_1:9; end; theorem for a,b being Element of Funcs(Y,BOOLEAN) holds a '&' (a 'imp' b) = a '&' b proof let a,b be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj(a '&' (a 'imp' b),x) = Pj(a '&' b,x) proof let x be Element of Y; Pj(a '&' (a 'imp' b),x) =Pj(a,x) '&' Pj(a 'imp' b,x) by VALUAT_1:def 6 .=Pj(a,x) '&' ('not' Pj(a,x) 'or' Pj(b,x)) by BVFUNC_1:def 11 .=(Pj(a,x) '&' 'not' Pj(a,x)) 'or' (Pj(a,x) '&' Pj(b,x)) by BINARITH:22 .=FALSE 'or' (Pj(a,x) '&' Pj(b,x)) by MARGREL1:46 .=Pj(a,x) '&' Pj(b,x) by BINARITH:7 .=Pj(a '&' b,x) by VALUAT_1:def 6; hence thesis; end; consider k3 being Function such that A2: (a '&' (a 'imp' b))=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: a '&' b=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence (a '&' (a 'imp' b))=a '&' b by A2,A3,FUNCT_1:9; end; theorem for a,b being Element of Funcs(Y,BOOLEAN) holds (a 'imp' b) '&' 'not' b = 'not' a '&' 'not' b proof let a,b be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj((a 'imp' b) '&' 'not' b,x) = Pj('not' a '&' 'not' b,x) proof let x be Element of Y; Pj((a 'imp' b) '&' 'not' b,x) =Pj(a 'imp' b,x) '&' Pj('not' b,x) by VALUAT_1:def 6 .=Pj('not' b,x) '&' ('not' Pj(a,x) 'or' Pj(b,x)) by BVFUNC_1:def 11 .=(Pj('not' b,x) '&' 'not' Pj(a,x)) 'or' (Pj('not' b,x) '&' Pj(b,x)) by BINARITH:22 .=(Pj('not' b,x) '&' 'not' Pj(a,x)) 'or' (Pj(b,x) '&' 'not' Pj(b,x)) by VALUAT_1:def 5 .=(Pj('not' b,x) '&' 'not' Pj(a,x)) 'or' FALSE by MARGREL1:46 .=Pj('not' b,x) '&' 'not' Pj(a,x) by BINARITH:7 .=Pj('not' b,x) '&' Pj('not' a,x) by VALUAT_1:def 5 .=Pj('not' a '&' 'not' b,x) by VALUAT_1:def 6; hence thesis; end; consider k3 being Function such that A2: ((a 'imp' b) '&' 'not' b)=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: 'not' a '&' 'not' b=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence ((a 'imp' b) '&' 'not' b)='not' a '&' 'not' b by A2,A3,FUNCT_1:9; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a 'imp' b) '&' (b 'imp' c) = (a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj((a 'imp' b) '&' (b 'imp' c),x) = Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x) proof let x be Element of Y; A2:Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x) =Pj((a 'imp' b) '&' (b 'imp' c),x) '&' Pj((a 'imp' c),x) by VALUAT_1:def 6 .=(Pj(a 'imp' b,x) '&' Pj(b 'imp' c,x)) '&' Pj((a 'imp' c),x) by VALUAT_1:def 6 .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj(b 'imp' c,x)) '&' Pj((a 'imp' c),x) by BVFUNC_1:def 11 .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' Pj((a 'imp' c),x) by BVFUNC_1:def 11 .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' ('not' Pj(a,x) 'or' Pj(c,x)) by BVFUNC_1:def 11 .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' 'not' Pj(a,x) 'or' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' Pj(c,x) by BINARITH:22; A3:Pj((a 'imp' b) '&' (b 'imp' c),x) =Pj(a 'imp' b,x) '&' Pj(b 'imp' c,x) by VALUAT_1:def 6 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj(b 'imp' c,x) by BVFUNC_1:def 11 .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x)) by BVFUNC_1:def 11; A4:(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) =(Pj(a 'imp' b,x) '&' ('not' Pj(b,x) 'or' Pj(c,x))) by BVFUNC_1:def 11 .=Pj(a 'imp' b,x) '&' Pj(b 'imp' c,x) by BVFUNC_1:def 11 .=Pj((a 'imp' b) '&' (b 'imp' c),x) by VALUAT_1:def 6; now per cases by MARGREL1:39; case Pj(a,x)=TRUE & Pj(c,x)=TRUE; then Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x) =(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' FALSE 'or' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' TRUE by A2,MARGREL1:41 .=FALSE 'or' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' TRUE by MARGREL1:49 .=FALSE 'or' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) by MARGREL1:50 .=Pj((a 'imp' b) '&' (b 'imp' c),x) by A4,BINARITH:7; hence thesis; case A5:Pj(a,x)=TRUE & Pj(c,x)=FALSE; then A6:Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x) =(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' FALSE 'or' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' FALSE by A2,MARGREL1:41 .=FALSE '&' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) by BINARITH:21 .=FALSE by MARGREL1:49; Pj((a 'imp' b) '&' (b 'imp' c),x) =(FALSE 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' FALSE) by A3,A5,MARGREL1:41 .=(FALSE 'or' Pj(b,x)) '&' 'not' Pj(b,x) by BINARITH:7 .=Pj(b,x) '&' 'not' Pj(b,x) by BINARITH:7 .=FALSE by MARGREL1:46; hence thesis by A6; case Pj(a,x)=FALSE & Pj(c,x)=TRUE; then Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x) =(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' TRUE 'or' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' TRUE by A2,MARGREL1:41 .=TRUE '&' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) by BINARITH:21 .=Pj((a 'imp' b) '&' (b 'imp' c),x) by A4,MARGREL1:50; hence thesis; case Pj(a,x)=FALSE & Pj(c,x)=FALSE; then Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x) =TRUE '&' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) 'or' FALSE '&' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) by A2,MARGREL1:41 .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) 'or' FALSE '&' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) by MARGREL1:50 .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) 'or' FALSE by MARGREL1:49 .=Pj((a 'imp' b) '&' (b 'imp' c),x) by A4,BINARITH:7; hence thesis; end; hence thesis; end; consider k3 being Function such that A7: ((a 'imp' b) '&' (b 'imp' c))=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A8: (a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c)= k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A7,A8; hence ((a 'imp' b) '&' (b 'imp' c))= (a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c) by A7,A8,FUNCT_1:9; end; theorem for a being Element of Funcs(Y,BOOLEAN) holds I_el(Y) 'imp' a = a proof let a be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj(I_el(Y) 'imp' a,x) = Pj(a,x) proof let x be Element of Y; Pj(I_el(Y) 'imp' a,x) ='not' Pj(I_el(Y),x) 'or' Pj(a,x) by BVFUNC_1:def 11 .='not' TRUE 'or' Pj(a,x) by BVFUNC_1:def 14 .=FALSE 'or' Pj(a,x) by MARGREL1:41; hence thesis by BINARITH:7; end; consider k3 being Function such that A2: (I_el(Y) 'imp' a)=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: a=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence (I_el(Y) 'imp' a)=a by A2,A3,FUNCT_1:9; end; theorem for a being Element of Funcs(Y,BOOLEAN) holds a 'imp' O_el(Y) = 'not' a proof let a be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj(a 'imp' O_el(Y),x) = Pj('not' a,x) proof let x be Element of Y; Pj(a 'imp' O_el(Y),x) ='not' Pj(a,x) 'or' Pj(O_el(Y),x) by BVFUNC_1:def 11 .='not' Pj(a,x) 'or' FALSE by BVFUNC_1:def 13 .='not' Pj(a,x) by BINARITH:7; hence thesis by VALUAT_1:def 5; end; consider k3 being Function such that A2: (a 'imp' O_el(Y))=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: 'not' a=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence (a 'imp' O_el(Y))='not' a by A2,A3,FUNCT_1:9; end; theorem for a being Element of Funcs(Y,BOOLEAN) holds O_el(Y) 'imp' a = I_el(Y) proof let a be Element of Funcs(Y,BOOLEAN); for x being Element of Y holds Pj(O_el(Y) 'imp' a,x) = TRUE proof let x be Element of Y; Pj(O_el(Y) 'imp' a,x) ='not' Pj(O_el(Y),x) 'or' Pj(a,x) by BVFUNC_1:def 11 .='not' FALSE 'or' Pj(a,x) by BVFUNC_1:def 13 .=TRUE 'or' Pj(a,x) by MARGREL1:41; hence thesis by BINARITH:19; end; hence thesis by BVFUNC_1:def 14; end; theorem for a being Element of Funcs(Y,BOOLEAN) holds a 'imp' I_el(Y) = I_el(Y) proof let a be Element of Funcs(Y,BOOLEAN); for x being Element of Y holds Pj(a 'imp' I_el(Y),x) = TRUE proof let x be Element of Y; Pj(a 'imp' I_el(Y),x) ='not' Pj(a,x) 'or' Pj(I_el(Y),x) by BVFUNC_1:def 11 .='not' Pj(a,x) 'or' TRUE by BVFUNC_1:def 14; hence thesis by BINARITH:19; end; hence thesis by BVFUNC_1:def 14; end; theorem for a being Element of Funcs(Y,BOOLEAN) holds a 'imp' 'not' a = 'not' a proof let a be Element of Funcs(Y,BOOLEAN); A1:for x being Element of Y holds Pj(a 'imp' 'not' a,x) = Pj('not' a,x) proof let x be Element of Y; Pj(a 'imp' 'not' a,x) ='not' Pj(a,x) 'or' Pj('not' a,x) by BVFUNC_1:def 11 .=Pj('not' a,x) 'or' Pj('not' a,x) by VALUAT_1:def 5 .=Pj('not' a,x) by BINARITH:21; hence thesis; end; consider k3 being Function such that A2: (a 'imp' 'not' a)=k3 & dom k3=Y & rng k3 c= BOOLEAN by FUNCT_2:def 2; consider k4 being Function such that A3: 'not' a=k4 & dom k4=Y & rng k4 c= BOOLEAN by FUNCT_2:def 2; Y=dom k3 & Y=dom k4 & (for u being set st u in Y holds k3.u=k4.u)by A1,A2,A3; hence (a 'imp' 'not' a)='not' a by A2,A3,FUNCT_1:9; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a 'imp' b) '<' (c 'imp' a) 'imp' (c 'imp' b) proof let a,b,c be Element of Funcs(Y,BOOLEAN); let z be Element of Y; assume Pj(a 'imp' b,z)=TRUE; then A1:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11; A2: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39; now per cases by A1,A2,BINARITH:7; case A3:'not' Pj(a,z)=TRUE; Pj((c 'imp' a) 'imp' (c 'imp' b),z) ='not' Pj(c 'imp' a,z) 'or' Pj(c 'imp' b,z) by BVFUNC_1:def 11 .='not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' Pj(c 'imp' b,z) by BVFUNC_1:def 11 .=('not' 'not' Pj(c,z) '&' TRUE) 'or' Pj(c 'imp' b,z) by A3,BINARITH:10 .=(TRUE '&' Pj(c,z)) 'or' Pj(c 'imp' b,z) by MARGREL1:40 .=Pj(c,z) 'or' Pj(c 'imp' b,z) by MARGREL1:50 .=Pj(c,z) 'or' ('not' Pj(c,z) 'or' Pj(b,z)) by BVFUNC_1:def 11 .=(Pj(c,z) 'or' 'not' Pj(c,z)) 'or' Pj(b,z) by BINARITH:20 .=TRUE 'or' Pj(b,z) by BINARITH:18 .=TRUE by BINARITH:19; hence thesis; case A4:Pj(b,z)=TRUE; Pj((c 'imp' a) 'imp' (c 'imp' b),z) ='not' Pj(c 'imp' a,z) 'or' Pj(c 'imp' b,z) by BVFUNC_1:def 11 .='not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' Pj(c 'imp' b,z) by BVFUNC_1:def 11 .='not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' TRUE) by A4,BVFUNC_1:def 11 .='not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' TRUE by BINARITH:19 .=TRUE by BINARITH:19; hence thesis; end; hence thesis; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a 'eqv' b) '<' (a 'eqv' c) 'eqv' (b 'eqv' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); let z be Element of Y; assume A1:Pj(a 'eqv' b,z)=TRUE; Pj(a 'eqv' b,z) =Pj((a 'imp' b) '&' (b 'imp' a),z) by BVFUNC_4:7 .=Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z) by VALUAT_1:def 6; then A2:Pj(a 'imp' b,z)=TRUE & Pj(b 'imp' a,z)=TRUE by A1,MARGREL1:45; then A3:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11; A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39; A5: Pj(b 'imp' a,z) = 'not' Pj(b,z) 'or' Pj(a,z) by BVFUNC_1:def 11; Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39; then A6:'not' Pj(b,z)=TRUE or Pj(a,z)=TRUE by A2,A5,BINARITH:7; A7:Pj((a 'eqv' c) 'eqv' (b 'eqv' c),z) =(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(a,z))) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' (('not' Pj(a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z)))) proof Pj((a 'eqv' c) 'eqv' (b 'eqv' c),z) =Pj(((a 'eqv' c) 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' (a 'eqv' c)),z) by BVFUNC_4:7 .=Pj((((a 'imp' c) '&' (c 'imp' a)) 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' (a 'eqv' c)),z) by BVFUNC_4:7 .=Pj((((a 'imp' c) '&' (c 'imp' a)) 'imp' (b 'imp' c) '&' (c 'imp' b)) '&' ((b 'eqv' c) 'imp' (a 'eqv' c)),z) by BVFUNC_4:7 .=Pj((((a 'imp' c) '&' (c 'imp' a)) 'imp' (b 'imp' c) '&' (c 'imp' b)) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' (a 'eqv' c)),z) by BVFUNC_4:7 .=Pj((((a 'imp' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z) by BVFUNC_4:7 .=Pj(((('not' a 'or' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z) by BVFUNC_4:8 .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z) by BVFUNC_4:8 .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp' (('not' b 'or' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z) by BVFUNC_4:8 .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z) by BVFUNC_4:8 .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' b 'or' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z) by BVFUNC_4:8 .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' b 'or' c) '&' ('not' c 'or' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z) by BVFUNC_4:8 .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' b 'or' c) '&' ('not' c 'or' b)) 'imp' (('not' a 'or' c) '&' (c 'imp' a))),z) by BVFUNC_4:8 .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' b 'or' c) '&' ('not' c 'or' b)) 'imp' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_4:8 .=Pj(('not'( ('not' a 'or' c) '&' ('not' c 'or' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' b 'or' c) '&' ('not' c 'or' b)) 'imp' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_4:8 .=Pj(('not'( ('not' a 'or' c) '&' ('not' c 'or' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ('not'( ('not' b 'or' c) '&' ('not' c 'or' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_4:8 .=Pj((('not'( 'not' a 'or' c) 'or' 'not'( 'not' c 'or' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ('not'( ('not' b 'or' c) '&' ('not' c 'or' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_1:17 .=Pj((('not'( 'not' a 'or' c) 'or' 'not'( 'not' c 'or' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (('not'( 'not' b 'or' c) 'or' 'not'( 'not' c 'or' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_1:17 .=Pj(((('not' 'not' a '&' 'not' c) 'or' 'not'( 'not' c 'or' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (('not'( 'not' b 'or' c) 'or' 'not'( 'not' c 'or' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_1:16 .=Pj(((('not' 'not' a '&' 'not' c) 'or' ('not' 'not' c '&' 'not' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (('not'( 'not' b 'or' c) 'or' 'not'( 'not' c 'or' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_1:16 .=Pj(((('not' 'not' a '&' 'not' c) 'or' ('not' 'not' c '&' 'not' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' 'not' b '&' 'not' c) 'or' 'not'( 'not' c 'or' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_1:16 .=Pj(((('not' 'not' a '&' 'not' c) 'or' ('not' 'not' c '&' 'not' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' 'not' b '&' 'not' c) 'or' ('not' 'not' c '&' 'not' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_1:16 .=Pj((((a '&' 'not' c) 'or' ('not' 'not' c '&' 'not' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' 'not' b '&' 'not' c) 'or' ('not' 'not' c '&' 'not' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_1:4 .=Pj((((a '&' 'not' c) 'or' (c '&' 'not' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' 'not' b '&' 'not' c) 'or' ('not' 'not' c '&' 'not' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_1:4 .=Pj((((a '&' 'not' c) 'or' (c '&' 'not' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (((b '&' 'not' c) 'or' ('not' 'not' c '&' 'not' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_1:4 .=Pj((((a '&' 'not' c) 'or' (c '&' 'not' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (((b '&' 'not' c) 'or' (c '&' 'not' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a))),z) by BVFUNC_1:4 .=Pj(((a '&' 'not' c) 'or' (c '&' 'not' a)) 'or' (('not' b 'or' c) '&' ('not' c 'or' b)),z) '&' Pj(((b '&' 'not' c) 'or' (c '&' 'not' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a)),z) by VALUAT_1:def 6 .=(Pj((a '&' 'not' c) 'or' (c '&' 'not' a),z) 'or' Pj(('not' b 'or' c) '&' ('not' c 'or' b),z)) '&' Pj(((b '&' 'not' c) 'or' (c '&' 'not' b)) 'or' (('not' a 'or' c) '&' ('not' c 'or' a)),z) by BVFUNC_1:def 7 .=(Pj((a '&' 'not' c) 'or' (c '&' 'not' a),z) 'or' Pj(('not' b 'or' c) '&' ('not' c 'or' b),z)) '&' (Pj((b '&' 'not' c) 'or' (c '&' 'not' b),z) 'or' Pj(('not' a 'or' c) '&' ('not' c 'or' a),z)) by BVFUNC_1:def 7 .=((Pj(a '&' 'not' c,z) 'or' Pj(c '&' 'not' a,z)) 'or' Pj(('not' b 'or' c) '&' ('not' c 'or' b),z)) '&' (Pj((b '&' 'not' c) 'or' (c '&' 'not' b),z) 'or' Pj(('not' a 'or' c) '&' ('not' c 'or' a),z)) by BVFUNC_1:def 7 .=((Pj(a '&' 'not' c,z) 'or' Pj(c '&' 'not' a,z)) 'or' (Pj('not' b 'or' c,z) '&' Pj('not' c 'or' b,z))) '&' (Pj((b '&' 'not' c) 'or' (c '&' 'not' b),z) 'or' Pj(('not' a 'or' c) '&' ('not' c 'or' a),z)) by VALUAT_1:def 6 .=((Pj(a '&' 'not' c,z) 'or' Pj(c '&' 'not' a,z)) 'or' (Pj('not' b 'or' c,z) '&' Pj('not' c 'or' b,z))) '&' ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or' Pj(('not' a 'or' c) '&' ('not' c 'or' a),z)) by BVFUNC_1:def 7 .=((Pj(a '&' 'not' c,z) 'or' Pj(c '&' 'not' a,z)) 'or' (Pj('not' b 'or' c,z) '&' Pj('not' c 'or' b,z))) '&' ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or' (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z))) by VALUAT_1:def 6 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' Pj(c '&' 'not' a,z)) 'or' (Pj('not' b 'or' c,z) '&' Pj('not' c 'or' b,z))) '&' ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or' (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z))) by VALUAT_1:def 6 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or' (Pj('not' b 'or' c,z) '&' Pj('not' c 'or' b,z))) '&' ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or' (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z))) by VALUAT_1:def 6 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or' ((Pj('not' b,z) 'or' Pj(c,z)) '&' Pj('not' c 'or' b,z))) '&' ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or' (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z))) by BVFUNC_1:def 7 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or' ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or' (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z))) by BVFUNC_1:def 7 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or' ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' Pj(c '&' 'not' b,z)) 'or' (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z))) by VALUAT_1:def 6 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or' ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' b,z))) 'or' (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z))) by VALUAT_1:def 6 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or' ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' b,z))) 'or' ((Pj('not' a,z) 'or' Pj(c,z)) '&' Pj('not' c 'or' a,z))) by BVFUNC_1:def 7 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or' ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' b,z))) 'or' ((Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z)))) by BVFUNC_1:def 7 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(a,z))) 'or' ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' b,z))) 'or' ((Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z)))) by VALUAT_1:def 5 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(a,z))) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' b,z))) 'or' ((Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z)))) by VALUAT_1:def 5 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(a,z))) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' ((Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z)))) by VALUAT_1:def 5 .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(a,z))) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' (('not' Pj(a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z)))) by VALUAT_1:def 5; hence thesis; end; now per cases by A3,A4,BINARITH:7; case A8:'not' Pj(a,z)=TRUE; then A9:Pj(a,z)=FALSE by MARGREL1:41; then Pj((a 'eqv' c) 'eqv' (b 'eqv' c),z) =((FALSE 'or' (Pj(c,z) '&' TRUE)) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' ((TRUE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' FALSE))) by A7,A8,MARGREL1:49 .=((FALSE 'or' Pj(c,z)) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' ((TRUE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' FALSE))) by MARGREL1:50 .=(Pj(c,z) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' ((TRUE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' FALSE))) by BINARITH:7 .=(Pj(c,z) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' ((TRUE 'or' Pj(c,z)) '&' Pj('not' c,z))) by BINARITH:7 .=(Pj(c,z) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' (TRUE '&' Pj('not' c,z))) by BINARITH:19 .=(Pj(c,z) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' Pj('not' c,z)) by MARGREL1:50 .=((Pj(c,z) 'or' (Pj(c,z) 'or' 'not' Pj(b,z))) '&' (Pj(c,z) 'or' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:23 .=(((Pj(c,z) 'or' Pj(c,z)) 'or' 'not' Pj(b,z)) '&' (Pj(c,z) 'or' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:20 .=((Pj(c,z) 'or' 'not' Pj(b,z)) '&' (Pj(c,z) 'or' (Pj('not' c,z) 'or' Pj(b,z)))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:21 .=((Pj(c,z) 'or' 'not' Pj(b,z)) '&' ((Pj(c,z) 'or' Pj('not' c,z)) 'or' Pj(b,z))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:20 .=((Pj(c,z) 'or' 'not' Pj(b,z)) '&' ((Pj(c,z) 'or' 'not' Pj(c,z)) 'or' Pj(b,z))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' Pj('not' c,z)) by VALUAT_1:def 5 .=((Pj(c,z) 'or' 'not' Pj(b,z)) '&' (TRUE 'or' Pj(b,z))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:18 .=(TRUE '&' (Pj(c,z) 'or' 'not' Pj(b,z))) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:19 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or' Pj('not' c,z)) by MARGREL1:50 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' ((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj('not' c,z) 'or' (Pj(c,z) '&' 'not' Pj(b,z)))) by BINARITH:20 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' ((Pj(b,z) '&' Pj('not' c,z)) 'or' ((Pj('not' c,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' 'not' Pj(b,z)))) by BINARITH:23 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' ((Pj(b,z) '&' Pj('not' c,z)) 'or' (('not' Pj(c,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' 'not' Pj(b,z)))) by VALUAT_1:def 5 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' ((Pj(b,z) '&' Pj('not' c,z)) 'or' (TRUE '&' (Pj('not' c,z) 'or' 'not' Pj(b,z)))) by BINARITH:18 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' ((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' (Pj(b,z) '&' Pj('not' c,z))) by MARGREL1:50 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' (((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' Pj(b,z)) '&' ((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' Pj('not' c,z))) by BINARITH:23 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' ((Pj('not' c,z) 'or' ('not' Pj(b,z) 'or' Pj(b,z))) '&' ((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' Pj('not' c,z))) by BINARITH:20 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' ((Pj('not' c,z) 'or' TRUE) '&' ((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' Pj('not' c,z))) by BINARITH:18 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' (TRUE '&' ((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' Pj('not' c,z))) by BINARITH:19 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' (('not' Pj(b,z) 'or' Pj('not' c,z)) 'or' Pj('not' c,z)) by MARGREL1:50 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' ('not' Pj(b,z) 'or' (Pj('not' c,z) 'or' Pj('not' c,z))) by BINARITH:20 .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj('not' c,z)) by BINARITH:21 .=('not' Pj(b,z) '&' (Pj(c,z) 'or' 'not' Pj(b,z))) 'or' ((Pj(c,z) 'or' 'not' Pj(b,z)) '&' Pj('not' c,z)) by BINARITH:22 .=(('not' Pj(b,z) '&' Pj(c,z)) 'or' ('not' Pj(b,z) '&' 'not' Pj(b,z))) 'or' (Pj('not' c,z) '&' (Pj(c,z) 'or' 'not' Pj(b,z))) by BINARITH:22 .=(('not' Pj(b,z) '&' Pj(c,z)) 'or' 'not' Pj(b,z)) 'or' (Pj('not' c,z) '&' (Pj(c,z) 'or' 'not' Pj(b,z))) by BINARITH:16 .=(('not' Pj(b,z) '&' Pj(c,z)) 'or' 'not' Pj(b,z)) 'or' (Pj('not' c,z) '&' Pj(c,z) 'or' Pj('not' c,z) '&' 'not' Pj(b,z)) by BINARITH:22 .=(('not' Pj(b,z) '&' Pj(c,z)) 'or' 'not' Pj(b,z)) 'or' ((Pj(c,z) '&' 'not' Pj(c,z)) 'or' (Pj('not' c,z) '&' 'not' Pj(b,z))) by VALUAT_1:def 5 .=(('not' Pj(b,z) '&' Pj(c,z)) 'or' 'not' Pj(b,z)) 'or' (FALSE 'or' (Pj('not' c,z) '&' 'not' Pj(b,z))) by MARGREL1:46 .=('not' Pj(b,z) 'or' ('not' Pj(b,z) '&' Pj(c,z))) 'or' (Pj('not' c,z) '&' 'not' Pj(b,z)) by BINARITH:7 .='not' Pj(b,z) 'or' (('not' Pj(b,z) '&' Pj(c,z)) 'or' (Pj('not' c,z) '&' 'not' Pj(b,z))) by BINARITH:20 .=TRUE by A6,A9,BINARITH:19,MARGREL1:43; hence thesis; case A10:Pj(b,z)=TRUE; then 'not' Pj(b,z)=FALSE by MARGREL1:41; then Pj((a 'eqv' c) 'eqv' (b 'eqv' c),z) =((Pj('not' c,z) 'or' (Pj(c,z) '&' FALSE)) 'or' ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) '&' (((TRUE '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' FALSE)) 'or' ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) by A6,A7,A10,MARGREL1:43,50 .=((Pj('not' c,z) 'or' (FALSE '&' Pj(c,z))) 'or' ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) '&' ((Pj('not' c,z) 'or' (Pj(c,z) '&' FALSE)) 'or' ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) by MARGREL1:50 .=((Pj('not' c,z) 'or' FALSE) 'or' ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) '&' ((Pj('not' c,z) 'or' (FALSE '&' Pj(c,z))) 'or' ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) by MARGREL1:49 .=((Pj('not' c,z) 'or' FALSE) 'or' ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) '&' ((Pj('not' c,z) 'or' FALSE) 'or' ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) by MARGREL1:49 .=((Pj('not' c,z) 'or' FALSE) 'or' ((FALSE 'or' Pj(c,z)) '&' TRUE)) '&' ((Pj('not' c,z) 'or' FALSE) 'or' ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) by BINARITH:19 .=((Pj('not' c,z) 'or' FALSE) 'or' ((FALSE 'or' Pj(c,z)) '&' TRUE)) '&' ((Pj('not' c,z) 'or' FALSE) 'or' ((FALSE 'or' Pj(c,z)) '&' TRUE)) by BINARITH:19 .=((Pj('not' c,z) 'or' FALSE) 'or' (Pj(c,z) '&' TRUE)) '&' ((Pj('not' c,z) 'or' FALSE) 'or' ((FALSE 'or' Pj(c,z)) '&' TRUE)) by BINARITH:7 .=((Pj('not' c,z) 'or' FALSE) 'or' (Pj(c,z) '&' TRUE)) '&' ((Pj('not' c,z) 'or' FALSE) 'or' (Pj(c,z) '&' TRUE)) by BINARITH:7 .=(Pj('not' c,z) 'or' (Pj(c,z) '&' TRUE)) '&' ((Pj('not' c,z) 'or' FALSE) 'or' (Pj(c,z) '&' TRUE)) by BINARITH:7 .=(Pj('not' c,z) 'or' (TRUE '&' Pj(c,z))) '&' (Pj('not' c,z) 'or' (Pj(c,z) '&' TRUE)) by BINARITH:7 .=(Pj('not' c,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' (TRUE '&' Pj(c,z))) by MARGREL1:50 .=(Pj('not' c,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(c,z)) by MARGREL1:50 .=('not' Pj(c,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(c,z)) by VALUAT_1:def 5 .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ('not' Pj(c,z) 'or' Pj(c,z)) by VALUAT_1:def 5 .=TRUE '&' ('not' Pj(c,z) 'or' Pj(c,z)) by BINARITH:18 .=TRUE '&' TRUE by BINARITH:18 .=TRUE by MARGREL1:45; hence thesis; end; hence thesis; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a 'eqv' b) '<' (a 'imp' c) 'eqv' (b 'imp' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); let z be Element of Y; assume A1:Pj(a 'eqv' b,z)=TRUE; Pj(a 'eqv' b,z) =Pj((a 'imp' b) '&' (b 'imp' a),z) by BVFUNC_4:7 .=Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z) by VALUAT_1:def 6; then A2:Pj(a 'imp' b,z)=TRUE & Pj(b 'imp' a,z)=TRUE by A1,MARGREL1:45; then A3:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11; A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39; A5: Pj(b 'imp' a,z) = 'not' Pj(b,z) 'or' Pj(a,z) by BVFUNC_1:def 11; A6:'not' Pj(b,z) 'or' Pj(a,z) = TRUE by A2,BVFUNC_1:def 11; Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39; then A7:'not' Pj(b,z)=TRUE or Pj(a,z)=TRUE by A2,A5,BINARITH:7; A8:Pj((a 'imp' c) 'eqv' (b 'imp' c),z) =Pj(((a 'imp' c) 'imp' (b 'imp' c)) '&' ((b 'imp' c) 'imp' (a 'imp' c)),z) by BVFUNC_4:7 .=Pj((a 'imp' c) 'imp' (b 'imp' c),z) '&' Pj((b 'imp' c) 'imp' (a 'imp' c),z) by VALUAT_1:def 6 .=('not' Pj(a 'imp' c,z) 'or' Pj(b 'imp' c,z)) '&' Pj((b 'imp' c) 'imp' (a 'imp' c),z) by BVFUNC_1:def 11 .=('not' Pj(a 'imp' c,z) 'or' Pj(b 'imp' c,z)) '&' ('not' Pj(b 'imp' c,z) 'or' Pj(a 'imp' c,z)) by BVFUNC_1:def 11 .=('not'( 'not' Pj(a,z) 'or' Pj(c,z)) 'or' Pj(b 'imp' c,z)) '&' ('not' Pj(b 'imp' c,z) 'or' Pj(a 'imp' c,z)) by BVFUNC_1:def 11 .=('not'( 'not' Pj(a,z) 'or' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&' ('not' Pj(b 'imp' c,z) 'or' Pj(a 'imp' c,z)) by BVFUNC_1:def 11 .=('not'( 'not' Pj(a,z) 'or' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&' ('not'( 'not' Pj(b,z) 'or' Pj(c,z)) 'or' Pj(a 'imp' c,z)) by BVFUNC_1:def 11 .=('not'( 'not' Pj(a,z) 'or' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&' ('not'( 'not' Pj(b,z) 'or' Pj(c,z)) 'or' ('not' Pj(a,z) 'or' Pj(c,z))) by BVFUNC_1:def 11 .=(('not' 'not' Pj(a,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&' ('not'( 'not' Pj(b,z) 'or' Pj(c,z)) 'or' ('not' Pj(a,z) 'or' Pj(c,z))) by BINARITH:10 .=(('not' 'not' Pj(a,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&' (('not' 'not' Pj(b,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(a,z) 'or' Pj(c,z))) by BINARITH:10 .=((Pj(a,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&' (('not' 'not' Pj(b,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(a,z) 'or' Pj(c,z))) by MARGREL1:40 .=((Pj(a,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&' ((Pj(b,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(a,z) 'or' Pj(c,z))) by MARGREL1:40; now per cases by A3,A4,BINARITH:7; case A9:'not' Pj(a,z)=TRUE; then A10:Pj(a,z)=FALSE by MARGREL1:41; then 'not' Pj(b,z)=TRUE by A6,BINARITH:7; then Pj(b,z)=FALSE by MARGREL1:41; then Pj((a 'imp' c) 'eqv' (b 'imp' c),z) =(FALSE 'or' (TRUE 'or' Pj(c,z))) '&' ((FALSE '&' 'not' Pj(c,z)) 'or' (TRUE 'or' Pj(c,z))) by A8,A9,A10,MARGREL1:49 .=(FALSE 'or' (TRUE 'or' Pj(c,z))) '&' (FALSE 'or' (TRUE 'or' Pj(c,z))) by MARGREL1:49 .=(TRUE 'or' Pj(c,z)) '&' (FALSE 'or' (TRUE 'or' Pj(c,z))) by BINARITH:7 .=(TRUE 'or' Pj(c,z)) '&' (TRUE 'or' Pj(c,z)) by BINARITH:7 .=TRUE '&' (TRUE 'or' Pj(c,z)) by BINARITH:19 .=TRUE '&' TRUE by BINARITH:19 .=TRUE by MARGREL1:45; hence thesis; case A11:Pj(b,z)=TRUE; then 'not' Pj(b,z)=FALSE by MARGREL1:41; then Pj((a 'imp' c) 'eqv' (b 'imp' c),z) =('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) '&' ((TRUE '&' 'not' Pj(c,z)) 'or' (FALSE 'or' Pj(c,z))) by A7,A8,A11,MARGREL1:43,50 .=('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) '&' ('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) by MARGREL1:50 .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) by BINARITH:7 .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ('not' Pj(c,z) 'or' Pj(c,z)) by BINARITH:7 .=TRUE '&' ('not' Pj(c,z) 'or' Pj(c,z)) by BINARITH:18 .=TRUE '&' TRUE by BINARITH:18 .=TRUE by MARGREL1:45; hence thesis; end; hence thesis; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a 'eqv' b) '<' (c 'imp' a) 'eqv' (c 'imp' b) proof let a,b,c be Element of Funcs(Y,BOOLEAN); let z be Element of Y; assume A1:Pj(a 'eqv' b,z)=TRUE; Pj(a 'eqv' b,z) =Pj((a 'imp' b) '&' (b 'imp' a),z) by BVFUNC_4:7 .=Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z) by VALUAT_1:def 6; then A2:Pj(a 'imp' b,z)=TRUE & Pj(b 'imp' a,z)=TRUE by A1,MARGREL1:45; then A3:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11; A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39; A5: Pj(b 'imp' a,z) = 'not' Pj(b,z) 'or' Pj(a,z) by BVFUNC_1:def 11; A6:'not' Pj(b,z) 'or' Pj(a,z) = TRUE by A2,BVFUNC_1:def 11; Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39; then A7:'not' Pj(b,z)=TRUE or Pj(a,z)=TRUE by A2,A5,BINARITH:7; A8:Pj((c 'imp' a) 'eqv' (c 'imp' b),z) =Pj(((c 'imp' a) 'imp' (c 'imp' b)) '&' ((c 'imp' b) 'imp' (c 'imp' a)),z) by BVFUNC_4:7 .=Pj((c 'imp' a) 'imp' (c 'imp' b),z) '&' Pj((c 'imp' b) 'imp' (c 'imp' a),z) by VALUAT_1:def 6 .=('not' Pj(c 'imp' a,z) 'or' Pj(c 'imp' b,z)) '&' Pj((c 'imp' b) 'imp' (c 'imp' a),z) by BVFUNC_1:def 11 .=('not' Pj(c 'imp' a,z) 'or' Pj(c 'imp' b,z)) '&' ('not' Pj(c 'imp' b,z) 'or' Pj(c 'imp' a,z)) by BVFUNC_1:def 11 .=('not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' Pj(c 'imp' b,z)) '&' ('not' Pj(c 'imp' b,z) 'or' Pj(c 'imp' a,z)) by BVFUNC_1:def 11 .=('not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&' ('not' Pj(c 'imp' b,z) 'or' Pj(c 'imp' a,z)) by BVFUNC_1:def 11 .=('not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&' ('not'( 'not' Pj(c,z) 'or' Pj(b,z)) 'or' Pj(c 'imp' a,z)) by BVFUNC_1:def 11 .=('not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&' ('not'( 'not' Pj(c,z) 'or' Pj(b,z)) 'or' ('not' Pj(c,z) 'or' Pj(a,z))) by BVFUNC_1:def 11 .=(('not' 'not' Pj(c,z) '&' 'not' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&' ('not'( 'not' Pj(c,z) 'or' Pj(b,z)) 'or' ('not' Pj(c,z) 'or' Pj(a,z))) by BINARITH:10 .=(('not' 'not' Pj(c,z) '&' 'not' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&' (('not' 'not' Pj(c,z) '&' 'not' Pj(b,z)) 'or' ('not' Pj(c,z) 'or' Pj(a,z))) by BINARITH:10 .=((Pj(c,z) '&' 'not' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&' (('not' 'not' Pj(c,z) '&' 'not' Pj(b,z)) 'or' ('not' Pj(c,z) 'or' Pj(a,z))) by MARGREL1:40 .=((Pj(c,z) '&' 'not' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&' ((Pj(c,z) '&' 'not' Pj(b,z)) 'or' ('not' Pj(c,z) 'or' Pj(a,z))) by MARGREL1:40; now per cases by A3,A4,BINARITH:7; case A9:'not' Pj(a,z)=TRUE; then A10:Pj(a,z)=FALSE by MARGREL1:41; then 'not' Pj(b,z)=TRUE by A6,BINARITH:7; then Pj(b,z)=FALSE by MARGREL1:41; then Pj((c 'imp' a) 'eqv' (c 'imp' b),z) =(Pj(c,z) 'or' ('not' Pj(c,z) 'or' FALSE)) '&' ((TRUE '&' Pj(c,z)) 'or' ('not' Pj(c,z) 'or' FALSE)) by A8,A9,A10,MARGREL1:50 .=(Pj(c,z) 'or' ('not' Pj(c,z) 'or' FALSE)) '&' (Pj(c,z) 'or' ('not' Pj(c,z) 'or' FALSE)) by MARGREL1:50 .=(Pj(c,z) 'or' 'not' Pj(c,z)) '&' (Pj(c,z) 'or' ('not' Pj(c,z) 'or' FALSE)) by BINARITH:7 .=(Pj(c,z) 'or' 'not' Pj(c,z)) '&' (Pj(c,z) 'or' 'not' Pj(c,z)) by BINARITH:7 .=TRUE '&' (Pj(c,z) 'or' 'not' Pj(c,z)) by BINARITH:18 .=TRUE '&' TRUE by BINARITH:18 .=TRUE by MARGREL1:45; hence thesis; case A11:Pj(b,z)=TRUE; then 'not' Pj(b,z)=FALSE by MARGREL1:41; then Pj((c 'imp' a) 'eqv' (c 'imp' b),z) =(FALSE 'or' ('not' Pj(c,z) 'or' TRUE)) '&' ((FALSE '&' Pj(c,z)) 'or' ('not' Pj(c,z) 'or' TRUE)) by A7,A8,A11,MARGREL1:43,49 .=(FALSE 'or' ('not' Pj(c,z) 'or' TRUE)) '&' (FALSE 'or' ('not' Pj(c,z) 'or' TRUE)) by MARGREL1:49 .=('not' Pj(c,z) 'or' TRUE) '&' (FALSE 'or' ('not' Pj(c,z) 'or' TRUE)) by BINARITH:7 .=('not' Pj(c,z) 'or' TRUE) '&' ('not' Pj(c,z) 'or' TRUE) by BINARITH:7 .=TRUE '&' ('not' Pj(c,z) 'or' TRUE) by BINARITH:19 .=TRUE '&' TRUE by BINARITH:19 .=TRUE by MARGREL1:45; hence thesis; end; hence thesis; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a 'eqv' b) '<' (a '&' c) 'eqv' (b '&' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); let z be Element of Y; assume A1:Pj(a 'eqv' b,z)=TRUE; Pj(a 'eqv' b,z) =Pj((a 'imp' b) '&' (b 'imp' a),z) by BVFUNC_4:7 .=Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z) by VALUAT_1:def 6; then A2:Pj(a 'imp' b,z)=TRUE & Pj(b 'imp' a,z)=TRUE by A1,MARGREL1:45; then A3:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11; A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39; A5: Pj(b 'imp' a,z) = 'not' Pj(b,z) 'or' Pj(a,z) by BVFUNC_1:def 11; A6:'not' Pj(b,z) 'or' Pj(a,z) = TRUE by A2,BVFUNC_1:def 11; Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39; then A7:'not' Pj(b,z)=TRUE or Pj(a,z)=TRUE by A2,A5,BINARITH:7; A8:Pj((a '&' c) 'eqv' (b '&' c),z) =Pj(((a '&' c) 'imp' (b '&' c)) '&' ((b '&' c) 'imp' (a '&' c)),z) by BVFUNC_4:7 .=Pj((a '&' c) 'imp' (b '&' c),z) '&' Pj((b '&' c) 'imp' (a '&' c),z) by VALUAT_1:def 6 .=('not' Pj(a '&' c,z) 'or' Pj(b '&' c,z)) '&' Pj((b '&' c) 'imp' (a '&' c),z) by BVFUNC_1:def 11 .=('not' Pj(a '&' c,z) 'or' Pj(b '&' c,z)) '&' ('not' Pj(b '&' c,z) 'or' Pj(a '&' c,z)) by BVFUNC_1:def 11 .=('not'( Pj(a,z) '&' Pj(c,z)) 'or' Pj(b '&' c,z)) '&' ('not' Pj(b '&' c,z) 'or' Pj(a '&' c,z)) by VALUAT_1:def 6 .=('not'( Pj(a,z) '&' Pj(c,z)) 'or' (Pj(b,z) '&' Pj(c,z))) '&' ('not' Pj(b '&' c,z) 'or' Pj(a '&' c,z)) by VALUAT_1:def 6 .=('not'( Pj(a,z) '&' Pj(c,z)) 'or' (Pj(b,z) '&' Pj(c,z))) '&' ('not'( Pj(b,z) '&' Pj(c,z)) 'or' Pj(a '&' c,z)) by VALUAT_1:def 6 .=('not'( Pj(a,z) '&' Pj(c,z)) 'or' (Pj(b,z) '&' Pj(c,z))) '&' ('not'( Pj(b,z) '&' Pj(c,z)) 'or' (Pj(a,z) '&' Pj(c,z))) by VALUAT_1:def 6 .=(('not' Pj(a,z) 'or' 'not' Pj(c,z)) 'or' (Pj(b,z) '&' Pj(c,z))) '&' ('not'( Pj(b,z) '&' Pj(c,z)) 'or' (Pj(a,z) '&' Pj(c,z))) by BINARITH:9 .=(('not' Pj(a,z) 'or' 'not' Pj(c,z)) 'or' (Pj(b,z) '&' Pj(c,z))) '&' (('not' Pj(b,z) 'or' 'not' Pj(c,z)) 'or' (Pj(a,z) '&' Pj(c,z))) by BINARITH:9; now per cases by A3,A4,BINARITH:7; case A9:'not' Pj(a,z)=TRUE; then A10:Pj(a,z)=FALSE by MARGREL1:41; then 'not' Pj(b,z)=TRUE by A6,BINARITH:7; then Pj(b,z)=FALSE by MARGREL1:41; then Pj((a '&' c) 'eqv' (b '&' c),z) =((TRUE 'or' 'not' Pj(c,z)) 'or' FALSE) '&' ((TRUE 'or' 'not' Pj(c,z)) 'or' (FALSE '&' Pj(c,z))) by A8,A9,A10,MARGREL1:49 .=((TRUE 'or' 'not' Pj(c,z)) 'or' FALSE) '&' ((TRUE 'or' 'not' Pj(c,z)) 'or' FALSE) by MARGREL1:49 .=(TRUE 'or' 'not' Pj(c,z)) '&' ((TRUE 'or' 'not' Pj(c,z)) 'or' FALSE) by BINARITH:7 .=(TRUE 'or' 'not' Pj(c,z)) '&' (TRUE 'or' 'not' Pj(c,z)) by BINARITH:7 .=TRUE '&' (TRUE 'or' 'not' Pj(c,z)) by BINARITH:19 .=TRUE '&' TRUE by BINARITH:19 .=TRUE by MARGREL1:45; hence thesis; case A11:Pj(b,z)=TRUE; then 'not' Pj(b,z)=FALSE by MARGREL1:41; then Pj((a '&' c) 'eqv' (b '&' c),z) =((FALSE 'or' 'not' Pj(c,z)) 'or' Pj(c,z)) '&' ((FALSE 'or' 'not' Pj(c,z)) 'or' (TRUE '&' Pj(c,z))) by A7,A8,A11,MARGREL1:43,50 .=((FALSE 'or' 'not' Pj(c,z)) 'or' Pj(c,z)) '&' ((FALSE 'or' 'not' Pj(c,z)) 'or' Pj(c,z)) by MARGREL1:50 .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ((FALSE 'or' 'not' Pj(c,z)) 'or' Pj(c,z)) by BINARITH:7 .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ('not' Pj(c,z) 'or' Pj(c,z)) by BINARITH:7 .=TRUE '&' ('not' Pj(c,z) 'or' Pj(c,z)) by BINARITH:18 .=TRUE '&' TRUE by BINARITH:18 .=TRUE by MARGREL1:45; hence thesis; end; hence thesis; end; theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds (a 'eqv' b) '<' (a 'or' c) 'eqv' (b 'or' c) proof let a,b,c be Element of Funcs(Y,BOOLEAN); let z be Element of Y; assume A1:Pj(a 'eqv' b,z)=TRUE; Pj(a 'eqv' b,z) =Pj((a 'imp' b) '&' (b 'imp' a),z) by BVFUNC_4:7 .=Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z) by VALUAT_1:def 6; then A2:Pj(a 'imp' b,z)=TRUE & Pj(b 'imp' a,z)=TRUE by A1,MARGREL1:45; then A3:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11; A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39; A5: Pj(b 'imp' a,z) = 'not' Pj(b,z) 'or' Pj(a,z) by BVFUNC_1:def 11; A6:'not' Pj(b,z) 'or' Pj(a,z) = TRUE by A2,BVFUNC_1:def 11; Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39; then A7:'not' Pj(b,z)=TRUE or Pj(a,z)=TRUE by A2,A5,BINARITH:7; A8:Pj((a 'or' c) 'eqv' (b 'or' c),z) =Pj(((a 'or' c) 'imp' (b 'or' c)) '&' ((b 'or' c) 'imp' (a 'or' c)),z) by BVFUNC_4:7 .=Pj((a 'or' c) 'imp' (b 'or' c),z) '&' Pj((b 'or' c) 'imp' (a 'or' c),z) by VALUAT_1:def 6 .=('not' Pj(a 'or' c,z) 'or' Pj(b 'or' c,z)) '&' Pj((b 'or' c) 'imp' (a 'or' c),z) by BVFUNC_1:def 11 .=('not' Pj(a 'or' c,z) 'or' Pj(b 'or' c,z)) '&' ('not' Pj(b 'or' c,z) 'or' Pj(a 'or' c,z)) by BVFUNC_1:def 11 .=('not'( Pj(a,z) 'or' Pj(c,z)) 'or' Pj(b 'or' c,z)) '&' ('not' Pj(b 'or' c,z) 'or' Pj(a 'or' c,z)) by BVFUNC_1:def 7 .=('not'( Pj(a,z) 'or' Pj(c,z)) 'or' (Pj(b,z) 'or' Pj(c,z))) '&' ('not' Pj(b 'or' c,z) 'or' Pj(a 'or' c,z)) by BVFUNC_1:def 7 .=('not'( Pj(a,z) 'or' Pj(c,z)) 'or' (Pj(b,z) 'or' Pj(c,z))) '&' ('not'( Pj(b,z) 'or' Pj(c,z)) 'or' Pj(a 'or' c,z)) by BVFUNC_1:def 7 .=('not'( Pj(a,z) 'or' Pj(c,z)) 'or' (Pj(b,z) 'or' Pj(c,z))) '&' ('not'( Pj(b,z) 'or' Pj(c,z)) 'or' (Pj(a,z) 'or' Pj(c,z))) by BVFUNC_1:def 7 .=(('not' Pj(a,z) '&' 'not' Pj(c,z)) 'or' (Pj(b,z) 'or' Pj(c,z))) '&' ('not'( Pj(b,z) 'or' Pj(c,z)) 'or' (Pj(a,z) 'or' Pj(c,z))) by BINARITH:10 .=(('not' Pj(a,z) '&' 'not' Pj(c,z)) 'or' (Pj(b,z) 'or' Pj(c,z))) '&' (('not' Pj(b,z) '&' 'not' Pj(c,z)) 'or' (Pj(a,z) 'or' Pj(c,z))) by BINARITH:10; now per cases by A3,A4,BINARITH:7; case A9:'not' Pj(a,z)=TRUE; then A10:Pj(a,z)=FALSE by MARGREL1:41; then 'not' Pj(b,z)=TRUE by A6,BINARITH:7; then Pj(b,z)=FALSE by MARGREL1:41; then Pj((a 'or' c) 'eqv' (b 'or' c),z) =('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) '&' ((TRUE '&' 'not' Pj(c,z)) 'or' (FALSE 'or' Pj(c,z))) by A8,A9,A10,MARGREL1:50 .=('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) '&' ('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) by MARGREL1:50 .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) by BINARITH:7 .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ('not' Pj(c,z) 'or' Pj(c,z)) by BINARITH:7 .=TRUE '&' ('not' Pj(c,z) 'or' Pj(c,z)) by BINARITH:18 .=TRUE '&' TRUE by BINARITH:18 .=TRUE by MARGREL1:45; hence thesis; case A11:Pj(b,z)=TRUE; then 'not' Pj(b,z)=FALSE by MARGREL1:41; then Pj((a 'or' c) 'eqv' (b 'or' c),z) =(FALSE 'or' (TRUE 'or' Pj(c,z))) '&' ((FALSE '&' 'not' Pj(c,z)) 'or' (TRUE 'or' Pj(c,z))) by A7,A8,A11,MARGREL1:43,49 .=(FALSE 'or' (TRUE 'or' Pj(c,z))) '&' (FALSE 'or' (TRUE 'or' Pj(c,z))) by MARGREL1:49 .=(TRUE 'or' Pj(c,z)) '&' (FALSE 'or' (TRUE 'or' Pj(c,z))) by BINARITH:7 .=(TRUE 'or' Pj(c,z)) '&' (TRUE 'or' Pj(c,z)) by BINARITH:7 .=TRUE '&' (TRUE 'or' Pj(c,z)) by BINARITH:19 .=TRUE '&' TRUE by BINARITH:19 .=TRUE by MARGREL1:45; hence thesis; end; hence thesis; end; theorem for a,b being Element of Funcs(Y,BOOLEAN) holds a '<' (a 'eqv' b) 'eqv' (b 'eqv' a) 'eqv' a proof let a,b be Element of Funcs(Y,BOOLEAN); let z be Element of Y; assume A1:Pj(a,z)=TRUE; then A2:'not' Pj(a,z)=FALSE by MARGREL1:41; A3:Pj('not' a,z)='not' Pj(a,z) by VALUAT_1:def 5; A4:Pj((a 'eqv' b) 'eqv' (b 'eqv' a),z) =Pj(((a 'eqv' b) 'imp' (b 'eqv' a)) '&' ((b 'eqv' a) 'imp' (a 'eqv' b)),z) by BVFUNC_4:7 .=Pj((a 'eqv' b) 'imp' (b 'eqv' a),z) '&' Pj((b 'eqv' a) 'imp' (a 'eqv' b),z) by VALUAT_1:def 6 .=Pj('not'( a 'eqv' b) 'or' (b 'eqv' a),z) '&' Pj((b 'eqv' a) 'imp' (a 'eqv' b),z) by BVFUNC_4:8 .=Pj('not'( a 'eqv' b) 'or' (b 'eqv' a),z) '&' Pj('not'( b 'eqv' a) 'or' (a 'eqv' b),z) by BVFUNC_4:8 .=(Pj('not'( a 'eqv' b),z) 'or' Pj(b 'eqv' a,z)) '&' Pj('not'( b 'eqv' a) 'or' (a 'eqv' b),z) by BVFUNC_1:def 7 .=(Pj('not'( a 'eqv' b),z) 'or' Pj(b 'eqv' a,z)) '&' (Pj('not'( b 'eqv' a),z) 'or' Pj(a 'eqv' b,z)) by BVFUNC_1:def 7 .=(Pj('not'( (a 'imp' b) '&' (b 'imp' a)),z) 'or' Pj(b 'eqv' a,z)) '&' (Pj('not'( b 'eqv' a),z) 'or' Pj(a 'eqv' b,z)) by BVFUNC_4:7 .=(Pj('not'( (a 'imp' b) '&' (b 'imp' a)),z) 'or' Pj(b 'eqv' a,z)) '&' (Pj('not'( b 'eqv' a),z) 'or' Pj((a 'imp' b) '&' (b 'imp' a),z)) by BVFUNC_4:7 .=(Pj('not'( (a 'imp' b) '&' (b 'imp' a)),z) 'or' Pj((b 'imp' a) '&' (a 'imp' b),z)) '&' (Pj('not'( b 'eqv' a),z) 'or' Pj((a 'imp' b) '&' (b 'imp' a),z)) by BVFUNC_4:7 .=(Pj('not'( (a 'imp' b) '&' (b 'imp' a)),z) 'or' Pj((b 'imp' a) '&' (a 'imp' b),z)) '&' (Pj('not'( (b 'imp' a) '&' (a 'imp' b)),z) 'or' Pj((a 'imp' b) '&' (b 'imp' a),z)) by BVFUNC_4:7 .=('not' Pj((a 'imp' b) '&' (b 'imp' a),z) 'or' Pj((b 'imp' a) '&' (a 'imp' b),z)) '&' (Pj('not'( (b 'imp' a) '&' (a 'imp' b)),z) 'or' Pj((a 'imp' b) '&' (b 'imp' a),z)) by VALUAT_1:def 5 .=('not' Pj((a 'imp' b) '&' (b 'imp' a),z) 'or' Pj((b 'imp' a) '&' (a 'imp' b),z)) '&' ('not' Pj((b 'imp' a) '&' (a 'imp' b),z) 'or' Pj((a 'imp' b) '&' (b 'imp' a),z)) by VALUAT_1:def 5 .=('not'( Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)) 'or' Pj((b 'imp' a) '&' (a 'imp' b),z)) '&' ('not' Pj((b 'imp' a) '&' (a 'imp' b),z) 'or' Pj((a 'imp' b) '&' (b 'imp' a),z)) by VALUAT_1:def 6 .=('not'( Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)) 'or' (Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z))) '&' ('not' Pj((b 'imp' a) '&' (a 'imp' b),z) 'or' Pj((a 'imp' b) '&' (b 'imp' a),z)) by VALUAT_1:def 6 .=('not'( Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)) 'or' (Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z))) '&' ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or' Pj((a 'imp' b) '&' (b 'imp' a),z)) by VALUAT_1:def 6 .=('not'( Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)) 'or' (Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z))) '&' ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or' (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z))) by VALUAT_1:def 6 .=('not'( Pj('not' a 'or' b,z) '&' Pj(b 'imp' a,z)) 'or' (Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z))) '&' ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or' (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z))) by BVFUNC_4:8 .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or' (Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z))) '&' ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or' (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z))) by BVFUNC_4:8 .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or' (Pj('not' b 'or' a,z) '&' Pj(a 'imp' b,z))) '&' ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or' (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z))) by BVFUNC_4:8 .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or' (Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z))) '&' ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or' (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z))) by BVFUNC_4:8 .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or' (Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z))) '&' ('not'( Pj('not' b 'or' a,z) '&' Pj(a 'imp' b,z)) 'or' (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z))) by BVFUNC_4:8 .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or' (Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z))) '&' ('not'( Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z)) 'or' (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z))) by BVFUNC_4:8 .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or' (Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z))) '&' ('not'( Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z)) 'or' (Pj('not' a 'or' b,z) '&' Pj(b 'imp' a,z))) by BVFUNC_4:8 .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or' (Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z))) '&' ('not'( Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z)) 'or' (Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z))) by BVFUNC_4:8 .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b 'or' a,z))) 'or' ((Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z)))) '&' ('not'( (Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z))) 'or' ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z)))) by BVFUNC_1:def 7 .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or' ((Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z)))) '&' ('not'( (Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z))) 'or' ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z)))) by BVFUNC_1:def 7 .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or' ((Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a 'or' b,z)))) '&' ('not'( (Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z))) 'or' ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z)))) by BVFUNC_1:def 7 .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or' ((Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z)))) '&' ('not'( (Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z))) 'or' ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z)))) by BVFUNC_1:def 7 .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or' ((Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z)))) '&' ('not'( (Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a 'or' b,z))) 'or' ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z)))) by BVFUNC_1:def 7 .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or' ((Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z)))) '&' ('not'( (Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z))) 'or' ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z)))) by BVFUNC_1:def 7 .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or' ((Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z)))) '&' ('not'( (Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z))) 'or' ((Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b 'or' a,z)))) by BVFUNC_1:def 7 .=('not'( (FALSE 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' TRUE)) 'or' ((Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z)))) '&' ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or' ((FALSE 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' TRUE))) by A1,A2,A3,BVFUNC_1:def 7 .=('not'( Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE)) 'or' ((Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z)))) '&' ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or' ((FALSE 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' TRUE))) by BINARITH:7 .=('not'( Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE)) 'or' ((Pj('not' b,z) 'or' TRUE) '&' Pj(b,z))) '&' ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or' ((FALSE 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' TRUE))) by BINARITH:7 .=('not'( Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE)) 'or' ((Pj('not' b,z) 'or' TRUE) '&' Pj(b,z))) '&' ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or' (Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE))) by BINARITH:7 .=('not'( Pj(b,z) '&' TRUE) 'or' ((Pj('not' b,z) 'or' TRUE) '&' Pj(b,z))) '&' ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or' (Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE))) by BINARITH:19 .=('not'( Pj(b,z) '&' TRUE) 'or' (TRUE '&' Pj(b,z))) '&' ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or' (Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE))) by BINARITH:19 .=('not'( Pj(b,z) '&' TRUE) 'or' (TRUE '&' Pj(b,z))) '&' ('not'( TRUE '&' (FALSE 'or' Pj(b,z))) 'or' (Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE))) by BINARITH:19 .=('not'( Pj(b,z) '&' TRUE) 'or' (TRUE '&' Pj(b,z))) '&' ('not'( TRUE '&' (FALSE 'or' Pj(b,z))) 'or' (Pj(b,z) '&' TRUE)) by BINARITH:19 .=('not'( TRUE '&' Pj(b,z)) 'or' (TRUE '&' Pj(b,z))) '&' ('not'( TRUE '&' Pj(b,z)) 'or' (Pj(b,z) '&' TRUE)) by BINARITH:7 .=('not' Pj(b,z) 'or' (TRUE '&' Pj(b,z))) '&' ('not'( TRUE '&' Pj(b,z)) 'or' (TRUE '&' Pj(b,z))) by MARGREL1:50 .=('not' Pj(b,z) 'or' (TRUE '&' Pj(b,z))) '&' ('not' Pj(b,z) 'or' (TRUE '&' Pj(b,z))) by MARGREL1:50 .=('not' Pj(b,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' (TRUE '&' Pj(b,z))) by MARGREL1:50 .=('not' Pj(b,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(b,z)) by MARGREL1:50 .=TRUE '&' ('not' Pj(b,z) 'or' Pj(b,z)) by BINARITH:18 .=TRUE '&' TRUE by BINARITH:18 .=TRUE by MARGREL1:45; Pj((a 'eqv' b) 'eqv' (b 'eqv' a) 'eqv' a,z) =Pj((((a 'eqv' b) 'eqv' (b 'eqv' a)) 'imp' a) '&' (a 'imp' ((a 'eqv' b) 'eqv' (b 'eqv' a))),z) by BVFUNC_4:7 .=Pj(((a 'eqv' b) 'eqv' (b 'eqv' a)) 'imp' a,z) '&' Pj(a 'imp' ((a 'eqv' b) 'eqv' (b 'eqv' a)),z) by VALUAT_1:def 6 .=('not' Pj((a 'eqv' b) 'eqv' (b 'eqv' a),z) 'or' Pj(a,z)) '&' Pj(a 'imp' ((a 'eqv' b) 'eqv' (b 'eqv' a)),z) by BVFUNC_1:def 11 .=('not' Pj((a 'eqv' b) 'eqv' (b 'eqv' a),z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' Pj((a 'eqv' b) 'eqv' (b 'eqv' a),z)) by BVFUNC_1:def 11 .=(FALSE 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' TRUE) by A4,MARGREL1:41 .=Pj(a,z) '&' ('not' Pj(a,z) 'or' TRUE) by BINARITH:7 .=TRUE '&' Pj(a,z) by BINARITH:19 .=TRUE by A1,MARGREL1:50; hence thesis; end; theorem for a,b being Element of Funcs(Y,BOOLEAN) holds a '<' (a 'imp' b) 'eqv' b proof let a,b be Element of Funcs(Y,BOOLEAN); let z be Element of Y; assume A1:Pj(a,z)=TRUE; then A2:'not' Pj(a,z)=FALSE by MARGREL1:41; Pj((a 'imp' b) 'eqv' b,z) =Pj(('not' a 'or' b) 'eqv' b,z) by BVFUNC_4:8 .=Pj((('not' a 'or' b) 'imp' b) '&' (b 'imp' ('not' a 'or' b)),z) by BVFUNC_4:7 .=Pj(('not'( 'not' a 'or' b) 'or' b) '&' (b 'imp' ('not' a 'or' b)),z) by BVFUNC_4:8 .=Pj(('not'( 'not' a 'or' b) 'or' b) '&' ('not' b 'or' ('not' a 'or' b)),z) by BVFUNC_4:8 .=Pj('not'( 'not' a 'or' b) 'or' b,z) '&' Pj('not' b 'or' ('not' a 'or' b),z) by VALUAT_1:def 6 .=(Pj('not'( 'not' a 'or' b),z) 'or' Pj(b,z)) '&' Pj('not' b 'or' ('not' a 'or' b),z) by BVFUNC_1:def 7 .=('not' Pj('not' a 'or' b,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' ('not' a 'or' b),z) by VALUAT_1:def 5 .=('not'( Pj('not' a,z) 'or' Pj(b,z)) 'or' Pj(b,z)) '&' Pj('not' b 'or' ('not' a 'or' b),z) by BVFUNC_1:def 7 .=('not'( 'not' Pj(a,z) 'or' Pj(b,z)) 'or' Pj(b,z)) '&' Pj('not' b 'or' ('not' a 'or' b),z) by VALUAT_1:def 5 .=(('not' 'not' Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&' Pj('not' b 'or' ('not' a 'or' b),z) by BINARITH:10 .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&' Pj('not' b 'or' ('not' a 'or' b),z) by MARGREL1:40 .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj('not' a 'or' b,z)) by BVFUNC_1:def 7 .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' (Pj('not' a,z) 'or' Pj(b,z))) by BVFUNC_1:def 7 .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' ('not' Pj(a,z) 'or' Pj(b,z))) by VALUAT_1:def 5 .=((TRUE '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' (FALSE 'or' Pj(b,z))) by A1,A2,VALUAT_1:def 5 .=('not' Pj(b,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' (FALSE 'or' Pj(b,z))) by MARGREL1:50 .=('not' Pj(b,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(b,z)) by BINARITH:7 .=TRUE '&' ('not' Pj(b,z) 'or' Pj(b,z)) by BINARITH:18 .=TRUE '&' TRUE by BINARITH:18 .=TRUE by MARGREL1:45; hence thesis; end; theorem for a,b being Element of Funcs(Y,BOOLEAN) holds a '<' (b 'imp' a) 'eqv' a proof let a,b be Element of Funcs(Y,BOOLEAN); let z be Element of Y; assume A1:Pj(a,z)=TRUE; then A2:'not' Pj(a,z)=FALSE by MARGREL1:41; Pj((b 'imp' a) 'eqv' a,z) =Pj(('not' b 'or' a) 'eqv' a,z) by BVFUNC_4:8 .=Pj((('not' b 'or' a) 'imp' a) '&' (a 'imp' ('not' b 'or' a)),z) by BVFUNC_4:7 .=Pj(('not'( 'not' b 'or' a) 'or' a) '&' (a 'imp' ('not' b 'or' a)),z) by BVFUNC_4:8 .=Pj(('not'( 'not' b 'or' a) 'or' a) '&' ('not' a 'or' ('not' b 'or' a)),z) by BVFUNC_4:8 .=Pj('not'( 'not' b 'or' a) 'or' a,z) '&' Pj('not' a 'or' ('not' b 'or' a),z) by VALUAT_1:def 6 .=(Pj('not'( 'not' b 'or' a),z) 'or' Pj(a,z)) '&' Pj('not' a 'or' ('not' b 'or' a),z) by BVFUNC_1:def 7 .=('not' Pj('not' b 'or' a,z) 'or' Pj(a,z)) '&' Pj('not' a 'or' ('not' b 'or' a),z) by VALUAT_1:def 5 .=('not'( Pj('not' b,z) 'or' Pj(a,z)) 'or' Pj(a,z)) '&' Pj('not' a 'or' ('not' b 'or' a),z) by BVFUNC_1:def 7 .=('not'( 'not' Pj(b,z) 'or' Pj(a,z)) 'or' Pj(a,z)) '&' Pj('not' a 'or' ('not' b 'or' a),z) by VALUAT_1:def 5 .=(('not' 'not' Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&' Pj('not' a 'or' ('not' b 'or' a),z) by BINARITH:10 .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&' Pj('not' a 'or' ('not' b 'or' a),z) by MARGREL1:40 .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj('not' b 'or' a,z)) by BVFUNC_1:def 7 .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' (Pj('not' b,z) 'or' Pj(a,z))) by BVFUNC_1:def 7 .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' ('not' Pj(b,z) 'or' Pj(a,z))) by VALUAT_1:def 5 .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' ('not' Pj(b,z) 'or' Pj(a,z))) by VALUAT_1:def 5 .=TRUE '&' (FALSE 'or' ('not' Pj(b,z) 'or' TRUE)) by A1,A2,BINARITH:19 .=FALSE 'or' ('not' Pj(b,z) 'or' TRUE) by MARGREL1:50 .='not' Pj(b,z) 'or' TRUE by BINARITH:7 .=TRUE by BINARITH:19; hence thesis; end; theorem for a,b being Element of Funcs(Y,BOOLEAN) holds a '<' (a '&' b) 'eqv' (b '&' a) 'eqv' a proof let a,b be Element of Funcs(Y,BOOLEAN); let z be Element of Y; assume A1:Pj(a,z)=TRUE; A2:Pj((a '&' b) 'eqv' (a '&' b),z) =Pj(((a '&' b) 'imp' (a '&' b)) '&' ((a '&' b) 'imp' (a '&' b)),z) by BVFUNC_4:7 .=Pj((a '&' b) 'imp' (a '&' b),z) '&' Pj((a '&' b) 'imp' (a '&' b),z) by VALUAT_1:def 6 .=Pj((a '&' b) 'imp' (a '&' b),z) by BINARITH:16 .=Pj('not'( a '&' b) 'or' (a '&' b),z) by BVFUNC_4:8 .=Pj(I_el(Y),z) by BVFUNC_4:6 .=TRUE by BVFUNC_1:def 14; Pj((a '&' b) 'eqv' (b '&' a) 'eqv' a,z) =Pj((((a '&' b) 'eqv' (a '&' b)) 'imp' a) '&' (a 'imp' ((a '&' b) 'eqv' (a '&' b))),z) by BVFUNC_4:7 .=Pj(((a '&' b) 'eqv' (a '&' b)) 'imp' a,z) '&' Pj(a 'imp' ((a '&' b) 'eqv' (a '&' b)),z) by VALUAT_1:def 6 .=Pj('not'( (a '&' b) 'eqv' (a '&' b)) 'or' a,z) '&' Pj(a 'imp' ((a '&' b) 'eqv' (a '&' b)),z) by BVFUNC_4:8 .=Pj('not'( (a '&' b) 'eqv' (a '&' b)) 'or' a,z) '&' Pj('not' a 'or' ((a '&' b) 'eqv' (a '&' b)),z) by BVFUNC_4:8 .=(Pj('not'( (a '&' b) 'eqv' (a '&' b)),z) 'or' Pj(a,z)) '&' Pj('not' a 'or' ((a '&' b) 'eqv' (a '&' b)),z) by BVFUNC_1:def 7 .=(Pj('not'( (a '&' b) 'eqv' (a '&' b)),z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj((a '&' b) 'eqv' (a '&' b),z)) by BVFUNC_1:def 7 .=('not' Pj((a '&' b) 'eqv' (a '&' b),z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj((a '&' b) 'eqv' (a '&' b),z)) by VALUAT_1:def 5 .=(FALSE 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' TRUE) by A2,MARGREL1:41 .=Pj(a,z) '&' (Pj('not' a,z) 'or' TRUE) by BINARITH:7 .=TRUE '&' Pj(a,z) by BINARITH:19 .=TRUE by A1,MARGREL1:50; hence thesis; end;