YES
Time: 0.099955
TRS:
 {       D t() -> 1(),
  D constant() -> 0(),
     D +(x, y) -> +(D x, D y),
     D *(x, y) -> +(*(y, D x), *(x, D y)),
     D -(x, y) -> -(D x, D y)}
 DP:
  DP:
   {D# +(x, y) -> D# x,
    D# +(x, y) -> D# y,
    D# *(x, y) -> D# x,
    D# *(x, y) -> D# y,
    D# -(x, y) -> D# x,
    D# -(x, y) -> D# y}
  TRS:
  {       D t() -> 1(),
   D constant() -> 0(),
      D +(x, y) -> +(D x, D y),
      D *(x, y) -> +(*(y, D x), *(x, D y)),
      D -(x, y) -> -(D x, D y)}
  UR:
   {}
   EDG:
    {(D# *(x, y) -> D# y, D# -(x, y) -> D# y)
     (D# *(x, y) -> D# y, D# -(x, y) -> D# x)
     (D# *(x, y) -> D# y, D# *(x, y) -> D# y)
     (D# *(x, y) -> D# y, D# *(x, y) -> D# x)
     (D# *(x, y) -> D# y, D# +(x, y) -> D# y)
     (D# *(x, y) -> D# y, D# +(x, y) -> D# x)
     (D# +(x, y) -> D# x, D# -(x, y) -> D# y)
     (D# +(x, y) -> D# x, D# -(x, y) -> D# x)
     (D# +(x, y) -> D# x, D# *(x, y) -> D# y)
     (D# +(x, y) -> D# x, D# *(x, y) -> D# x)
     (D# +(x, y) -> D# x, D# +(x, y) -> D# y)
     (D# +(x, y) -> D# x, D# +(x, y) -> D# x)
     (D# -(x, y) -> D# x, D# -(x, y) -> D# y)
     (D# -(x, y) -> D# x, D# -(x, y) -> D# x)
     (D# -(x, y) -> D# x, D# *(x, y) -> D# y)
     (D# -(x, y) -> D# x, D# *(x, y) -> D# x)
     (D# -(x, y) -> D# x, D# +(x, y) -> D# y)
     (D# -(x, y) -> D# x, D# +(x, y) -> D# x)
     (D# *(x, y) -> D# x, D# +(x, y) -> D# x)
     (D# *(x, y) -> D# x, D# +(x, y) -> D# y)
     (D# *(x, y) -> D# x, D# *(x, y) -> D# x)
     (D# *(x, y) -> D# x, D# *(x, y) -> D# y)
     (D# *(x, y) -> D# x, D# -(x, y) -> D# x)
     (D# *(x, y) -> D# x, D# -(x, y) -> D# y)
     (D# -(x, y) -> D# y, D# +(x, y) -> D# x)
     (D# -(x, y) -> D# y, D# +(x, y) -> D# y)
     (D# -(x, y) -> D# y, D# *(x, y) -> D# x)
     (D# -(x, y) -> D# y, D# *(x, y) -> D# y)
     (D# -(x, y) -> D# y, D# -(x, y) -> D# x)
     (D# -(x, y) -> D# y, D# -(x, y) -> D# y)
     (D# +(x, y) -> D# y, D# +(x, y) -> D# x)
     (D# +(x, y) -> D# y, D# +(x, y) -> D# y)
     (D# +(x, y) -> D# y, D# *(x, y) -> D# x)
     (D# +(x, y) -> D# y, D# *(x, y) -> D# y)
     (D# +(x, y) -> D# y, D# -(x, y) -> D# x)
     (D# +(x, y) -> D# y, D# -(x, y) -> D# y)}
    STATUS:
     arrows: 0.000000
     SCCS (1):
      Scc:
       {D# +(x, y) -> D# x,
        D# +(x, y) -> D# y,
        D# *(x, y) -> D# x,
        D# *(x, y) -> D# y,
        D# -(x, y) -> D# x,
        D# -(x, y) -> D# y}
      
      SCC (6):
       Strict:
        {D# +(x, y) -> D# x,
         D# +(x, y) -> D# y,
         D# *(x, y) -> D# x,
         D# *(x, y) -> D# y,
         D# -(x, y) -> D# x,
         D# -(x, y) -> D# y}
       Weak:
       {       D t() -> 1(),
        D constant() -> 0(),
           D +(x, y) -> +(D x, D y),
           D *(x, y) -> +(*(y, D x), *(x, D y)),
           D -(x, y) -> -(D x, D y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [+](x0, x1) = x0 + x1,
         
         [*](x0, x1) = x0 + x1 + 1,
         
         [-](x0, x1) = x0 + x1,
         
         [D](x0) = x0,
         
         [1] = 0,
         
         [t] = 0,
         
         [0] = 0,
         
         [constant] = 0,
         
         [D#](x0) = x0
        Strict:
         D# -(x, y) -> D# y
         0 + 1x + 1y >= 0 + 1y
         D# -(x, y) -> D# x
         0 + 1x + 1y >= 0 + 1x
         D# *(x, y) -> D# y
         1 + 1x + 1y >= 0 + 1y
         D# *(x, y) -> D# x
         1 + 1x + 1y >= 0 + 1x
         D# +(x, y) -> D# y
         0 + 1x + 1y >= 0 + 1y
         D# +(x, y) -> D# x
         0 + 1x + 1y >= 0 + 1x
        Weak:
         D -(x, y) -> -(D x, D y)
         0 + 1x + 1y >= 0 + 1x + 1y
         D *(x, y) -> +(*(y, D x), *(x, D y))
         1 + 1x + 1y >= 2 + 2x + 2y
         D +(x, y) -> +(D x, D y)
         0 + 1x + 1y >= 0 + 1x + 1y
         D constant() -> 0()
         0 >= 0
         D t() -> 1()
         0 >= 0
       SCCS (1):
        Scc:
         {D# +(x, y) -> D# x,
          D# +(x, y) -> D# y,
          D# -(x, y) -> D# x,
          D# -(x, y) -> D# y}
        
        SCC (4):
         Strict:
          {D# +(x, y) -> D# x,
           D# +(x, y) -> D# y,
           D# -(x, y) -> D# x,
           D# -(x, y) -> D# y}
         Weak:
         {       D t() -> 1(),
          D constant() -> 0(),
             D +(x, y) -> +(D x, D y),
             D *(x, y) -> +(*(y, D x), *(x, D y)),
             D -(x, y) -> -(D x, D y)}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [+](x0, x1) = x0 + x1 + 1,
           
           [*](x0, x1) = 1,
           
           [-](x0, x1) = x0 + x1,
           
           [D](x0) = 0,
           
           [1] = 0,
           
           [t] = 0,
           
           [0] = 0,
           
           [constant] = 0,
           
           [D#](x0) = x0
          Strict:
           D# -(x, y) -> D# y
           0 + 1x + 1y >= 0 + 1y
           D# -(x, y) -> D# x
           0 + 1x + 1y >= 0 + 1x
           D# +(x, y) -> D# y
           1 + 1x + 1y >= 0 + 1y
           D# +(x, y) -> D# x
           1 + 1x + 1y >= 0 + 1x
          Weak:
           D -(x, y) -> -(D x, D y)
           0 + 0x + 0y >= 0 + 0x + 0y
           D *(x, y) -> +(*(y, D x), *(x, D y))
           0 + 0x + 0y >= 3 + 0x + 0y
           D +(x, y) -> +(D x, D y)
           0 + 0x + 0y >= 1 + 0x + 0y
           D constant() -> 0()
           0 >= 0
           D t() -> 1()
           0 >= 0
         SCCS (1):
          Scc:
           {D# -(x, y) -> D# x,
            D# -(x, y) -> D# y}
          
          SCC (2):
           Strict:
            {D# -(x, y) -> D# x,
             D# -(x, y) -> D# y}
           Weak:
           {       D t() -> 1(),
            D constant() -> 0(),
               D +(x, y) -> +(D x, D y),
               D *(x, y) -> +(*(y, D x), *(x, D y)),
               D -(x, y) -> -(D x, D y)}
           POLY:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [+](x0, x1) = 0,
             
             [*](x0, x1) = 0,
             
             [-](x0, x1) = x0 + x1 + 1,
             
             [D](x0) = 0,
             
             [1] = 0,
             
             [t] = 0,
             
             [0] = 0,
             
             [constant] = 0,
             
             [D#](x0) = x0
            Strict:
             D# -(x, y) -> D# y
             1 + 1x + 1y >= 0 + 1y
             D# -(x, y) -> D# x
             1 + 1x + 1y >= 0 + 1x
            Weak:
             D -(x, y) -> -(D x, D y)
             0 + 0x + 0y >= 1 + 0x + 0y
             D *(x, y) -> +(*(y, D x), *(x, D y))
             0 + 0x + 0y >= 0 + 0x + 0y
             D +(x, y) -> +(D x, D y)
             0 + 0x + 0y >= 0 + 0x + 0y
             D constant() -> 0()
             0 >= 0
             D t() -> 1()
             0 >= 0
           Qed