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)))}
 DP:
  Strict:
   {      plus#(s(X), Y) -> plus#(X, Y),
        min#(s(X), s(Y)) -> min#(X, Y),
    min#(min(X, Y), Z()) -> plus#(Y, Z()),
    min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())),
       quot#(s(X), s(Y)) -> min#(X, Y),
       quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y))}
  Weak:
  {       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)))}
  EDG:
   {(min#(s(X), s(Y)) -> min#(X, Y), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())))
    (min#(s(X), s(Y)) -> min#(X, Y), min#(min(X, Y), Z()) -> plus#(Y, Z()))
    (min#(s(X), s(Y)) -> min#(X, Y), min#(s(X), s(Y)) -> min#(X, Y))
    (quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y)), quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y)))
    (quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y)), quot#(s(X), s(Y)) -> min#(X, Y))
    (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())))
    (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(min(X, Y), Z()) -> plus#(Y, Z()))
    (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(s(X), s(Y)) -> min#(X, Y))
    (min#(min(X, Y), Z()) -> plus#(Y, Z()), plus#(s(X), Y) -> plus#(X, Y))
    (quot#(s(X), s(Y)) -> min#(X, Y), min#(s(X), s(Y)) -> min#(X, Y))
    (quot#(s(X), s(Y)) -> min#(X, Y), min#(min(X, Y), Z()) -> plus#(Y, Z()))
    (quot#(s(X), s(Y)) -> min#(X, Y), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())))
    (plus#(s(X), Y) -> plus#(X, Y), plus#(s(X), Y) -> plus#(X, Y))}
   SCCS:
    Scc:
     {quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y))}
    Scc:
     {    min#(s(X), s(Y)) -> min#(X, Y),
      min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))}
    Scc:
     {plus#(s(X), Y) -> plus#(X, Y)}
    SCC:
     Strict:
      {quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y))}
     Weak:
     {       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)))}
     POLY:
      Argument Filtering:
       pi(quot#) = 0, pi(quot) = [], pi(Z) = [], pi(min) = 0, pi(s) = [0], pi(0) = [], pi(plus) = []
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {       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)))}
      Qed
    SCC:
     Strict:
      {    min#(s(X), s(Y)) -> min#(X, Y),
       min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))}
     Weak:
     {       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)))}
     SPSC:
      Simple Projection:
       pi(min#) = 0
      Strict:
       {min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))}
      EDG:
       {(min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())))}
       SCCS:
        Scc:
         {min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))}
        SCC:
         Strict:
          {min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))}
         Weak:
         {       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)))}
         SPSC:
          Simple Projection:
           pi(min#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {plus#(s(X), Y) -> plus#(X, Y)}
     Weak:
     {       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)))}
     SPSC:
      Simple Projection:
       pi(plus#) = 0
      Strict:
       {}
      Qed