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 ELPO with interpretations on natural numbers

  if_A(x1,x2,x3) = x1 + x2 + x3
  tt_A = 2
  ff_A = 0
  eq_A(x1,x2) = 0
  0_A = 1
  s_A(x1) = x1 + 1
  has_A(x1,x2) = 1
  empty_A = 0
  +_A(x1,x2) = x1 + 1
  subset_A(x1,x2) = x1 + x2 + 1
  if#_A(x1,x2,x3) = x1 + x2 + x3
  tt#_A = 0
  ff#_A = 0
  eq#_A(x1,x2) = x1
  0#_A = 0
  has#_A(x1,x2) = x1
  empty#_A = 0
  +#_A(x1,x2) = x1 + x2
  subset#_A(x1,x2) = x1

and precedence:

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