YES

TRS:

  plus(0(),Y) -> Y
  plus(s(X),Y) -> s(plus(X,Y))
  min(X,0()) -> X
  min(s(X),s(Y)) -> min(X,Y)
  min(min(X,Y),Z()) -> min(X,plus(Y,Z()))
  quot(0(),s(Y)) -> 0()
  quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))

linear polynomial interpretations on N:

  plus_A(x1,x2) = x1 + x2 + 1
  plus#_A(x1,x2) = x2 + 2
  0_A = 1
  0#_A = 0
  s_A(x1) = x1 + 1
  s#_A(x1) = 1
  min_A(x1,x2) = x1
  min#_A(x1,x2) = 4
  Z_A = 1
  Z#_A = 0
  quot_A(x1,x2) = x1 + 1
  quot#_A(x1,x2) = x1 + x2 + 3

precedence:

  quot > min > plus = Z > s > 0