YES

TRS:

  le(0(),Y) -> true()
  le(s(X),0()) -> false()
  le(s(X),s(Y)) -> le(X,Y)
  minus(0(),Y) -> 0()
  minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
  ifMinus(true(),s(X),Y) -> 0()
  ifMinus(false(),s(X),Y) -> s(minus(X,Y))
  quot(0(),s(Y)) -> 0()
  quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))

linear polynomial interpretations on N:

  le_A(x1,x2) = 1
  le#_A(x1,x2) = x1 + x2
  0_A = 1
  0#_A = 8
  true_A = 1
  true#_A = 0
  s_A(x1) = x1 + 4
  s#_A(x1) = 7
  false_A = 1
  false#_A = 6
  minus_A(x1,x2) = x1
  minus#_A(x1,x2) = x1 + x2 + 6
  ifMinus_A(x1,x2,x3) = x2
  ifMinus#_A(x1,x2,x3) = x2 + x3 + 5
  quot_A(x1,x2) = x1 + x2
  quot#_A(x1,x2) = x1 + x2 + 4

precedence:

  ifMinus = quot > le = 0 > true = false = minus > s