(=>
  (or
   (= [bitvec 1 y] {bitconst 0})
   (= y {bitconst 1}))

(=
 {bitsel {bitplus @32 {bitcat [bitvec 1 y] [bitvec 30 x]} {bitconst 1}} 31 31}
 {bitsel {bitplus @31 x y} 30 30}))