YES
Time: 0.009138
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:
  DP:
   {       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)}
  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)}
  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 (3):
    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 (1):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [plus](x0, x1) = 0,
       
       [min](x0, x1) = x0,
       
       [quot](x0, x1) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [0] = 0,
       
       [Z] = 0,
       
       [quot#](x0, x1) = x0 + 1
      Strict:
       quot#(s X, s Y) -> quot#(min(X, Y), s Y)
       2 + 0Y + 1X >= 1 + 0Y + 1X
      Weak:
       
     Qed
   SCC (2):
    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 (1):
       Scc:
        {min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))}
       SCC (1):
        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 (1):
    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