(bvxnor s t) abbreviates (bvor (bvand s t) (bvand (bvnot s) (bvnot t)))