(bvnor s t) abbreviates (bvnot (bvor s t))