YES

TRS:

  minus(n__0(),Y) -> 0()
  minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
  geq(X,n__0()) -> true()
  geq(n__0(),n__s(Y)) -> false()
  geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
  div(0(),n__s(Y)) -> 0()
  div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0())
  if(true(),X,Y) -> activate(X)
  if(false(),X,Y) -> activate(Y)
  0() -> n__0()
  s(X) -> n__s(X)
  activate(n__0()) -> 0()
  activate(n__s(X)) -> s(X)
  activate(X) -> X

linear polynomial interpretations on N:

  minus_A(x1,x2) = 0
  minus#_A(x1,x2) = x1 + x2 + 3
  n__0_A = 0
  n__0#_A = 1
  0_A = 0
  0#_A = 2
  n__s_A(x1) = x1 + 1
  n__s#_A(x1) = 3
  activate_A(x1) = x1
  activate#_A(x1) = x1 + 4
  geq_A(x1,x2) = x1 + 1
  geq#_A(x1,x2) = x1 + x2 + 3
  true_A = 1
  true#_A = 0
  false_A = 1
  false#_A = 0
  div_A(x1,x2) = x1 + 1
  div#_A(x1,x2) = x1 + x2 + 6
  s_A(x1) = x1 + 1
  s#_A(x1) = x1 + 4
  if_A(x1,x2,x3) = x2 + x3
  if#_A(x1,x2,x3) = x2 + x3 + 5

precedence:

  minus > div > geq = if > activate > s > n__s > 0 > n__0 > true = false