YES
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:
  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))}
  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#(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#(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))
    (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), 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#(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#(y))}
   SCCS:
    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:
     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#(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#(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#(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))
        (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))}
       SCCS:
        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:
         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#(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#(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#(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#(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))}
           SCCS:
            Scc:
             {D#(+(x, y)) -> D#(x),
              D#(+(x, y)) -> D#(y),
              D#(*(x, y)) -> D#(x),
              D#(-(x, y)) -> D#(y)}
            SCC:
             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#(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#(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#(y))
                (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x))
                (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(y))}
               SCCS:
                Scc:
                 {D#(+(x, y)) -> D#(y),
                  D#(*(x, y)) -> D#(x),
                  D#(-(x, y)) -> D#(y)}
                SCC:
                 Strict:
                  {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#(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#(y))
                    (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(y))}
                   SCCS:
                    Scc:
                     {D#(+(x, y)) -> D#(y),
                      D#(-(x, y)) -> D#(y)}
                    SCC:
                     Strict:
                      {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#(y)}
                      EDG:
                       {(D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(y))}
                       SCCS:
                        Scc:
                         {D#(-(x, y)) -> D#(y)}
                        SCC:
                         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