YES
TRS:
 {       plus(x, 0()) -> x,
         plus(0(), y) -> y,
        plus(s(x), y) -> s(plus(x, y)),
        times(0(), y) -> 0(),
       times(s(x), y) -> plus(y, times(x, y)),
     times(s(0()), y) -> y,
            div(x, y) -> quot(x, y, y),
          div(0(), y) -> 0(),
    div(div(x, y), z) -> div(x, times(y, z)),
   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:
   {      plus#(s(x), y) -> plus#(x, y),
         times#(s(x), y) -> plus#(y, times(x, y)),
         times#(s(x), y) -> times#(x, y),
              div#(x, y) -> quot#(x, y, y),
      div#(div(x, y), z) -> times#(y, z),
      div#(div(x, y), z) -> div#(x, times(y, z)),
     quot#(x, 0(), s(z)) -> div#(x, s(z)),
    quot#(s(x), s(y), z) -> quot#(x, y, z)}
  Weak:
  {       plus(x, 0()) -> x,
          plus(0(), y) -> y,
         plus(s(x), y) -> s(plus(x, y)),
         times(0(), y) -> 0(),
        times(s(x), y) -> plus(y, times(x, y)),
      times(s(0()), y) -> y,
             div(x, y) -> quot(x, y, y),
           div(0(), y) -> 0(),
     div(div(x, y), z) -> div(x, times(y, z)),
    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:
   {(times#(s(x), y) -> plus#(y, times(x, y)), plus#(s(x), y) -> plus#(x, y))
    (div#(div(x, y), z) -> div#(x, times(y, z)), div#(div(x, y), z) -> div#(x, times(y, z)))
    (div#(div(x, y), z) -> div#(x, times(y, z)), div#(div(x, y), z) -> times#(y, z))
    (div#(div(x, y), z) -> div#(x, times(y, z)), div#(x, y) -> quot#(x, y, y))
    (quot#(x, 0(), s(z)) -> div#(x, s(z)), div#(div(x, y), z) -> div#(x, times(y, z)))
    (quot#(x, 0(), s(z)) -> div#(x, s(z)), div#(div(x, y), z) -> times#(y, z))
    (quot#(x, 0(), s(z)) -> div#(x, s(z)), div#(x, y) -> quot#(x, y, y))
    (times#(s(x), y) -> times#(x, y), times#(s(x), y) -> times#(x, y))
    (times#(s(x), y) -> times#(x, y), times#(s(x), y) -> plus#(y, times(x, y)))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
    (div#(div(x, y), z) -> times#(y, z), times#(s(x), y) -> plus#(y, times(x, y)))
    (div#(div(x, y), z) -> times#(y, z), times#(s(x), y) -> times#(x, y))
    (div#(x, y) -> quot#(x, y, y), 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#(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),
        div#(div(x, y), z) -> div#(x, times(y, z)),
       quot#(x, 0(), s(z)) -> div#(x, s(z)),
      quot#(s(x), s(y), z) -> quot#(x, y, z)}
    Scc:
     {times#(s(x), y) -> times#(x, y)}
    Scc:
     {plus#(s(x), y) -> plus#(x, y)}
    SCC:
     Strict:
      {          div#(x, y) -> quot#(x, y, y),
         div#(div(x, y), z) -> div#(x, times(y, z)),
        quot#(x, 0(), s(z)) -> div#(x, s(z)),
       quot#(s(x), s(y), z) -> quot#(x, y, z)}
     Weak:
     {       plus(x, 0()) -> x,
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            times(0(), y) -> 0(),
           times(s(x), y) -> plus(y, times(x, y)),
         times(s(0()), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
       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),
         div#(div(x, y), z) -> div#(x, times(y, z)),
        quot#(x, 0(), s(z)) -> div#(x, s(z))}
      EDG:
       {(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#(x, 0(), s(z)) -> div#(x, s(z)), div#(div(x, y), z) -> div#(x, times(y, z)))
        (div#(div(x, y), z) -> div#(x, times(y, z)), div#(x, y) -> quot#(x, y, y))
        (div#(div(x, y), z) -> div#(x, times(y, z)), div#(div(x, y), z) -> div#(x, times(y, z)))}
       SCCS:
        Scc:
         {         div#(x, y) -> quot#(x, y, y),
           div#(div(x, y), z) -> div#(x, times(y, z)),
          quot#(x, 0(), s(z)) -> div#(x, s(z))}
        SCC:
         Strict:
          {         div#(x, y) -> quot#(x, y, y),
            div#(div(x, y), z) -> div#(x, times(y, z)),
           quot#(x, 0(), s(z)) -> div#(x, s(z))}
         Weak:
         {       plus(x, 0()) -> x,
                 plus(0(), y) -> y,
                plus(s(x), y) -> s(plus(x, y)),
                times(0(), y) -> 0(),
               times(s(x), y) -> plus(y, times(x, y)),
             times(s(0()), y) -> y,
                    div(x, y) -> quot(x, y, y),
                  div(0(), y) -> 0(),
            div(div(x, y), z) -> div(x, times(y, z)),
           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:
             {       plus(x, 0()) -> x,
                     plus(0(), y) -> y,
                    plus(s(x), y) -> s(plus(x, y)),
                    times(0(), y) -> 0(),
                   times(s(x), y) -> plus(y, times(x, y)),
                 times(s(0()), y) -> y,
                        div(x, y) -> quot(x, y, y),
                      div(0(), y) -> 0(),
                div(div(x, y), z) -> div(x, times(y, z)),
               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(quot#) = 1, pi(quot) = [], pi(div#) = 1, pi(div) = [], pi(times) = [], pi(s) = [], pi(0) = [], pi(plus) = []
              Usable Rules:
               {}
              Interpretation:
               [s] = 0,
               [0] = 1
              Strict:
               {div#(x, y) -> quot#(x, y, y)}
              Weak:
               {       plus(x, 0()) -> x,
                       plus(0(), y) -> y,
                      plus(s(x), y) -> s(plus(x, y)),
                      times(0(), y) -> 0(),
                     times(s(x), y) -> plus(y, times(x, y)),
                   times(s(0()), y) -> y,
                          div(x, y) -> quot(x, y, y),
                        div(0(), y) -> 0(),
                  div(div(x, y), z) -> div(x, times(y, z)),
                 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
    SCC:
     Strict:
      {times#(s(x), y) -> times#(x, y)}
     Weak:
     {       plus(x, 0()) -> x,
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            times(0(), y) -> 0(),
           times(s(x), y) -> plus(y, times(x, y)),
         times(s(0()), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
       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(times#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {plus#(s(x), y) -> plus#(x, y)}
     Weak:
     {       plus(x, 0()) -> x,
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            times(0(), y) -> 0(),
           times(s(x), y) -> plus(y, times(x, y)),
         times(s(0()), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
       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(plus#) = 0
      Strict:
       {}
      Qed