YES
Time: 0.004495
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)}
  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)}
   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)}
     SPSC:
      Simple Projection:
       pi(D#) = 0
      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# y}
      EDG:
       {(D# *(x, y) -> D# y, D# -(x, y) -> D# y)
        (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# 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# 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# 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# y)}
       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# y}
        SCC (5):
         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# 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)}
         SPSC:
          Simple Projection:
           pi(D#) = 0
          Strict:
           {D# +(x, y) -> D# x,
            D# +(x, y) -> D# y,
            D# *(x, y) -> D# x,
            D# -(x, y) -> D# y}
          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# 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# 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)}
           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)}
             SPSC:
              Simple Projection:
               pi(D#) = 0
              Strict:
               {D# +(x, y) -> D# x,
                D# +(x, y) -> D# y,
                D# -(x, y) -> D# y}
              EDG:
               {(D# -(x, y) -> D# y, D# -(x, y) -> D# y)
                (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# x)
                (D# +(x, y) -> D# x, D# +(x, y) -> D# y)
                (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# y)}
               SCCS (1):
                Scc:
                 {D# +(x, y) -> D# x,
                  D# +(x, y) -> D# y,
                  D# -(x, y) -> D# y}
                SCC (3):
                 Strict:
                  {D# +(x, y) -> D# x,
                   D# +(x, y) -> D# y,
                   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)}
                 SPSC:
                  Simple Projection:
                   pi(D#) = 0
                  Strict:
                   {D# +(x, y) -> D# x,
                    D# -(x, y) -> D# y}
                  EDG:
                   {(D# +(x, y) -> D# x, 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# y, D# -(x, y) -> D# y)}
                   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)}
                     SPSC:
                      Simple Projection:
                       pi(D#) = 0
                      Strict:
                       {D# -(x, y) -> D# y}
                      EDG:
                       {(D# -(x, y) -> D# y, D# -(x, y) -> D# y)}
                       SCCS (1):
                        Scc:
                         {D# -(x, y) -> D# y}
                        SCC (1):
                         Strict:
                          {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)}
                         SPSC:
                          Simple Projection:
                           pi(D#) = 0
                          Strict:
                           {}
                          Qed