YES
TRS:
 {   quot(x, 0(), s(z)) -> s(quot(x, plus(z, s(0())), s(z))),
  quot(0(), s(y), s(z)) -> 0(),
    quot(s(x), s(y), z) -> quot(x, y, z),
           plus(0(), y) -> y,
          plus(s(x), y) -> s(plus(x, y))}
 DP:
  Strict:
   { quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z)),
     quot#(x, 0(), s(z)) -> plus#(z, s(0())),
    quot#(s(x), s(y), z) -> quot#(x, y, z),
          plus#(s(x), y) -> plus#(x, y)}
  Weak:
  {   quot(x, 0(), s(z)) -> s(quot(x, plus(z, s(0())), s(z))),
   quot(0(), s(y), s(z)) -> 0(),
     quot(s(x), s(y), z) -> quot(x, y, z),
            plus(0(), y) -> y,
           plus(s(x), y) -> s(plus(x, y))}
  EDG:
   {(plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
    (quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z)), quot#(s(x), s(y), z) -> quot#(x, y, z))
    (quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z)), quot#(x, 0(), s(z)) -> plus#(z, s(0())))
    (quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z)), quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z)))
    (quot#(s(x), s(y), z) -> quot#(x, y, z), quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z)))
    (quot#(s(x), s(y), z) -> quot#(x, y, z), quot#(x, 0(), s(z)) -> plus#(z, s(0())))
    (quot#(s(x), s(y), z) -> quot#(x, y, z), quot#(s(x), s(y), z) -> quot#(x, y, z))
    (quot#(x, 0(), s(z)) -> plus#(z, s(0())), plus#(s(x), y) -> plus#(x, y))}
   SCCS:
    Scc:
     {plus#(s(x), y) -> plus#(x, y)}
    Scc:
     { quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z)),
      quot#(s(x), s(y), z) -> quot#(x, y, z)}
    SCC:
     Strict:
      {plus#(s(x), y) -> plus#(x, y)}
     Weak:
     {   quot(x, 0(), s(z)) -> s(quot(x, plus(z, s(0())), s(z))),
      quot(0(), s(y), s(z)) -> 0(),
        quot(s(x), s(y), z) -> quot(x, y, z),
               plus(0(), y) -> y,
              plus(s(x), y) -> s(plus(x, y))}
     SPSC:
      Simple Projection:
       pi(plus#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      { quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z)),
       quot#(s(x), s(y), z) -> quot#(x, y, z)}
     Weak:
     {   quot(x, 0(), s(z)) -> s(quot(x, plus(z, s(0())), s(z))),
      quot(0(), s(y), s(z)) -> 0(),
        quot(s(x), s(y), z) -> quot(x, y, z),
               plus(0(), y) -> y,
              plus(s(x), y) -> s(plus(x, y))}
     SPSC:
      Simple Projection:
       pi(quot#) = 0
      Strict:
       {quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z))}
      EDG:
       {(quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z)), quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z)))}
       SCCS:
        Scc:
         {quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z))}
        SCC:
         Strict:
          {quot#(x, 0(), s(z)) -> quot#(x, plus(z, s(0())), s(z))}
         Weak:
         {   quot(x, 0(), s(z)) -> s(quot(x, plus(z, s(0())), s(z))),
          quot(0(), s(y), s(z)) -> 0(),
            quot(s(x), s(y), z) -> quot(x, y, z),
                   plus(0(), y) -> y,
                  plus(s(x), y) -> s(plus(x, y))}
         POLY:
          Argument Filtering:
           pi(plus) = 1, pi(s) = [], pi(quot#) = 1, pi(quot) = [], pi(0) = []
          Usable Rules:
           {}
          Interpretation:
           [s] = 0,
           [0] = 1
          Strict:
           {}
          Weak:
           {   quot(x, 0(), s(z)) -> s(quot(x, plus(z, s(0())), s(z))),
            quot(0(), s(y), s(z)) -> 0(),
              quot(s(x), s(y), z) -> quot(x, y, z),
                     plus(0(), y) -> y,
                    plus(s(x), y) -> s(plus(x, y))}
          Qed