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 Th16
.= (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' c)) 'or' (((('not' a) '&' b) '&' ('not' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) by BVFUNC_1:12
.= (((a '&' b) '&' c) 'or' (((a '&' ('not' b)) '&' ('not' c)) 'or' ((('not' a) '&' b) '&' ('not' c)))) 'or' ((('not' a) '&' ('not' b)) '&' c) by BVFUNC_1:8
.= ((((a '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' ('not' c))) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' ((('not' a) '&' ('not' b)) '&' c) by BVFUNC_1:8 ;
a 'xor' (b 'xor' c) = (('not' a) '&' (b 'xor' c)) 'or' (a '&' ('not' (b 'xor' c))) by BVFUNC_4:9
.= (('not' a) '&' ((('not' b) '&' c) 'or' (b '&' ('not' c)))) 'or' (a '&' ('not' (b 'xor' c))) by BVFUNC_4:9
.= (('not' a) '&' ((('not' b) '&' c) 'or' (b '&' ('not' c)))) 'or' (a '&' ('not' ((('not' b) '&' c) 'or' (b '&' ('not' c))))) by BVFUNC_4:9
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ('not' ((('not' b) '&' c) 'or' (b '&' ('not' c))))) by BVFUNC_1:12
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' (('not' (('not' b) '&' c)) '&' ('not' (b '&' ('not' c))))) by BVFUNC_1:13
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ((('not' ('not' b)) 'or' ('not' c)) '&' ('not' (b '&' ('not' c))))) by BVFUNC_1:14
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ((b 'or' ('not' c)) '&' (('not' b) 'or' ('not' ('not' c))))) by BVFUNC_1:14
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ((b '&' c) 'or' (('not' b) '&' ('not' c)))) by Th16
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:12
.= (((('not' a) '&' ('not' b)) '&' c) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:4
.= (((('not' a) '&' ('not' b)) '&' c) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:4
.= (((('not' a) '&' ('not' b)) '&' c) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' (((a '&' b) '&' c) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:4
.= (((a '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' ('not' c))) 'or' (((('not' a) '&' b) '&' ('not' c)) 'or' ((('not' a) '&' ('not' b)) '&' c)) by BVFUNC_1:4
.= ((((a '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' ('not' c))) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' ((('not' a) '&' ('not' b)) '&' c) by BVFUNC_1:8 ;
hence a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c by A1; :: thesis: verum