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