YES

(VAR u x v y)
(RULES
  subset(+(u,x),v) -> if(has(v,x),subset(u,v),ff())
  subset(empty(),v) -> tt()
  has(+(u,x),y) -> if(eq(x,y),tt(),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()
  eq(0(),0()) -> tt()
  if(x,tt(),ff()) -> x
  if(x,y,y) -> y
  if(ff(),x,y) -> y
  if(tt(),x,y) -> x
)

(COMMENT
Termination is shown by ELPO with interpretations on natural numbers

  if_A(x1,x2,x3) = x1 + x2 + x3
  tt_A = 0
  ff_A = 0
  eq_A(x1,x2) = 0
  0_A = 1
  s_A(x1) = x1 + 18814
  has_A(x1,x2) = 0
  empty_A = 3
  +_A(x1,x2) = 1
  subset_A(x1,x2) = 0
  if#_A(x1,x2,x3) = x1 + x2 + x3
  tt#_A = 0
  ff#_A = 0
  0#_A = 0
  s#_A(x1) = 0
  empty#_A = 0

and precedence:

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