:: BVFUNC25 semantic presentation begin theorem :: BVFUNC25:1 for Y being non empty set for a, b being Function of Y,BOOLEAN holds 'not' (a 'imp' b) = a '&' ('not' b) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds 'not' (a 'imp' b) = a '&' ('not' b) let a, b be Function of Y,BOOLEAN; ::_thesis: 'not' (a 'imp' b) = a '&' ('not' b) thus 'not' (a 'imp' b) = 'not' (('not' a) 'or' b) by BVFUNC_4:8 .= ('not' ('not' a)) '&' ('not' b) by BVFUNC_1:13 .= a '&' ('not' b) ; ::_thesis: verum end; theorem Th2: :: BVFUNC25:2 for Y being non empty set for b, a being Function of Y,BOOLEAN holds (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y proof let Y be non empty set ; ::_thesis: for b, a being Function of Y,BOOLEAN holds (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y let b, a be Function of Y,BOOLEAN; ::_thesis: (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = ('not' (('not' b) 'imp' ('not' a))) 'or' (a 'imp' b) by BVFUNC_4:8 .= ('not' (('not' ('not' b)) 'or' ('not' a))) 'or' (a 'imp' b) by BVFUNC_4:8 .= (('not' b) '&' ('not' ('not' a))) 'or' (a 'imp' b) by BVFUNC_1:13 .= (('not' b) '&' a) 'or' (('not' a) 'or' b) by BVFUNC_4:8 .= ((('not' b) '&' a) 'or' ('not' a)) 'or' b by BVFUNC_1:8 .= ((('not' b) 'or' ('not' a)) '&' (a 'or' ('not' a))) 'or' b by BVFUNC_1:11 .= ((('not' b) 'or' ('not' a)) '&' (I_el Y)) 'or' b by BVFUNC_4:6 .= (('not' b) 'or' ('not' a)) 'or' b by BVFUNC_1:6 .= ('not' a) 'or' (('not' b) 'or' b) by BVFUNC_1:8 .= ('not' a) 'or' (I_el Y) by BVFUNC_4:6 ; hence (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y by BVFUNC_1:10; ::_thesis: verum end; theorem Th3: :: BVFUNC25:3 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' b) 'imp' ('not' a) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' b) 'imp' ('not' a) let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' b = ('not' b) 'imp' ('not' a) (a 'imp' b) 'imp' (('not' b) 'imp' ('not' a)) = I_el Y by BVFUNC_5:32; then A1: a 'imp' b '<' ('not' b) 'imp' ('not' a) by BVFUNC_1:16; (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y by Th2; then ('not' b) 'imp' ('not' a) '<' a 'imp' b by BVFUNC_1:16; hence a 'imp' b = ('not' b) 'imp' ('not' a) by A1, BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC25:4 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'eqv' b = ('not' a) 'eqv' ('not' b) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = ('not' a) 'eqv' ('not' b) let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = ('not' a) 'eqv' ('not' b) thus ('not' a) 'eqv' ('not' b) = (('not' a) 'imp' ('not' b)) '&' (('not' b) 'imp' ('not' a)) by BVFUNC_4:7 .= (b 'imp' a) '&' (('not' b) 'imp' ('not' a)) by Th3 .= (b 'imp' a) '&' (a 'imp' b) by Th3 .= a 'eqv' b by BVFUNC_4:7 ; ::_thesis: verum end; theorem Th5: :: BVFUNC25:5 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'imp' (a '&' b) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'imp' (a '&' b) let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' b = a 'imp' (a '&' b) a 'imp' (a '&' b) = ('not' a) 'or' (a '&' b) by BVFUNC_4:8 .= (('not' a) 'or' a) '&' (('not' a) 'or' b) by BVFUNC_1:11 .= (I_el Y) '&' (('not' a) 'or' b) by BVFUNC_4:6 .= ('not' a) 'or' b by BVFUNC_1:6 ; hence a 'imp' b = a 'imp' (a '&' b) by BVFUNC_4:8; ::_thesis: verum end; theorem :: BVFUNC25:6 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' b) 'imp' (a '&' b) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' b) 'imp' (a '&' b) let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = (a 'or' b) 'imp' (a '&' b) thus (a 'or' b) 'imp' (a '&' b) = (a 'imp' (a '&' b)) '&' (b 'imp' (a '&' b)) by BVFUNC_7:5 .= (a 'imp' b) '&' (b 'imp' (a '&' b)) by Th5 .= (a 'imp' b) '&' (b 'imp' a) by Th5 .= a 'eqv' b by BVFUNC_4:7 ; ::_thesis: verum end; theorem :: BVFUNC25:7 for Y being non empty set for a being Function of Y,BOOLEAN holds a 'eqv' ('not' a) = O_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'eqv' ('not' a) = O_el Y let a be Function of Y,BOOLEAN; ::_thesis: a 'eqv' ('not' a) = O_el Y thus a 'eqv' ('not' a) = (a 'imp' ('not' a)) '&' (('not' a) 'imp' a) by BVFUNC_4:7 .= (('not' a) 'or' ('not' a)) '&' (('not' a) 'imp' a) by BVFUNC_4:8 .= ('not' a) '&' (('not' ('not' a)) 'or' a) by BVFUNC_4:8 .= O_el Y by BVFUNC_4:5 ; ::_thesis: verum end; theorem :: BVFUNC25:8 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c) let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c) thus a 'imp' (b 'imp' c) = ('not' a) 'or' (b 'imp' c) by BVFUNC_4:8 .= ('not' a) 'or' (('not' b) 'or' c) by BVFUNC_4:8 .= ('not' b) 'or' (('not' a) 'or' c) by BVFUNC_1:8 .= ('not' b) 'or' (a 'imp' c) by BVFUNC_4:8 .= b 'imp' (a 'imp' c) by BVFUNC_4:8 ; ::_thesis: verum end; theorem :: BVFUNC25:9 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c) let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c) thus (a 'imp' b) 'imp' (a 'imp' c) = (a 'imp' b) 'imp' (('not' a) 'or' c) by BVFUNC_4:8 .= ('not' (a 'imp' b)) 'or' (('not' a) 'or' c) by BVFUNC_4:8 .= ('not' (('not' a) 'or' b)) 'or' (('not' a) 'or' c) by BVFUNC_4:8 .= (('not' ('not' a)) '&' ('not' b)) 'or' (('not' a) 'or' c) by BVFUNC_1:13 .= ((a '&' ('not' b)) 'or' ('not' a)) 'or' c by BVFUNC_1:8 .= ((a 'or' ('not' a)) '&' (('not' b) 'or' ('not' a))) 'or' c by BVFUNC_1:11 .= ((I_el Y) '&' (('not' b) 'or' ('not' a))) 'or' c by BVFUNC_4:6 .= (('not' a) 'or' ('not' b)) 'or' c by BVFUNC_1:6 .= ('not' a) 'or' (('not' b) 'or' c) by BVFUNC_1:8 .= ('not' a) 'or' (b 'imp' c) by BVFUNC_4:8 .= a 'imp' (b 'imp' c) by BVFUNC_4:8 ; ::_thesis: verum end; theorem :: BVFUNC25:10 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'eqv' b = a 'xor' ('not' b) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = a 'xor' ('not' b) let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = a 'xor' ('not' b) 'not' (a 'xor' b) = 'not' ('not' (a 'eqv' b)) by BVFUNC_8:12; hence a 'eqv' b = a 'xor' ('not' b) by BVFUNC_8:17; ::_thesis: verum end; theorem :: BVFUNC25:11 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c) let a, b, c be Function of Y,BOOLEAN; ::_thesis: a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c) A1: (a '&' b) 'xor' (a '&' c) = (('not' (a '&' b)) '&' (a '&' c)) 'or' ((a '&' b) '&' ('not' (a '&' c))) by BVFUNC_4:9 .= ((('not' a) 'or' ('not' b)) '&' (a '&' c)) 'or' ((a '&' b) '&' ('not' (a '&' c))) by BVFUNC_1:14 .= ((a '&' c) '&' (('not' a) 'or' ('not' b))) 'or' ((a '&' b) '&' (('not' a) 'or' ('not' c))) by BVFUNC_1:14 .= (((a '&' c) '&' ('not' a)) 'or' ((a '&' c) '&' ('not' b))) 'or' ((a '&' b) '&' (('not' a) 'or' ('not' c))) by BVFUNC_1:12 .= (((a '&' c) '&' ('not' a)) 'or' ((a '&' c) '&' ('not' b))) 'or' (((a '&' b) '&' ('not' a)) 'or' ((a '&' b) '&' ('not' c))) by BVFUNC_1:12 .= ((a '&' c) '&' ('not' a)) 'or' (((a '&' c) '&' ('not' b)) 'or' (((a '&' b) '&' ('not' c)) 'or' ((a '&' b) '&' ('not' a)))) by BVFUNC_1:8 .= ((a '&' c) '&' ('not' a)) 'or' ((((a '&' c) '&' ('not' b)) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' b) '&' ('not' a))) by BVFUNC_1:8 .= (((a '&' c) '&' ('not' a)) 'or' ((a '&' b) '&' ('not' a))) 'or' (((a '&' c) '&' ('not' b)) 'or' ((a '&' b) '&' ('not' c))) by BVFUNC_1:8 ; A2: ((c '&' a) '&' ('not' a)) 'or' ((b '&' a) '&' ('not' a)) = (c '&' (a '&' ('not' a))) 'or' ((b '&' a) '&' ('not' a)) by BVFUNC_1:4 .= (c '&' (a '&' ('not' a))) 'or' (b '&' (a '&' ('not' a))) by BVFUNC_1:4 .= (c '&' (O_el Y)) 'or' (b '&' (a '&' ('not' a))) by BVFUNC_4:5 .= (c '&' (O_el Y)) 'or' (b '&' (O_el Y)) by BVFUNC_4:5 .= (O_el Y) 'or' (b '&' (O_el Y)) by BVFUNC_1:5 .= (O_el Y) 'or' (O_el Y) by BVFUNC_1:5 .= O_el Y ; a '&' (b 'xor' c) = a '&' ((('not' b) '&' c) 'or' (b '&' ('not' c))) by BVFUNC_4:9 .= (a '&' (('not' b) '&' c)) 'or' (a '&' (b '&' ('not' c))) by BVFUNC_1:12 .= ((a '&' c) '&' ('not' b)) 'or' (a '&' (b '&' ('not' c))) by BVFUNC_1:4 .= ((a '&' c) '&' ('not' b)) 'or' ((a '&' b) '&' ('not' c)) by BVFUNC_1:4 ; hence a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c) by A1, A2, BVFUNC_1:9; ::_thesis: verum end; theorem :: BVFUNC25:12 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'eqv' b = 'not' (a 'xor' b) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = 'not' (a 'xor' b) let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = 'not' (a 'xor' b) 'not' (a 'xor' b) = 'not' ('not' (a 'eqv' b)) by BVFUNC_8:12; hence a 'eqv' b = 'not' (a 'xor' b) ; ::_thesis: verum end; theorem :: BVFUNC25:13 for Y being non empty set for a being Function of Y,BOOLEAN holds a 'xor' a = O_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'xor' a = O_el Y let a be Function of Y,BOOLEAN; ::_thesis: a 'xor' a = O_el Y thus a 'xor' a = (('not' a) '&' a) 'or' (a '&' ('not' a)) by BVFUNC_4:9 .= O_el Y by BVFUNC_4:5 ; ::_thesis: verum end; theorem :: BVFUNC25:14 for Y being non empty set for a being Function of Y,BOOLEAN holds a 'xor' ('not' a) = I_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'xor' ('not' a) = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: a 'xor' ('not' a) = I_el Y thus a 'xor' ('not' a) = (('not' a) '&' ('not' a)) 'or' (a '&' ('not' ('not' a))) by BVFUNC_4:9 .= I_el Y by BVFUNC_4:6 ; ::_thesis: verum end; theorem :: BVFUNC25:15 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a (a 'imp' b) 'imp' (b 'imp' a) = (('not' a) 'or' b) 'imp' (b 'imp' a) by BVFUNC_4:8 .= (('not' a) 'or' b) 'imp' (('not' b) 'or' a) by BVFUNC_4:8 .= ('not' (('not' a) 'or' b)) 'or' (('not' b) 'or' a) by BVFUNC_4:8 .= (('not' ('not' a)) '&' ('not' b)) 'or' (('not' b) 'or' a) by BVFUNC_1:13 .= ((a '&' ('not' b)) 'or' ('not' b)) 'or' a by BVFUNC_1:8 .= ((a 'or' ('not' b)) '&' (('not' b) 'or' ('not' b))) 'or' a by BVFUNC_1:11 .= ((a 'or' ('not' b)) 'or' a) '&' (('not' b) 'or' a) by BVFUNC_1:11 .= (('not' b) 'or' (a 'or' a)) '&' (('not' b) 'or' a) by BVFUNC_1:8 .= ('not' b) 'or' a ; hence (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a by BVFUNC_4:8; ::_thesis: verum end; theorem Th16: :: BVFUNC25:16 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b)) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b)) let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b)) a 'xor' b = (('not' a) '&' b) 'or' (a '&' ('not' b)) by BVFUNC_4:9; hence (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b)) by BVFUNC_8:13; ::_thesis: verum end; theorem Th17: :: BVFUNC25:17 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a '&' b) 'or' (('not' a) '&' ('not' b)) = (('not' a) 'or' b) '&' (a 'or' ('not' b)) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a '&' b) 'or' (('not' a) '&' ('not' b)) = (('not' a) 'or' b) '&' (a 'or' ('not' b)) let a, b be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'or' (('not' a) '&' ('not' b)) = (('not' a) 'or' b) '&' (a 'or' ('not' b)) thus (a '&' b) 'or' (('not' a) '&' ('not' b)) = (('not' a) 'or' b) '&' (('not' ('not' a)) 'or' ('not' b)) by Th16 .= (('not' a) 'or' b) '&' (a 'or' ('not' b)) ; ::_thesis: verum end; theorem :: BVFUNC25:18 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c A1: (a 'xor' b) 'xor' c = ((('not' a) '&' b) 'or' (a '&' ('not' b))) 'xor' c by BVFUNC_4:9 .= (('not' ((('not' a) '&' b) 'or' (a '&' ('not' b)))) '&' c) 'or' (((('not' a) '&' b) 'or' (a '&' ('not' b))) '&' ('not' c)) by BVFUNC_4:9 .= ((('not' (('not' a) '&' b)) '&' ('not' (a '&' ('not' b)))) '&' c) 'or' (((('not' a) '&' b) 'or' (a '&' ('not' b))) '&' ('not' c)) by BVFUNC_1:13 .= (((('not' ('not' a)) 'or' ('not' b)) '&' ('not' (a '&' ('not' b)))) '&' c) 'or' (((('not' a) '&' b) 'or' (a '&' ('not' b))) '&' ('not' c)) by BVFUNC_1:14 .= (((a 'or' ('not' b)) '&' (('not' a) 'or' ('not' ('not' b)))) '&' c) 'or' (((('not' a) '&' b) 'or' (a '&' ('not' b))) '&' ('not' c)) by BVFUNC_1:14 .= (((a 'or' ('not' b)) '&' (('not' a) 'or' b)) '&' c) 'or' (((('not' a) '&' b) '&' ('not' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) by BVFUNC_1:12 .= (((a '&' b) 'or' (('not' a) '&' ('not' b))) '&' c) 'or' (((('not' a) '&' b) '&' ('not' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) by Th17 .= (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' c)) 'or' (((('not' a) '&' b) '&' ('not' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) by BVFUNC_1:12 .= (((a '&' b) '&' c) 'or' (((a '&' ('not' b)) '&' ('not' c)) 'or' ((('not' a) '&' b) '&' ('not' c)))) 'or' ((('not' a) '&' ('not' b)) '&' c) by BVFUNC_1:8 .= ((((a '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' ('not' c))) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' ((('not' a) '&' ('not' b)) '&' c) by BVFUNC_1:8 ; a 'xor' (b 'xor' c) = (('not' a) '&' (b 'xor' c)) 'or' (a '&' ('not' (b 'xor' c))) by BVFUNC_4:9 .= (('not' a) '&' ((('not' b) '&' c) 'or' (b '&' ('not' c)))) 'or' (a '&' ('not' (b 'xor' c))) by BVFUNC_4:9 .= (('not' a) '&' ((('not' b) '&' c) 'or' (b '&' ('not' c)))) 'or' (a '&' ('not' ((('not' b) '&' c) 'or' (b '&' ('not' c))))) by BVFUNC_4:9 .= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ('not' ((('not' b) '&' c) 'or' (b '&' ('not' c))))) by BVFUNC_1:12 .= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' (('not' (('not' b) '&' c)) '&' ('not' (b '&' ('not' c))))) by BVFUNC_1:13 .= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ((('not' ('not' b)) 'or' ('not' c)) '&' ('not' (b '&' ('not' c))))) by BVFUNC_1:14 .= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ((b 'or' ('not' c)) '&' (('not' b) 'or' ('not' ('not' c))))) by BVFUNC_1:14 .= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ((b '&' c) 'or' (('not' b) '&' ('not' c)))) by Th17 .= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:12 .= (((('not' a) '&' ('not' b)) '&' c) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:4 .= (((('not' a) '&' ('not' b)) '&' c) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:4 .= (((('not' a) '&' ('not' b)) '&' c) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' (((a '&' b) '&' c) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:4 .= (((a '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' ('not' c))) 'or' (((('not' a) '&' b) '&' ('not' c)) 'or' ((('not' a) '&' ('not' b)) '&' c)) by BVFUNC_1:4 .= ((((a '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' ('not' c))) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' ((('not' a) '&' ('not' b)) '&' c) by BVFUNC_1:8 ; hence a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c by A1; ::_thesis: verum end; theorem :: BVFUNC25:19 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c A1: (a 'eqv' b) 'eqv' c = ((a 'eqv' b) 'imp' c) '&' (c 'imp' (a 'eqv' b)) by BVFUNC_4:7 .= (((a 'imp' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' (a 'eqv' b)) by BVFUNC_4:7 .= (((a 'imp' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:7 .= (((('not' a) 'or' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8 .= (((('not' a) 'or' b) '&' (('not' b) 'or' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8 .= (('not' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) 'or' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8 .= (('not' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) 'or' c) '&' (('not' c) 'or' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8 .= (('not' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (b 'imp' a))) by BVFUNC_4:8 .= (('not' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by BVFUNC_4:8 .= ((('not' (('not' a) 'or' b)) 'or' ('not' (('not' b) 'or' a))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by BVFUNC_1:14 .= (((('not' ('not' a)) '&' ('not' b)) 'or' ('not' (('not' b) 'or' a))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by BVFUNC_1:13 .= (((a '&' ('not' b)) 'or' (('not' ('not' b)) '&' ('not' a))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by BVFUNC_1:13 .= (((a 'or' b) '&' (('not' a) 'or' ('not' b))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by Th16 .= (((a 'or' b) 'or' c) '&' ((('not' a) 'or' ('not' b)) 'or' c)) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by BVFUNC_1:11 .= (((a 'or' b) 'or' c) '&' ((('not' a) 'or' ('not' b)) 'or' c)) '&' (((a 'or' ('not' b)) 'or' ('not' c)) '&' ((('not' a) 'or' b) 'or' ('not' c))) by BVFUNC_1:11 .= (((a 'or' b) 'or' c) '&' (((a 'or' ('not' b)) 'or' ('not' c)) '&' ((('not' a) 'or' b) 'or' ('not' c)))) '&' ((('not' a) 'or' ('not' b)) 'or' c) by BVFUNC_1:4 .= ((((a 'or' b) 'or' c) '&' ((a 'or' ('not' b)) 'or' ('not' c))) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' ((('not' a) 'or' ('not' b)) 'or' c) by BVFUNC_1:4 ; a 'eqv' (b 'eqv' c) = (a 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' a) by BVFUNC_4:7 .= (a 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' ((b 'eqv' c) 'imp' a) by BVFUNC_4:7 .= (a 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:7 .= (('not' a) 'or' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8 .= (('not' a) 'or' ((('not' b) 'or' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8 .= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8 .= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8 .= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) 'imp' a) by BVFUNC_4:8 .= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (('not' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) 'or' a) by BVFUNC_4:8 .= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' ((('not' (('not' b) 'or' c)) 'or' ('not' (('not' c) 'or' b))) 'or' a) by BVFUNC_1:14 .= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' ('not' b)) '&' ('not' c)) 'or' ('not' (('not' c) 'or' b))) 'or' a) by BVFUNC_1:13 .= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((b '&' ('not' c)) 'or' (('not' ('not' c)) '&' ('not' b))) 'or' a) by BVFUNC_1:13 .= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((b 'or' c) '&' (('not' b) 'or' ('not' c))) 'or' a) by Th16 .= ((('not' a) 'or' (('not' b) 'or' c)) '&' (('not' a) 'or' (('not' c) 'or' b))) '&' (((b 'or' c) '&' (('not' b) 'or' ('not' c))) 'or' a) by BVFUNC_1:11 .= (((('not' a) 'or' ('not' b)) 'or' c) '&' (('not' a) 'or' (b 'or' ('not' c)))) '&' (((b 'or' c) '&' (('not' b) 'or' ('not' c))) 'or' a) by BVFUNC_1:8 .= (((('not' a) 'or' ('not' b)) 'or' c) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' (((b 'or' c) '&' (('not' b) 'or' ('not' c))) 'or' a) by BVFUNC_1:8 .= (((('not' a) 'or' ('not' b)) 'or' c) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' ((a 'or' (b 'or' c)) '&' (a 'or' (('not' b) 'or' ('not' c)))) by BVFUNC_1:11 .= (((('not' a) 'or' ('not' b)) 'or' c) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' (((a 'or' b) 'or' c) '&' (a 'or' (('not' b) 'or' ('not' c)))) by BVFUNC_1:8 .= (((('not' a) 'or' ('not' b)) 'or' c) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' (((a 'or' b) 'or' c) '&' ((a 'or' ('not' b)) 'or' ('not' c))) by BVFUNC_1:8 .= ((((a 'or' b) 'or' c) '&' ((a 'or' ('not' b)) 'or' ('not' c))) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' ((('not' a) 'or' ('not' b)) 'or' c) by BVFUNC_1:4 ; hence a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c by A1; ::_thesis: verum end; theorem :: BVFUNC25:20 for Y being non empty set for a being Function of Y,BOOLEAN holds ('not' ('not' a)) 'imp' a = I_el Y by BVFUNC_5:7; theorem :: BVFUNC25:21 for Y being non empty set for a, b being Function of Y,BOOLEAN holds ((a 'imp' b) '&' a) 'imp' b = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ((a 'imp' b) '&' a) 'imp' b = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' b) '&' a) 'imp' b = I_el Y ((a 'imp' b) '&' a) 'imp' b = (a '&' b) 'imp' b by BVFUNC_7:10; hence ((a 'imp' b) '&' a) 'imp' b = I_el Y by BVFUNC_6:40; ::_thesis: verum end; theorem Th22: :: BVFUNC25:22 for Y being non empty set for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'imp' a) = I_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'imp' a) = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: a 'imp' (('not' a) 'imp' a) = I_el Y a 'imp' (('not' a) 'imp' a) = ('not' a) 'or' (('not' a) 'imp' a) by BVFUNC_4:8 .= ('not' a) 'or' (('not' ('not' a)) 'or' a) by BVFUNC_4:8 .= ('not' a) 'or' a ; hence a 'imp' (('not' a) 'imp' a) = I_el Y by BVFUNC_4:6; ::_thesis: verum end; theorem :: BVFUNC25:23 for Y being non empty set for a being Function of Y,BOOLEAN holds (('not' a) 'imp' a) 'eqv' a = I_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (('not' a) 'imp' a) 'eqv' a = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: (('not' a) 'imp' a) 'eqv' a = I_el Y (('not' a) 'imp' a) 'eqv' a = ((('not' a) 'imp' a) 'imp' a) '&' (a 'imp' (('not' a) 'imp' a)) by BVFUNC_4:7 .= (I_el Y) '&' (a 'imp' (('not' a) 'imp' a)) by BVFUNC_5:11 .= a 'imp' (('not' a) 'imp' a) by BVFUNC_1:6 ; hence (('not' a) 'imp' a) 'eqv' a = I_el Y by Th22; ::_thesis: verum end; theorem :: BVFUNC25:24 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'or' (a 'imp' b) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' (a 'imp' b) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' (a 'imp' b) = I_el Y a 'or' (a 'imp' b) = a 'or' (('not' a) 'or' b) by BVFUNC_4:8 .= (a 'or' ('not' a)) 'or' b by BVFUNC_1:8 .= (I_el Y) 'or' b by BVFUNC_4:6 ; hence a 'or' (a 'imp' b) = I_el Y by BVFUNC_1:10; ::_thesis: verum end; theorem :: BVFUNC25:25 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (c 'imp' a) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (c 'imp' a) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'or' (c 'imp' a) = I_el Y (a 'imp' b) 'or' (c 'imp' a) = (('not' a) 'or' b) 'or' (c 'imp' a) by BVFUNC_4:8 .= (('not' a) 'or' b) 'or' (('not' c) 'or' a) by BVFUNC_4:8 .= ('not' c) 'or' (a 'or' (('not' a) 'or' b)) by BVFUNC_1:8 .= ('not' c) 'or' ((a 'or' ('not' a)) 'or' b) by BVFUNC_1:8 .= ('not' c) 'or' ((I_el Y) 'or' b) by BVFUNC_4:6 .= ('not' c) 'or' (I_el Y) by BVFUNC_1:10 ; hence (a 'imp' b) 'or' (c 'imp' a) = I_el Y by BVFUNC_1:10; ::_thesis: verum end; theorem :: BVFUNC25:26 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y (a 'imp' b) 'or' (('not' a) 'imp' b) = (('not' a) 'or' b) 'or' (('not' a) 'imp' b) by BVFUNC_4:8 .= (('not' a) 'or' b) 'or' (('not' ('not' a)) 'or' b) by BVFUNC_4:8 .= b 'or' (('not' a) 'or' (a 'or' b)) by BVFUNC_1:8 .= b 'or' ((('not' a) 'or' a) 'or' b) by BVFUNC_1:8 .= b 'or' ((I_el Y) 'or' b) by BVFUNC_4:6 .= b 'or' (I_el Y) by BVFUNC_1:10 ; hence (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y by BVFUNC_1:10; ::_thesis: verum end; theorem :: BVFUNC25:27 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y (a 'imp' b) 'or' (a 'imp' ('not' b)) = (('not' a) 'or' b) 'or' (a 'imp' ('not' b)) by BVFUNC_4:8 .= (('not' a) 'or' b) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_4:8 .= ('not' a) 'or' (b 'or' (('not' b) 'or' ('not' a))) by BVFUNC_1:8 .= ('not' a) 'or' ((b 'or' ('not' b)) 'or' ('not' a)) by BVFUNC_1:8 .= ('not' a) 'or' ((I_el Y) 'or' ('not' a)) by BVFUNC_4:6 .= ('not' a) 'or' (I_el Y) by BVFUNC_1:10 ; hence (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y by BVFUNC_1:10; ::_thesis: verum end; theorem :: BVFUNC25:28 for Y being non empty set for a, b being Function of Y,BOOLEAN holds ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = ('not' ('not' a)) 'or' (('not' b) 'eqv' (b 'imp' a)) by BVFUNC_4:8 .= a 'or' ((('not' b) 'imp' (b 'imp' a)) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_4:7 .= a 'or' ((('not' ('not' b)) 'or' (b 'imp' a)) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_4:8 .= a 'or' ((b 'or' (('not' b) 'or' a)) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_4:8 .= a 'or' (((b 'or' ('not' b)) 'or' a) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_1:8 .= a 'or' (((I_el Y) 'or' a) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_4:6 .= a 'or' ((I_el Y) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_1:10 .= a 'or' ((b 'imp' a) 'imp' ('not' b)) by BVFUNC_1:6 .= a 'or' ((('not' b) 'or' a) 'imp' ('not' b)) by BVFUNC_4:8 .= a 'or' (('not' (('not' b) 'or' a)) 'or' ('not' b)) by BVFUNC_4:8 .= a 'or' ((('not' ('not' b)) '&' ('not' a)) 'or' ('not' b)) by BVFUNC_1:13 .= a 'or' ((b 'or' ('not' b)) '&' (('not' a) 'or' ('not' b))) by BVFUNC_1:11 .= a 'or' ((I_el Y) '&' (('not' a) 'or' ('not' b))) by BVFUNC_4:6 .= a 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:6 .= (a 'or' ('not' a)) 'or' ('not' b) by BVFUNC_1:8 .= (I_el Y) 'or' ('not' b) by BVFUNC_4:6 ; hence ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y by BVFUNC_1:10; ::_thesis: verum end; theorem :: BVFUNC25:29 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el Y (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = ('not' (a 'imp' b)) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_4:8 .= ('not' (('not' a) 'or' b)) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_4:8 .= (('not' ('not' a)) '&' ('not' b)) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_1:13 .= (a '&' ('not' b)) 'or' (('not' ((a 'imp' c) 'imp' b)) 'or' b) by BVFUNC_4:8 .= (a '&' ('not' b)) 'or' (('not' ((('not' a) 'or' c) 'imp' b)) 'or' b) by BVFUNC_4:8 .= (a '&' ('not' b)) 'or' (('not' (('not' (('not' a) 'or' c)) 'or' b)) 'or' b) by BVFUNC_4:8 .= (a '&' ('not' b)) 'or' (('not' ((('not' ('not' a)) '&' ('not' c)) 'or' b)) 'or' b) by BVFUNC_1:13 .= (a '&' ('not' b)) 'or' ((('not' (a '&' ('not' c))) '&' ('not' b)) 'or' b) by BVFUNC_1:13 .= (a '&' ('not' b)) 'or' (((('not' a) 'or' ('not' ('not' c))) '&' ('not' b)) 'or' b) by BVFUNC_1:14 .= (a '&' ('not' b)) 'or' (((('not' a) 'or' c) 'or' b) '&' (('not' b) 'or' b)) by BVFUNC_1:11 .= (a '&' ('not' b)) 'or' (((('not' a) 'or' c) 'or' b) '&' (I_el Y)) by BVFUNC_4:6 .= (a '&' ('not' b)) 'or' ((('not' a) 'or' c) 'or' b) by BVFUNC_1:6 .= ((a '&' ('not' b)) 'or' b) 'or' (('not' a) 'or' c) by BVFUNC_1:8 .= ((a 'or' b) '&' (('not' b) 'or' b)) 'or' (('not' a) 'or' c) by BVFUNC_1:11 .= ((a 'or' b) '&' (I_el Y)) 'or' (('not' a) 'or' c) by BVFUNC_4:6 .= (a 'or' b) 'or' (('not' a) 'or' c) by BVFUNC_1:6 .= b 'or' (a 'or' (('not' a) 'or' c)) by BVFUNC_1:8 .= b 'or' ((a 'or' ('not' a)) 'or' c) by BVFUNC_1:8 .= b 'or' ((I_el Y) 'or' c) by BVFUNC_4:6 .= b 'or' (I_el Y) by BVFUNC_1:10 ; hence (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el Y by BVFUNC_1:10; ::_thesis: verum end; theorem :: BVFUNC25:30 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'eqv' (a '&' b) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'eqv' (a '&' b) let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' b = a 'eqv' (a '&' b) a 'eqv' (a '&' b) = (a 'imp' (a '&' b)) '&' ((a '&' b) 'imp' a) by BVFUNC_4:7 .= (('not' a) 'or' (a '&' b)) '&' ((a '&' b) 'imp' a) by BVFUNC_4:8 .= (('not' a) 'or' (a '&' b)) '&' (('not' (a '&' b)) 'or' a) by BVFUNC_4:8 .= ((('not' a) 'or' a) '&' (('not' a) 'or' b)) '&' (('not' (a '&' b)) 'or' a) by BVFUNC_1:11 .= ((I_el Y) '&' (('not' a) 'or' b)) '&' (('not' (a '&' b)) 'or' a) by BVFUNC_4:6 .= (('not' a) 'or' b) '&' (('not' (a '&' b)) 'or' a) by BVFUNC_1:6 .= (('not' a) 'or' b) '&' ((('not' a) 'or' ('not' b)) 'or' a) by BVFUNC_1:14 .= (('not' a) 'or' b) '&' (('not' b) 'or' (('not' a) 'or' a)) by BVFUNC_1:8 .= (('not' a) 'or' b) '&' (('not' b) 'or' (I_el Y)) by BVFUNC_4:6 .= (('not' a) 'or' b) '&' (I_el Y) by BVFUNC_1:10 .= ('not' a) 'or' b by BVFUNC_1:6 ; hence a 'imp' b = a 'eqv' (a '&' b) by BVFUNC_4:8; ::_thesis: verum end; theorem :: BVFUNC25:31 for Y being non empty set for a, b being Function of Y,BOOLEAN holds ( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b ) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b ) let a, b be Function of Y,BOOLEAN; ::_thesis: ( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b ) ( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ) by BVFUNC_4:10; hence ( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b ) by BVFUNC_1:17; ::_thesis: verum end; theorem :: BVFUNC25:32 for Y being non empty set for a being Function of Y,BOOLEAN holds a = ('not' a) 'imp' a proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a = ('not' a) 'imp' a let a be Function of Y,BOOLEAN; ::_thesis: a = ('not' a) 'imp' a (('not' a) 'imp' a) 'imp' a = I_el Y by BVFUNC_5:11; then A1: ('not' a) 'imp' a '<' a by BVFUNC_1:16; a 'imp' (('not' a) 'imp' a) = I_el Y by Th22; then a '<' ('not' a) 'imp' a by BVFUNC_1:16; hence a = ('not' a) 'imp' a by A1, BVFUNC_1:15; ::_thesis: verum end; theorem Th33: :: BVFUNC25:33 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'imp' ((a 'imp' b) 'imp' a) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' ((a 'imp' b) 'imp' a) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' ((a 'imp' b) 'imp' a) = I_el Y thus a 'imp' ((a 'imp' b) 'imp' a) = ('not' a) 'or' ((a 'imp' b) 'imp' a) by BVFUNC_4:8 .= ('not' a) 'or' (('not' (a 'imp' b)) 'or' a) by BVFUNC_4:8 .= ('not' a) 'or' (('not' (('not' a) 'or' b)) 'or' a) by BVFUNC_4:8 .= ('not' a) 'or' ((('not' ('not' a)) '&' ('not' b)) 'or' a) by BVFUNC_1:13 .= (('not' a) 'or' a) 'or' (a '&' ('not' b)) by BVFUNC_1:8 .= (I_el Y) 'or' (a '&' ('not' b)) by BVFUNC_4:6 .= I_el Y by BVFUNC_1:10 ; ::_thesis: verum end; theorem :: BVFUNC25:34 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a = (a 'imp' b) 'imp' a proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a = (a 'imp' b) 'imp' a let a, b be Function of Y,BOOLEAN; ::_thesis: a = (a 'imp' b) 'imp' a ((a 'imp' b) 'imp' a) 'imp' a = I_el Y by BVFUNC_8:27; then A1: (a 'imp' b) 'imp' a '<' a by BVFUNC_1:16; a 'imp' ((a 'imp' b) 'imp' a) = I_el Y by Th33; then a '<' (a 'imp' b) 'imp' a by BVFUNC_1:16; hence a = (a 'imp' b) 'imp' a by A1, BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC25:35 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a = (b 'imp' a) '&' (('not' b) 'imp' a) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a = (b 'imp' a) '&' (('not' b) 'imp' a) let a, b be Function of Y,BOOLEAN; ::_thesis: a = (b 'imp' a) '&' (('not' b) 'imp' a) a = (a 'or' b) '&' (a 'or' ('not' b)) by BVFUNC_8:7 .= (a 'or' ('not' ('not' b))) '&' (b 'imp' a) by BVFUNC_4:8 .= (('not' b) 'imp' a) '&' (b 'imp' a) by BVFUNC_4:8 ; hence a = (b 'imp' a) '&' (('not' b) 'imp' a) ; ::_thesis: verum end; theorem :: BVFUNC25:36 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a '&' b = 'not' (a 'imp' ('not' b)) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' b = 'not' (a 'imp' ('not' b)) let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' b = 'not' (a 'imp' ('not' b)) ('not' (a 'imp' ('not' b))) 'imp' (a '&' b) = I_el Y by BVFUNC_6:35; then A1: 'not' (a 'imp' ('not' b)) '<' a '&' b by BVFUNC_1:16; (a '&' b) 'imp' ('not' (a 'imp' ('not' b))) = I_el Y by BVFUNC_6:34; then a '&' b '<' 'not' (a 'imp' ('not' b)) by BVFUNC_1:16; hence a '&' b = 'not' (a 'imp' ('not' b)) by A1, BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC25:37 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'or' b = ('not' a) 'imp' b proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' b = ('not' a) 'imp' b let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' b = ('not' a) 'imp' b thus ('not' a) 'imp' b = ('not' ('not' a)) 'or' b by BVFUNC_4:8 .= a 'or' b ; ::_thesis: verum end; theorem :: BVFUNC25:38 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'or' b = (a 'imp' b) 'imp' b proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' b = (a 'imp' b) 'imp' b let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' b = (a 'imp' b) 'imp' b thus (a 'imp' b) 'imp' b = ('not' (a 'imp' b)) 'or' b by BVFUNC_4:8 .= ('not' (('not' a) 'or' b)) 'or' b by BVFUNC_4:8 .= (('not' ('not' a)) '&' ('not' b)) 'or' b by BVFUNC_1:13 .= (a 'or' b) '&' (('not' b) 'or' b) by BVFUNC_1:11 .= (a 'or' b) '&' (I_el Y) by BVFUNC_4:6 .= a 'or' b by BVFUNC_1:6 ; ::_thesis: verum end; theorem :: BVFUNC25:39 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (a 'imp' a) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (a 'imp' a) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' (a 'imp' a) = I_el Y thus (a 'imp' b) 'imp' (a 'imp' a) = (a 'imp' b) 'imp' (I_el Y) by BVFUNC_5:7 .= I_el Y by BVFUNC_7:16 ; ::_thesis: verum end; theorem :: BVFUNC25:40 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el Y let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el Y thus (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = ('not' (a 'imp' (b 'imp' c))) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) by BVFUNC_4:8 .= ('not' (('not' a) 'or' (b 'imp' c))) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) by BVFUNC_4:8 .= ('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) by BVFUNC_4:8 .= ('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' (('not' (d 'imp' b)) 'or' (a 'imp' (d 'imp' c))) by BVFUNC_4:8 .= ('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' (('not' (('not' d) 'or' b)) 'or' (a 'imp' (d 'imp' c))) by BVFUNC_4:8 .= ('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' (('not' (('not' d) 'or' b)) 'or' (('not' a) 'or' (d 'imp' c))) by BVFUNC_4:8 .= ('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' (('not' (('not' d) 'or' b)) 'or' (('not' a) 'or' (('not' d) 'or' c))) by BVFUNC_4:8 .= (('not' ('not' a)) '&' ('not' (('not' b) 'or' c))) 'or' (('not' (('not' d) 'or' b)) 'or' (('not' a) 'or' (('not' d) 'or' c))) by BVFUNC_1:13 .= (('not' ('not' a)) '&' (('not' ('not' b)) '&' ('not' c))) 'or' (('not' (('not' d) 'or' b)) 'or' (('not' a) 'or' (('not' d) 'or' c))) by BVFUNC_1:13 .= (a '&' (('not' ('not' b)) '&' ('not' c))) 'or' ((('not' ('not' d)) '&' ('not' b)) 'or' (('not' a) 'or' (('not' d) 'or' c))) by BVFUNC_1:13 .= (a '&' (b '&' ('not' c))) 'or' (((d '&' ('not' b)) 'or' ('not' a)) 'or' (('not' d) 'or' c)) by BVFUNC_1:8 .= ((a '&' (b '&' ('not' c))) 'or' (('not' a) 'or' (d '&' ('not' b)))) 'or' (('not' d) 'or' c) by BVFUNC_1:8 .= (((a '&' (b '&' ('not' c))) 'or' ('not' a)) 'or' (d '&' ('not' b))) 'or' (('not' d) 'or' c) by BVFUNC_1:8 .= (((a 'or' ('not' a)) '&' ((b '&' ('not' c)) 'or' ('not' a))) 'or' (d '&' ('not' b))) 'or' (('not' d) 'or' c) by BVFUNC_1:11 .= (((I_el Y) '&' ((b '&' ('not' c)) 'or' ('not' a))) 'or' (d '&' ('not' b))) 'or' (('not' d) 'or' c) by BVFUNC_4:6 .= (((b '&' ('not' c)) 'or' ('not' a)) 'or' (d '&' ('not' b))) 'or' (('not' d) 'or' c) by BVFUNC_1:6 .= ((b '&' ('not' c)) 'or' ('not' a)) 'or' ((d '&' ('not' b)) 'or' (('not' d) 'or' c)) by BVFUNC_1:8 .= ((b '&' ('not' c)) 'or' ('not' a)) 'or' (((('not' b) '&' d) 'or' ('not' d)) 'or' c) by BVFUNC_1:8 .= ((b '&' ('not' c)) 'or' ('not' a)) 'or' (((('not' b) 'or' ('not' d)) '&' (d 'or' ('not' d))) 'or' c) by BVFUNC_1:11 .= ((b '&' ('not' c)) 'or' ('not' a)) 'or' (((('not' b) 'or' ('not' d)) '&' (I_el Y)) 'or' c) by BVFUNC_4:6 .= ((b '&' ('not' c)) 'or' ('not' a)) 'or' ((('not' b) 'or' ('not' d)) 'or' c) by BVFUNC_1:6 .= ('not' a) 'or' ((('not' c) '&' b) 'or' ((('not' b) 'or' ('not' d)) 'or' c)) by BVFUNC_1:8 .= ('not' a) 'or' (((('not' c) '&' b) 'or' (('not' b) 'or' ('not' d))) 'or' c) by BVFUNC_1:8 .= ('not' a) 'or' ((((('not' c) '&' b) 'or' ('not' b)) 'or' ('not' d)) 'or' c) by BVFUNC_1:8 .= ('not' a) 'or' ((((('not' c) 'or' ('not' b)) '&' (b 'or' ('not' b))) 'or' ('not' d)) 'or' c) by BVFUNC_1:11 .= ('not' a) 'or' ((((('not' c) 'or' ('not' b)) '&' (I_el Y)) 'or' ('not' d)) 'or' c) by BVFUNC_4:6 .= ('not' a) 'or' (((('not' b) 'or' ('not' c)) 'or' ('not' d)) 'or' c) by BVFUNC_1:6 .= ('not' a) 'or' ((('not' b) 'or' (('not' c) 'or' ('not' d))) 'or' c) by BVFUNC_1:8 .= ('not' a) 'or' (('not' b) 'or' ((('not' d) 'or' ('not' c)) 'or' c)) by BVFUNC_1:8 .= ('not' a) 'or' (('not' b) 'or' (('not' d) 'or' (('not' c) 'or' c))) by BVFUNC_1:8 .= ('not' a) 'or' (('not' b) 'or' (('not' d) 'or' (I_el Y))) by BVFUNC_4:6 .= ('not' a) 'or' (('not' b) 'or' (I_el Y)) by BVFUNC_1:10 .= ('not' a) 'or' (I_el Y) by BVFUNC_1:10 .= I_el Y by BVFUNC_1:10 ; ::_thesis: verum end; theorem :: BVFUNC25:41 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el Y thus (((a 'imp' b) '&' a) '&' c) 'imp' b = (((('not' a) 'or' b) '&' a) '&' c) 'imp' b by BVFUNC_4:8 .= (((('not' a) '&' a) 'or' (b '&' a)) '&' c) 'imp' b by BVFUNC_1:12 .= (((O_el Y) 'or' (b '&' a)) '&' c) 'imp' b by BVFUNC_4:5 .= ((b '&' a) '&' c) 'imp' b by BVFUNC_1:9 .= ('not' ((b '&' a) '&' c)) 'or' b by BVFUNC_4:8 .= (('not' (b '&' a)) 'or' ('not' c)) 'or' b by BVFUNC_1:14 .= ((('not' b) 'or' ('not' a)) 'or' ('not' c)) 'or' b by BVFUNC_1:14 .= (b 'or' (('not' b) 'or' ('not' a))) 'or' ('not' c) by BVFUNC_1:8 .= ((b 'or' ('not' b)) 'or' ('not' a)) 'or' ('not' c) by BVFUNC_1:8 .= ((I_el Y) 'or' ('not' a)) 'or' ('not' c) by BVFUNC_4:6 .= (I_el Y) 'or' ('not' c) by BVFUNC_1:10 .= I_el Y by BVFUNC_1:10 ; ::_thesis: verum end; theorem :: BVFUNC25:42 for Y being non empty set for b, c, a being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el Y proof let Y be non empty set ; ::_thesis: for b, c, a being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el Y let b, c, a be Function of Y,BOOLEAN; ::_thesis: (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el Y thus (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = ('not' (b 'imp' c)) 'or' ((a '&' b) 'imp' c) by BVFUNC_4:8 .= ('not' (('not' b) 'or' c)) 'or' ((a '&' b) 'imp' c) by BVFUNC_4:8 .= ('not' (('not' b) 'or' c)) 'or' (('not' (a '&' b)) 'or' c) by BVFUNC_4:8 .= (('not' ('not' b)) '&' ('not' c)) 'or' (('not' (a '&' b)) 'or' c) by BVFUNC_1:13 .= (b '&' ('not' c)) 'or' ((('not' a) 'or' ('not' b)) 'or' c) by BVFUNC_1:14 .= ((b '&' ('not' c)) 'or' c) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:8 .= ((b 'or' c) '&' (('not' c) 'or' c)) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:11 .= ((b 'or' c) '&' (I_el Y)) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_4:6 .= (('not' a) 'or' ('not' b)) 'or' (b 'or' c) by BVFUNC_1:6 .= ((('not' a) 'or' ('not' b)) 'or' b) 'or' c by BVFUNC_1:8 .= (('not' a) 'or' (('not' b) 'or' b)) 'or' c by BVFUNC_1:8 .= (('not' a) 'or' (I_el Y)) 'or' c by BVFUNC_4:6 .= (I_el Y) 'or' c by BVFUNC_1:10 .= I_el Y by BVFUNC_1:10 ; ::_thesis: verum end; theorem :: BVFUNC25:43 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el Y ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = (('not' (a '&' b)) 'or' c) 'imp' ((a '&' b) 'imp' (c '&' b)) by BVFUNC_4:8 .= ('not' (('not' (a '&' b)) 'or' c)) 'or' ((a '&' b) 'imp' (c '&' b)) by BVFUNC_4:8 .= ('not' (('not' (a '&' b)) 'or' c)) 'or' (('not' (a '&' b)) 'or' (c '&' b)) by BVFUNC_4:8 .= (('not' ('not' (a '&' b))) '&' ('not' c)) 'or' (('not' (a '&' b)) 'or' (c '&' b)) by BVFUNC_1:13 .= ((a '&' b) '&' ('not' c)) 'or' ((('not' a) 'or' ('not' b)) 'or' (c '&' b)) by BVFUNC_1:14 .= ((a '&' b) '&' ('not' c)) 'or' (('not' a) 'or' (('not' b) 'or' (b '&' c))) by BVFUNC_1:8 .= ((a '&' b) '&' ('not' c)) 'or' (('not' a) 'or' ((('not' b) 'or' b) '&' (('not' b) 'or' c))) by BVFUNC_1:11 .= ((a '&' b) '&' ('not' c)) 'or' (('not' a) 'or' ((I_el Y) '&' (('not' b) 'or' c))) by BVFUNC_4:6 .= ((a '&' b) '&' ('not' c)) 'or' (('not' a) 'or' (('not' b) 'or' c)) by BVFUNC_1:6 .= (((a '&' b) '&' ('not' c)) 'or' ('not' a)) 'or' (('not' b) 'or' c) by BVFUNC_1:8 .= (((a '&' b) 'or' ('not' a)) '&' (('not' c) 'or' ('not' a))) 'or' (('not' b) 'or' c) by BVFUNC_1:11 .= (((a 'or' ('not' a)) '&' (b 'or' ('not' a))) '&' (('not' c) 'or' ('not' a))) 'or' (('not' b) 'or' c) by BVFUNC_1:11 .= (((I_el Y) '&' (b 'or' ('not' a))) '&' (('not' c) 'or' ('not' a))) 'or' (('not' b) 'or' c) by BVFUNC_4:6 .= ((b 'or' ('not' a)) '&' (('not' c) 'or' ('not' a))) 'or' (('not' b) 'or' c) by BVFUNC_1:6 .= (((b 'or' ('not' a)) '&' (('not' c) 'or' ('not' a))) 'or' c) 'or' ('not' b) by BVFUNC_1:8 .= (((b 'or' ('not' a)) 'or' c) '&' ((('not' c) 'or' ('not' a)) 'or' c)) 'or' ('not' b) by BVFUNC_1:11 .= (((b 'or' ('not' a)) 'or' c) '&' (('not' a) 'or' (('not' c) 'or' c))) 'or' ('not' b) by BVFUNC_1:8 .= (((b 'or' ('not' a)) 'or' c) '&' (('not' a) 'or' (I_el Y))) 'or' ('not' b) by BVFUNC_4:6 .= (((b 'or' ('not' a)) 'or' c) '&' (I_el Y)) 'or' ('not' b) by BVFUNC_1:10 .= ((b 'or' ('not' a)) 'or' c) 'or' ('not' b) by BVFUNC_1:6 .= (('not' b) 'or' (b 'or' ('not' a))) 'or' c by BVFUNC_1:8 .= ((('not' b) 'or' b) 'or' ('not' a)) 'or' c by BVFUNC_1:8 .= ((I_el Y) 'or' ('not' a)) 'or' c by BVFUNC_4:6 .= (I_el Y) 'or' c by BVFUNC_1:10 ; hence ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el Y by BVFUNC_1:10; ::_thesis: verum end; theorem :: BVFUNC25:44 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y a 'imp' b '<' (a '&' c) 'imp' (b '&' c) by BVFUNC_9:10; hence (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC25:45 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = I_el Y ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = (((a 'imp' b) '&' a) '&' c) 'imp' (b '&' c) by BVFUNC_1:4 .= ((a '&' b) '&' c) 'imp' (b '&' c) by BVFUNC_7:10 .= (a '&' (b '&' c)) 'imp' (b '&' c) by BVFUNC_1:4 ; hence ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = I_el Y by BVFUNC_6:38; ::_thesis: verum end; theorem :: BVFUNC25:46 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a '&' (a 'imp' b)) '&' (b 'imp' c) '<' c proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a '&' (a 'imp' b)) '&' (b 'imp' c) '<' c let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a '&' (a 'imp' b)) '&' (b 'imp' c) '<' c ((a '&' (a 'imp' b)) '&' (b 'imp' c)) 'imp' c = ('not' ((a '&' (a 'imp' b)) '&' (b 'imp' c))) 'or' c by BVFUNC_4:8 .= ('not' ((a '&' b) '&' (b 'imp' c))) 'or' c by BVFUNC_7:10 .= ('not' (a '&' (b '&' (b 'imp' c)))) 'or' c by BVFUNC_1:4 .= ('not' (a '&' (b '&' c))) 'or' c by BVFUNC_7:10 .= ('not' ((a '&' b) '&' c)) 'or' c by BVFUNC_1:4 .= (('not' (a '&' b)) 'or' ('not' c)) 'or' c by BVFUNC_1:14 .= ('not' (a '&' b)) 'or' (('not' c) 'or' c) by BVFUNC_1:8 .= ('not' (a '&' b)) 'or' (I_el Y) by BVFUNC_4:6 .= I_el Y by BVFUNC_1:10 ; hence (a '&' (a 'imp' b)) '&' (b 'imp' c) '<' c by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC25:47 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c) let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c) (((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c)) 'imp' (('not' a) 'imp' (b 'or' c)) = ('not' (((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c))) 'or' (('not' a) 'imp' (b 'or' c)) by BVFUNC_4:8 .= ('not' (((a 'or' b) '&' (('not' a) 'or' c)) '&' (b 'imp' c))) 'or' (('not' a) 'imp' (b 'or' c)) by BVFUNC_4:8 .= ('not' (((a 'or' b) '&' (('not' a) 'or' c)) '&' (('not' b) 'or' c))) 'or' (('not' a) 'imp' (b 'or' c)) by BVFUNC_4:8 .= ('not' (((a 'or' b) '&' (('not' a) 'or' c)) '&' (('not' b) 'or' c))) 'or' (('not' ('not' a)) 'or' (b 'or' c)) by BVFUNC_4:8 .= (('not' ((a 'or' b) '&' (('not' a) 'or' c))) 'or' ('not' (('not' b) 'or' c))) 'or' (('not' ('not' a)) 'or' (b 'or' c)) by BVFUNC_1:14 .= (('not' ((a 'or' b) '&' (('not' a) 'or' c))) 'or' (('not' ('not' b)) '&' ('not' c))) 'or' (('not' ('not' a)) 'or' (b 'or' c)) by BVFUNC_1:13 .= ((('not' (a 'or' b)) 'or' ('not' (('not' a) 'or' c))) 'or' (b '&' ('not' c))) 'or' (('not' ('not' a)) 'or' (b 'or' c)) by BVFUNC_1:14 .= (((('not' a) '&' ('not' b)) 'or' ('not' (('not' a) 'or' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:13 .= (((('not' a) '&' ('not' b)) 'or' (('not' ('not' a)) '&' ('not' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:13 .= (((('not' a) 'or' (a '&' ('not' c))) '&' (('not' b) 'or' (a '&' ('not' c)))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:11 .= ((((('not' a) 'or' a) '&' (('not' a) 'or' ('not' c))) '&' (('not' b) 'or' (a '&' ('not' c)))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:11 .= ((((I_el Y) '&' (('not' a) 'or' ('not' c))) '&' (('not' b) 'or' (a '&' ('not' c)))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_4:6 .= (((('not' a) 'or' ('not' c)) '&' (('not' b) 'or' (a '&' ('not' c)))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:6 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' ((('not' a) 'or' ('not' c)) '&' (a '&' ('not' c)))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:12 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((('not' a) 'or' ('not' c)) '&' a) '&' ('not' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:4 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((('not' a) '&' a) 'or' (('not' c) '&' a)) '&' ('not' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:12 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((O_el Y) 'or' (('not' c) '&' a)) '&' ('not' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_4:5 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' ((('not' c) '&' a) '&' ('not' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:9 .= (((('not' c) '&' a) '&' ('not' c)) 'or' (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c)))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:8 .= (((('not' c) '&' a) '&' ('not' c)) 'or' (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c)))) 'or' (c 'or' (a 'or' b)) by BVFUNC_1:8 .= (((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' ((('not' c) '&' a) '&' ('not' c))) 'or' c) 'or' (a 'or' b) by BVFUNC_1:8 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (((('not' c) '&' a) '&' ('not' c)) 'or' c)) 'or' (a 'or' b) by BVFUNC_1:8 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (((('not' c) '&' a) 'or' c) '&' (('not' c) 'or' c))) 'or' (a 'or' b) by BVFUNC_1:11 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (((('not' c) '&' a) 'or' c) '&' (I_el Y))) 'or' (a 'or' b) by BVFUNC_4:6 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' ((('not' c) '&' a) 'or' c)) 'or' (a 'or' b) by BVFUNC_1:6 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' ((('not' c) 'or' c) '&' (a 'or' c))) 'or' (a 'or' b) by BVFUNC_1:11 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' ((I_el Y) '&' (a 'or' c))) 'or' (a 'or' b) by BVFUNC_4:6 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (a 'or' c)) 'or' (a 'or' b) by BVFUNC_1:6 .= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' ((b '&' ('not' c)) 'or' (c 'or' a))) 'or' (a 'or' b) by BVFUNC_1:8 .= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((b '&' ('not' c)) 'or' c) 'or' a)) 'or' (a 'or' b) by BVFUNC_1:8 .= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((b 'or' c) '&' (('not' c) 'or' c)) 'or' a)) 'or' (a 'or' b) by BVFUNC_1:11 .= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((b 'or' c) '&' (I_el Y)) 'or' a)) 'or' (a 'or' b) by BVFUNC_4:6 .= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' ((b 'or' c) 'or' a)) 'or' (a 'or' b) by BVFUNC_1:6 .= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b 'or' (c 'or' a))) 'or' (a 'or' b) by BVFUNC_1:8 .= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' b) 'or' (c 'or' a)) 'or' (a 'or' b) by BVFUNC_1:8 .= ((((('not' a) 'or' ('not' c)) 'or' b) '&' (('not' b) 'or' b)) 'or' (c 'or' a)) 'or' (a 'or' b) by BVFUNC_1:11 .= ((((('not' a) 'or' ('not' c)) 'or' b) '&' (I_el Y)) 'or' (c 'or' a)) 'or' (a 'or' b) by BVFUNC_4:6 .= (((('not' a) 'or' ('not' c)) 'or' b) 'or' (c 'or' a)) 'or' (a 'or' b) by BVFUNC_1:6 .= ((((('not' a) 'or' ('not' c)) 'or' b) 'or' c) 'or' a) 'or' (a 'or' b) by BVFUNC_1:8 .= ((((('not' a) 'or' ('not' c)) 'or' c) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_1:8 .= (((('not' a) 'or' (('not' c) 'or' c)) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_1:8 .= (((('not' a) 'or' (I_el Y)) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_4:6 .= (((I_el Y) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_1:10 .= ((I_el Y) 'or' a) 'or' (a 'or' b) by BVFUNC_1:10 .= (I_el Y) 'or' (a 'or' b) by BVFUNC_1:10 .= I_el Y by BVFUNC_1:10 ; hence ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c) by BVFUNC_1:16; ::_thesis: verum end;