YES
Time: 0.050489
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:
  DP:
   {     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)}
  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)}
  UR:
   {   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,
            a(w, v) -> w,
            a(w, v) -> v}
   EDG:
    {(times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> plus#(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) -> times#(x, y))
     (div#(div(x, y), z) -> times#(y, z), times#(s x, y) -> plus#(y, times(x, y)))
     (quot#(s x, s y, z) -> quot#(x, y, z), 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#(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) -> times#(y, z))
     (quot#(x, 0(), s z) -> div#(x, s z), div#(div(x, y), z) -> div#(x, times(y, z)))
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> plus#(y, times(x, y)))
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> times#(x, y))
     (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) -> times#(y, 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), 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))}
    STATUS:
     arrows: 0.750000
     SCCS (3):
      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 (4):
       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)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [quot](x0, x1, x2) = 0,
         
         [plus](x0, x1) = x0 + x1 + 1,
         
         [times](x0, x1) = x0 + x1 + 1,
         
         [div](x0, x1) = x0,
         
         [s](x0) = x0 + 1,
         
         [0] = 1,
         
         [quot#](x0, x1, x2) = x0 + 1,
         
         [div#](x0, x1) = x0 + 1
        Strict:
         quot#(s x, s y, z) -> quot#(x, y, z)
         2 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z
         quot#(x, 0(), s z) -> div#(x, s z)
         1 + 1x + 0z >= 1 + 1x + 0z
         div#(div(x, y), z) -> div#(x, times(y, z))
         1 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z
         div#(x, y) -> quot#(x, y, y)
         1 + 1x + 0y >= 1 + 1x + 0y
        Weak:
         quot(s x, s y, z) -> quot(x, y, z)
         0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
         quot(0(), s y, z) -> 0()
         0 + 0y + 0z >= 1
         quot(x, 0(), s z) -> s div(x, s z)
         0 + 0x + 0z >= 1 + 1x + 0z
         div(div(x, y), z) -> div(x, times(y, z))
         0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z
         div(0(), y) -> 0()
         1 + 0y >= 1
         div(x, y) -> quot(x, y, y)
         0 + 1x + 0y >= 0 + 0x + 0y
         times(s 0(), y) -> y
         3 + 1y >= 1y
         times(s x, y) -> plus(y, times(x, y))
         2 + 1x + 1y >= 2 + 1x + 2y
         times(0(), y) -> 0()
         2 + 1y >= 1
         plus(s x, y) -> s plus(x, y)
         2 + 1x + 1y >= 2 + 1x + 1y
         plus(0(), y) -> y
         2 + 1y >= 1y
         plus(x, 0()) -> x
         2 + 1x >= 1x
       SCCS (1):
        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 (3):
         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)}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [quot](x0, x1, x2) = x0 + x1 + 1,
           
           [plus](x0, x1) = 0,
           
           [times](x0, x1) = x0 + 1,
           
           [div](x0, x1) = x0 + 1,
           
           [s](x0) = 0,
           
           [0] = 1,
           
           [quot#](x0, x1, x2) = x0,
           
           [div#](x0, x1) = x0
          Strict:
           quot#(x, 0(), s z) -> div#(x, s z)
           0 + 1x + 0z >= 0 + 1x + 0z
           div#(div(x, y), z) -> div#(x, times(y, z))
           1 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z
           div#(x, y) -> quot#(x, y, y)
           0 + 1x + 0y >= 0 + 1x + 0y
          Weak:
           quot(s x, s y, z) -> quot(x, y, z)
           1 + 0x + 0y + 1z >= 1 + 0x + 1y + 1z
           quot(0(), s y, z) -> 0()
           1 + 0y + 1z >= 1
           quot(x, 0(), s z) -> s div(x, s z)
           2 + 0x + 0z >= 0 + 0x + 0z
           div(div(x, y), z) -> div(x, times(y, z))
           2 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z
           div(0(), y) -> 0()
           2 + 0y >= 1
           div(x, y) -> quot(x, y, y)
           1 + 1x + 0y >= 1 + 0x + 2y
           times(s 0(), y) -> y
           1 + 0y >= 1y
           times(s x, y) -> plus(y, times(x, y))
           1 + 0x + 0y >= 0 + 0x + 0y
           times(0(), y) -> 0()
           2 + 0y >= 1
           plus(s x, y) -> s plus(x, y)
           0 + 0x + 0y >= 0 + 0x + 0y
           plus(0(), y) -> y
           0 + 0y >= 1y
           plus(x, 0()) -> x
           0 + 0x >= 1x
         SCCS (1):
          Scc:
           {        div#(x, y) -> quot#(x, y, y),
            quot#(x, 0(), s z) -> div#(x, s z)}
          
          SCC (2):
           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:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [quot](x0, x1, x2) = x0 + x1 + x2 + 1,
             
             [plus](x0, x1) = 0,
             
             [times](x0, x1) = x0 + 1,
             
             [div](x0, x1) = x0 + x1 + 1,
             
             [s](x0) = 0,
             
             [0] = 1,
             
             [quot#](x0, x1, x2) = x0 + 1,
             
             [div#](x0, x1) = x0 + 1
            Strict:
             quot#(x, 0(), s z) -> div#(x, s z)
             2 + 0x + 0z >= 1 + 0x + 0z
             div#(x, y) -> quot#(x, y, y)
             1 + 0x + 1y >= 1 + 0x + 1y
            Weak:
             quot(s x, s y, z) -> quot(x, y, z)
             1 + 0x + 0y + 1z >= 1 + 1x + 1y + 1z
             quot(0(), s y, z) -> 0()
             2 + 0y + 1z >= 1
             quot(x, 0(), s z) -> s div(x, s z)
             2 + 1x + 0z >= 0 + 0x + 0z
             div(div(x, y), z) -> div(x, times(y, z))
             2 + 1x + 1y + 1z >= 2 + 1x + 1y + 0z
             div(0(), y) -> 0()
             2 + 1y >= 1
             div(x, y) -> quot(x, y, y)
             1 + 1x + 1y >= 1 + 1x + 2y
             times(s 0(), y) -> y
             1 + 0y >= 1y
             times(s x, y) -> plus(y, times(x, y))
             1 + 0x + 0y >= 0 + 0x + 0y
             times(0(), y) -> 0()
             2 + 0y >= 1
             plus(s x, y) -> s plus(x, y)
             0 + 0x + 0y >= 0 + 0x + 0y
             plus(0(), y) -> y
             0 + 0y >= 1y
             plus(x, 0()) -> x
             0 + 0x >= 1x
           SCCS (0):
            
            
    
    SCC (1):
     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)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [quot](x0, x1, x2) = x0 + x1 + x2,
       
       [plus](x0, x1) = x0 + x1 + 1,
       
       [times](x0, x1) = x0 + x1 + 1,
       
       [div](x0, x1) = x0 + x1 + 1,
       
       [s](x0) = x0 + 1,
       
       [0] = 1,
       
       [times#](x0, x1) = x0 + 1
      Strict:
       times#(s x, y) -> times#(x, y)
       2 + 1x + 0y >= 1 + 1x + 0y
      Weak:
       quot(s x, s y, z) -> quot(x, y, z)
       2 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
       quot(0(), s y, z) -> 0()
       2 + 1y + 1z >= 1
       quot(x, 0(), s z) -> s div(x, s z)
       2 + 1x + 1z >= 3 + 1x + 1z
       div(div(x, y), z) -> div(x, times(y, z))
       2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z
       div(0(), y) -> 0()
       2 + 1y >= 1
       div(x, y) -> quot(x, y, y)
       1 + 1x + 1y >= 0 + 1x + 2y
       times(s 0(), y) -> y
       3 + 1y >= 1y
       times(s x, y) -> plus(y, times(x, y))
       2 + 1x + 1y >= 2 + 1x + 2y
       times(0(), y) -> 0()
       2 + 1y >= 1
       plus(s x, y) -> s plus(x, y)
       2 + 1x + 1y >= 2 + 1x + 1y
       plus(0(), y) -> y
       2 + 1y >= 1y
       plus(x, 0()) -> x
       2 + 1x >= 1x
     Qed
    
    SCC (1):
     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)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [quot](x0, x1, x2) = x0 + x1 + x2,
       
       [plus](x0, x1) = x0 + x1 + 1,
       
       [times](x0, x1) = x0 + x1 + 1,
       
       [div](x0, x1) = x0 + x1 + 1,
       
       [s](x0) = x0 + 1,
       
       [0] = 1,
       
       [plus#](x0, x1) = x0 + 1
      Strict:
       plus#(s x, y) -> plus#(x, y)
       2 + 1x + 0y >= 1 + 1x + 0y
      Weak:
       quot(s x, s y, z) -> quot(x, y, z)
       2 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
       quot(0(), s y, z) -> 0()
       2 + 1y + 1z >= 1
       quot(x, 0(), s z) -> s div(x, s z)
       2 + 1x + 1z >= 3 + 1x + 1z
       div(div(x, y), z) -> div(x, times(y, z))
       2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z
       div(0(), y) -> 0()
       2 + 1y >= 1
       div(x, y) -> quot(x, y, y)
       1 + 1x + 1y >= 0 + 1x + 2y
       times(s 0(), y) -> y
       3 + 1y >= 1y
       times(s x, y) -> plus(y, times(x, y))
       2 + 1x + 1y >= 2 + 1x + 2y
       times(0(), y) -> 0()
       2 + 1y >= 1
       plus(s x, y) -> s plus(x, y)
       2 + 1x + 1y >= 2 + 1x + 1y
       plus(0(), y) -> y
       2 + 1y >= 1y
       plus(x, 0()) -> x
       2 + 1x >= 1x
     Qed