YES

(VAR u x v y)
(RULES
  subset(+(u,x),v) -> if(has(v,x),subset(u,v),ff())
  subset(empty(),v) -> eq(0(),0())
  has(+(u,x),y) -> if(eq(x,y),eq(0(),0()),has(u,y))
  has(empty(),x) -> ff()
  eq(s(x),s(y)) -> eq(x,y)
  eq(s(x),0()) -> ff()
  eq(0(),s(x)) -> ff()
  if(eq(0(),0()),x,y) -> x
  if(x,eq(0(),0()),ff()) -> x
  tt() -> eq(0(),0())
  if(x,y,y) -> y
  if(ff(),x,y) -> y
)

(COMMENT
Termination is shown by LPO with precedence:

  subset > tt > has > if > s > empty > eq > 0 > ff > +
)