YES

TRS:

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

linear polynomial interpretations on N:

  minus_A(x1,x2) = 1
  minus#_A(x1,x2) = 0
  0_A = 1
  0#_A = 2
  s_A(x1) = 2
  s#_A(x1) = 3
  geq_A(x1,x2) = 1
  geq#_A(x1,x2) = 1
  true_A = 1
  true#_A = 0
  false_A = 1
  false#_A = 0
  div_A(x1,x2) = x1 + x2
  div#_A(x1,x2) = x1 + x2
  if_A(x1,x2,x3) = x2 + x3
  if#_A(x1,x2,x3) = x2

precedence:

  div = if > s > 0 = geq > minus = true = false