(bvnand s t) abbreviates (bvnot (bvand s t))