YES

TRS:

  minus(X,0()) -> X
  minus(s(X),s(Y)) -> p(minus(X,Y))
  p(s(X)) -> X
  div(0(),s(Y)) -> 0()
  div(s(X),s(Y)) -> s(div(minus(X,Y),s(Y)))

linear polynomial interpretations on N:

  minus_A(x1,x2) = x1
  minus#_A(x1,x2) = 1
  0_A = 1
  0#_A = 6
  s_A(x1) = x1 + 4
  s#_A(x1) = 7
  p_A(x1) = x1
  p#_A(x1) = 0
  div_A(x1,x2) = x1 + 1
  div#_A(x1,x2) = x1 + x2

precedence:

  div > minus = s = p > 0