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)))

max/plus interpretations on N:

  le_A(x1,x2) = max{2, 1, 1 + x2}
  le#_A(x1,x2) = max{6, -3, 11}
  0_A = 6
  0#_A = 11
  true_A = 2
  true#_A = 7
  s_A(x1) = max{3, 9 + x1}
  s#_A(x1) = max{6, 4}
  false_A = 3
  false#_A = 5
  minus_A(x1,x2) = max{0, x1, -10}
  minus#_A(x1,x2) = max{0, 2 + x1, -2}
  ifMinus_A(x1,x2,x3) = max{4, -10, x2, -10}
  ifMinus#_A(x1,x2,x3) = max{1, -1, -6 + x2, 11}
  quot_A(x1,x2) = max{0, 1 + x1, -9}
  quot#_A(x1,x2) = max{7, 6 + x1, 8}

precedence:

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