; NOT ((x + y + (2^32-1))[0]) = (x + y)[0]

(= {bitsel {bitplus [bitvec 32 x] [bitvec 32 y]} 0 0}
   {bitnot {bitsel {bitplus x y -1 {bitconst 1}} 0 0}})