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)),
    D(minus(x)) -> minus(D(x)),
   D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
   D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
       D(ln(x)) -> div(D(x), x)}
 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),
     D#(minus(x)) -> D#(x),
    D#(div(x, y)) -> D#(x),
    D#(div(x, y)) -> D#(y),
    D#(pow(x, y)) -> D#(x),
    D#(pow(x, y)) -> D#(y),
        D#(ln(x)) -> D#(x)}
  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)),
     D(minus(x)) -> minus(D(x)),
    D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
    D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
        D(ln(x)) -> div(D(x), x)}
  EDG:
   {(D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x))
    (D#(*(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y))
    (D#(*(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x))
    (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
    (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
    (D#(*(x, y)) -> D#(x), D#(minus(x)) -> 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#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x))
    (D#(minus(x)) -> D#(x), D#(pow(x, y)) -> D#(y))
    (D#(minus(x)) -> D#(x), D#(pow(x, y)) -> D#(x))
    (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(y))
    (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x))
    (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x))
    (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y))
    (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x))
    (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y))
    (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x))
    (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y))
    (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(x))
    (D#(pow(x, y)) -> D#(x), D#(ln(x)) -> D#(x))
    (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y))
    (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x))
    (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
    (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
    (D#(pow(x, y)) -> D#(x), D#(minus(x)) -> D#(x))
    (D#(pow(x, y)) -> D#(x), D#(-(x, y)) -> D#(y))
    (D#(pow(x, y)) -> D#(x), D#(-(x, y)) -> D#(x))
    (D#(pow(x, y)) -> D#(x), D#(*(x, y)) -> D#(y))
    (D#(pow(x, y)) -> D#(x), D#(*(x, y)) -> D#(x))
    (D#(pow(x, y)) -> D#(x), D#(+(x, y)) -> D#(y))
    (D#(pow(x, y)) -> D#(x), D#(+(x, y)) -> D#(x))
    (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
    (D#(+(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y))
    (D#(+(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x))
    (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
    (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
    (D#(+(x, y)) -> D#(y), D#(minus(x)) -> 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#(ln(x)) -> D#(x))
    (D#(-(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y))
    (D#(-(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x))
    (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
    (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
    (D#(-(x, y)) -> D#(y), D#(minus(x)) -> 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#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
    (D#(pow(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y))
    (D#(pow(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x))
    (D#(pow(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
    (D#(pow(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
    (D#(pow(x, y)) -> D#(y), D#(minus(x)) -> D#(x))
    (D#(pow(x, y)) -> D#(y), D#(-(x, y)) -> D#(y))
    (D#(pow(x, y)) -> D#(y), D#(-(x, y)) -> D#(x))
    (D#(pow(x, y)) -> D#(y), D#(*(x, y)) -> D#(y))
    (D#(pow(x, y)) -> D#(y), D#(*(x, y)) -> D#(x))
    (D#(pow(x, y)) -> D#(y), D#(+(x, y)) -> D#(y))
    (D#(pow(x, y)) -> D#(y), D#(+(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(y))
    (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(y))
    (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(y))
    (D#(div(x, y)) -> D#(y), D#(minus(x)) -> D#(x))
    (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
    (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y))
    (D#(div(x, y)) -> D#(y), D#(ln(x)) -> 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#(y), D#(minus(x)) -> D#(x))
    (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
    (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
    (D#(*(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x))
    (D#(*(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y))
    (D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
    (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(x))
    (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y))
    (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x))
    (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y))
    (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x))
    (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y))
    (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x))
    (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x))
    (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(y))
    (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> D#(x))
    (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> D#(y))
    (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x))
    (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(y))
    (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(y))
    (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(y))
    (D#(div(x, y)) -> D#(x), D#(minus(x)) -> D#(x))
    (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
    (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x))
    (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y))
    (D#(div(x, y)) -> D#(x), D#(ln(x)) -> 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#(x), D#(minus(x)) -> D#(x))
    (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
    (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
    (D#(-(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x))
    (D#(-(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y))
    (D#(-(x, y)) -> D#(x), D#(ln(x)) -> 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#(x), D#(minus(x)) -> D#(x))
    (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
    (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
    (D#(+(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x))
    (D#(+(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y))
    (D#(+(x, y)) -> D#(x), D#(ln(x)) -> D#(x))}
   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),
       D#(minus(x)) -> D#(x),
      D#(div(x, y)) -> D#(x),
      D#(div(x, y)) -> D#(y),
      D#(pow(x, y)) -> D#(x),
      D#(pow(x, y)) -> D#(y),
          D#(ln(x)) -> D#(x)}
    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),
        D#(minus(x)) -> D#(x),
       D#(div(x, y)) -> D#(x),
       D#(div(x, y)) -> D#(y),
       D#(pow(x, y)) -> D#(x),
       D#(pow(x, y)) -> D#(y),
           D#(ln(x)) -> D#(x)}
     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)),
        D(minus(x)) -> minus(D(x)),
       D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
       D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
           D(ln(x)) -> div(D(x), x)}
     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#(x),
          D#(-(x, y)) -> D#(y),
         D#(minus(x)) -> D#(x),
        D#(div(x, y)) -> D#(x),
        D#(div(x, y)) -> D#(y),
        D#(pow(x, y)) -> D#(x),
            D#(ln(x)) -> D#(x)}
      EDG:
       {(D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x))
        (D#(*(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x))
        (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
        (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
        (D#(*(x, y)) -> D#(x), D#(minus(x)) -> 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#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x))
        (D#(minus(x)) -> D#(x), D#(pow(x, y)) -> D#(x))
        (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(y))
        (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x))
        (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x))
        (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y))
        (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x))
        (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y))
        (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x))
        (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y))
        (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(x))
        (D#(pow(x, y)) -> D#(x), D#(ln(x)) -> D#(x))
        (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x))
        (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
        (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
        (D#(pow(x, y)) -> D#(x), D#(minus(x)) -> D#(x))
        (D#(pow(x, y)) -> D#(x), D#(-(x, y)) -> D#(y))
        (D#(pow(x, y)) -> D#(x), D#(-(x, y)) -> D#(x))
        (D#(pow(x, y)) -> D#(x), D#(*(x, y)) -> D#(y))
        (D#(pow(x, y)) -> D#(x), D#(*(x, y)) -> D#(x))
        (D#(pow(x, y)) -> D#(x), D#(+(x, y)) -> D#(y))
        (D#(pow(x, y)) -> D#(x), D#(+(x, y)) -> D#(x))
        (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
        (D#(+(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x))
        (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
        (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
        (D#(+(x, y)) -> D#(y), D#(minus(x)) -> 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#(ln(x)) -> D#(x))
        (D#(-(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x))
        (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
        (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
        (D#(-(x, y)) -> D#(y), D#(minus(x)) -> 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#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(x))
        (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(y))
        (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(x))
        (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(y))
        (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(x))
        (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(y))
        (D#(div(x, y)) -> D#(y), D#(minus(x)) -> D#(x))
        (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
        (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
        (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x))
        (D#(div(x, y)) -> D#(y), D#(ln(x)) -> 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#(y), D#(minus(x)) -> D#(x))
        (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
        (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
        (D#(*(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x))
        (D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
        (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(x))
        (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y))
        (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x))
        (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y))
        (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x))
        (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y))
        (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x))
        (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x))
        (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(y))
        (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> D#(x))
        (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x))
        (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(x))
        (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(y))
        (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(x))
        (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(y))
        (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(x))
        (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(y))
        (D#(div(x, y)) -> D#(x), D#(minus(x)) -> D#(x))
        (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
        (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
        (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x))
        (D#(div(x, y)) -> D#(x), D#(ln(x)) -> 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#(x), D#(minus(x)) -> D#(x))
        (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
        (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
        (D#(-(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x))
        (D#(-(x, y)) -> D#(x), D#(ln(x)) -> 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#(x), D#(minus(x)) -> D#(x))
        (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
        (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
        (D#(+(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x))
        (D#(+(x, y)) -> D#(x), D#(ln(x)) -> D#(x))}
       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),
           D#(minus(x)) -> D#(x),
          D#(div(x, y)) -> D#(x),
          D#(div(x, y)) -> D#(y),
          D#(pow(x, y)) -> D#(x),
              D#(ln(x)) -> D#(x)}
        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),
            D#(minus(x)) -> D#(x),
           D#(div(x, y)) -> D#(x),
           D#(div(x, y)) -> D#(y),
           D#(pow(x, y)) -> D#(x),
               D#(ln(x)) -> D#(x)}
         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)),
            D(minus(x)) -> minus(D(x)),
           D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
           D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
               D(ln(x)) -> div(D(x), x)}
         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#(x),
              D#(-(x, y)) -> D#(y),
             D#(minus(x)) -> D#(x),
            D#(div(x, y)) -> D#(x),
            D#(div(x, y)) -> D#(y),
                D#(ln(x)) -> D#(x)}
          EDG:
           {(D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x))
            (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
            (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
            (D#(*(x, y)) -> D#(x), D#(minus(x)) -> 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#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x))
            (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(y))
            (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x))
            (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x))
            (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y))
            (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x))
            (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y))
            (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x))
            (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y))
            (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(x))
            (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x))
            (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(y))
            (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x))
            (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x))
            (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y))
            (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x))
            (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y))
            (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x))
            (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y))
            (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(x))
            (D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
            (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
            (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
            (D#(*(x, y)) -> D#(y), D#(minus(x)) -> 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#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
            (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
            (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
            (D#(div(x, y)) -> D#(y), D#(minus(x)) -> D#(x))
            (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(y))
            (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(x))
            (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(y))
            (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(x))
            (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(y))
            (D#(div(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#(y), D#(minus(x)) -> D#(x))
            (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
            (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
            (D#(-(x, y)) -> D#(y), D#(ln(x)) -> 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#(y), D#(minus(x)) -> D#(x))
            (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
            (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
            (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
            (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(x))
            (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(y))
            (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(x))
            (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(y))
            (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(x))
            (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(y))
            (D#(div(x, y)) -> D#(x), D#(minus(x)) -> D#(x))
            (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
            (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
            (D#(div(x, y)) -> D#(x), D#(ln(x)) -> 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#(x), D#(minus(x)) -> D#(x))
            (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
            (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
            (D#(-(x, y)) -> D#(x), D#(ln(x)) -> 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#(x), D#(minus(x)) -> D#(x))
            (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
            (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
            (D#(+(x, y)) -> D#(x), D#(ln(x)) -> D#(x))}
           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),
               D#(minus(x)) -> D#(x),
              D#(div(x, y)) -> D#(x),
              D#(div(x, y)) -> D#(y),
                  D#(ln(x)) -> D#(x)}
            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),
                D#(minus(x)) -> D#(x),
               D#(div(x, y)) -> D#(x),
               D#(div(x, y)) -> D#(y),
                   D#(ln(x)) -> D#(x)}
             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)),
                D(minus(x)) -> minus(D(x)),
               D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
               D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
                   D(ln(x)) -> div(D(x), x)}
             SPSC:
              Simple Projection:
               pi(D#) = 0
              Strict:
               {  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#(minus(x)) -> D#(x),
                D#(div(x, y)) -> D#(x),
                D#(div(x, y)) -> D#(y),
                    D#(ln(x)) -> D#(x)}
              EDG:
               {(D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
                (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
                (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
                (D#(*(x, y)) -> D#(y), D#(minus(x)) -> 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#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
                (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
                (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
                (D#(div(x, y)) -> D#(y), D#(minus(x)) -> D#(x))
                (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(y))
                (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(x))
                (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(y))
                (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(x))
                (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(y))
                (D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x))
                (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
                (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
                (D#(-(x, y)) -> D#(x), D#(minus(x)) -> 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#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x))
                (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
                (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
                (D#(div(x, y)) -> D#(x), D#(minus(x)) -> D#(x))
                (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(y))
                (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(x))
                (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(y))
                (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(x))
                (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(y))
                (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y))
                (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x))
                (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y))
                (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x))
                (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y))
                (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x))
                (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x))
                (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(y))
                (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x))
                (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y))
                (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x))
                (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y))
                (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x))
                (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y))
                (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x))
                (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x))
                (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(y))
                (D#(minus(x)) -> D#(x), D#(ln(x)) -> 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#(minus(x)) -> D#(x))
                (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
                (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(y))
                (D#(*(x, y)) -> D#(x), D#(ln(x)) -> 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#(minus(x)) -> D#(x))
                (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
                (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
                (D#(-(x, y)) -> D#(y), D#(ln(x)) -> 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#(minus(x)) -> D#(x))
                (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
                (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(y))
                (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x))}
               SCCS:
                Scc:
                 {  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#(minus(x)) -> D#(x),
                  D#(div(x, y)) -> D#(x),
                  D#(div(x, y)) -> D#(y),
                      D#(ln(x)) -> D#(x)}
                SCC:
                 Strict:
                  {  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#(minus(x)) -> D#(x),
                   D#(div(x, y)) -> D#(x),
                   D#(div(x, y)) -> D#(y),
                       D#(ln(x)) -> D#(x)}
                 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)),
                    D(minus(x)) -> minus(D(x)),
                   D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
                   D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
                       D(ln(x)) -> div(D(x), x)}
                 SPSC:
                  Simple Projection:
                   pi(D#) = 0
                  Strict:
                   {  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#(minus(x)) -> D#(x),
                    D#(div(x, y)) -> D#(x),
                        D#(ln(x)) -> D#(x)}
                  EDG:
                   {(D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
                    (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
                    (D#(*(x, y)) -> D#(y), D#(minus(x)) -> 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#(ln(x)) -> D#(x))
                    (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
                    (D#(*(x, y)) -> D#(x), D#(minus(x)) -> 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#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x))
                    (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x))
                    (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x))
                    (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y))
                    (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x))
                    (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y))
                    (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x))
                    (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y))
                    (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x))
                    (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x))
                    (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x))
                    (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y))
                    (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x))
                    (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y))
                    (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x))
                    (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y))
                    (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(y))
                    (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(x))
                    (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(y))
                    (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(x))
                    (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(y))
                    (D#(div(x, y)) -> D#(x), D#(minus(x)) -> D#(x))
                    (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
                    (D#(div(x, y)) -> D#(x), D#(ln(x)) -> 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#(minus(x)) -> D#(x))
                    (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(x))
                    (D#(-(x, y)) -> D#(x), D#(ln(x)) -> 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#(minus(x)) -> D#(x))
                    (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
                    (D#(-(x, y)) -> D#(y), D#(ln(x)) -> 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#(minus(x)) -> D#(x))
                    (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(x))
                    (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x))}
                   SCCS:
                    Scc:
                     {  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#(minus(x)) -> D#(x),
                      D#(div(x, y)) -> D#(x),
                          D#(ln(x)) -> D#(x)}
                    SCC:
                     Strict:
                      {  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#(minus(x)) -> D#(x),
                       D#(div(x, y)) -> D#(x),
                           D#(ln(x)) -> D#(x)}
                     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)),
                        D(minus(x)) -> minus(D(x)),
                       D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
                       D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
                           D(ln(x)) -> div(D(x), x)}
                     SPSC:
                      Simple Projection:
                       pi(D#) = 0
                      Strict:
                       { 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#(minus(x)) -> D#(x),
                           D#(ln(x)) -> D#(x)}
                      EDG:
                       {(D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
                        (D#(*(x, y)) -> D#(y), D#(minus(x)) -> 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#(ln(x)) -> D#(x))
                        (D#(*(x, y)) -> D#(x), D#(minus(x)) -> 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#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x))
                        (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x))
                        (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y))
                        (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x))
                        (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y))
                        (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x))
                        (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y))
                        (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y))
                        (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x))
                        (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y))
                        (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x))
                        (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y))
                        (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x))
                        (D#(ln(x)) -> D#(x), D#(ln(x)) -> 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#(minus(x)) -> D#(x))
                        (D#(-(x, y)) -> D#(x), D#(ln(x)) -> 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#(minus(x)) -> D#(x))
                        (D#(-(x, y)) -> D#(y), D#(ln(x)) -> 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#(minus(x)) -> D#(x))
                        (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x))}
                       SCCS:
                        Scc:
                         { 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#(minus(x)) -> D#(x),
                             D#(ln(x)) -> D#(x)}
                        SCC:
                         Strict:
                          { 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#(minus(x)) -> D#(x),
                              D#(ln(x)) -> D#(x)}
                         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)),
                            D(minus(x)) -> minus(D(x)),
                           D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
                           D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
                               D(ln(x)) -> div(D(x), x)}
                         SPSC:
                          Simple Projection:
                           pi(D#) = 0
                          Strict:
                           { D#(+(x, y)) -> D#(y),
                             D#(*(x, y)) -> D#(x),
                             D#(*(x, y)) -> D#(y),
                             D#(-(x, y)) -> D#(x),
                            D#(minus(x)) -> D#(x),
                               D#(ln(x)) -> D#(x)}
                          EDG:
                           {(D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x))
                            (D#(-(x, y)) -> D#(x), D#(minus(x)) -> 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#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x))
                            (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x))
                            (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x))
                            (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y))
                            (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x))
                            (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y))
                            (D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
                            (D#(*(x, y)) -> D#(y), D#(minus(x)) -> 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#(minus(x)) -> D#(x))
                            (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x))
                            (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y))
                            (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x))
                            (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y))
                            (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x))
                            (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x))
                            (D#(minus(x)) -> D#(x), D#(ln(x)) -> 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#(minus(x)) -> D#(x))
                            (D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x))}
                           SCCS:
                            Scc:
                             { D#(+(x, y)) -> D#(y),
                               D#(*(x, y)) -> D#(x),
                               D#(*(x, y)) -> D#(y),
                               D#(-(x, y)) -> D#(x),
                              D#(minus(x)) -> D#(x),
                                 D#(ln(x)) -> D#(x)}
                            SCC:
                             Strict:
                              { D#(+(x, y)) -> D#(y),
                                D#(*(x, y)) -> D#(x),
                                D#(*(x, y)) -> D#(y),
                                D#(-(x, y)) -> D#(x),
                               D#(minus(x)) -> D#(x),
                                  D#(ln(x)) -> D#(x)}
                             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)),
                                D(minus(x)) -> minus(D(x)),
                               D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
                               D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
                                   D(ln(x)) -> div(D(x), x)}
                             SPSC:
                              Simple Projection:
                               pi(D#) = 0
                              Strict:
                               {D#(+(x, y)) -> D#(y),
                                D#(*(x, y)) -> D#(x),
                                D#(*(x, y)) -> D#(y),
                                D#(-(x, y)) -> D#(x),
                                  D#(ln(x)) -> D#(x)}
                              EDG:
                               {(D#(-(x, y)) -> D#(x), D#(ln(x)) -> 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#(ln(x)) -> 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#(ln(x)) -> D#(x))
                                (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y))
                                (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x))
                                (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y))
                                (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x))
                                (D#(ln(x)) -> D#(x), D#(ln(x)) -> 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#(ln(x)) -> D#(x))}
                               SCCS:
                                Scc:
                                 {D#(+(x, y)) -> D#(y),
                                  D#(*(x, y)) -> D#(x),
                                  D#(*(x, y)) -> D#(y),
                                  D#(-(x, y)) -> D#(x),
                                    D#(ln(x)) -> D#(x)}
                                SCC:
                                 Strict:
                                  {D#(+(x, y)) -> D#(y),
                                   D#(*(x, y)) -> D#(x),
                                   D#(*(x, y)) -> D#(y),
                                   D#(-(x, y)) -> D#(x),
                                     D#(ln(x)) -> D#(x)}
                                 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)),
                                    D(minus(x)) -> minus(D(x)),
                                   D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
                                   D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
                                       D(ln(x)) -> div(D(x), x)}
                                 SPSC:
                                  Simple Projection:
                                   pi(D#) = 0
                                  Strict:
                                   {D#(+(x, y)) -> D#(y),
                                    D#(*(x, y)) -> D#(x),
                                    D#(*(x, y)) -> D#(y),
                                      D#(ln(x)) -> D#(x)}
                                  EDG:
                                   {(D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x))
                                    (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y))
                                    (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x))
                                    (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y))
                                    (D#(*(x, y)) -> D#(y), D#(ln(x)) -> 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#(ln(x)) -> 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#(ln(x)) -> D#(x))}
                                   SCCS:
                                    Scc:
                                     {D#(+(x, y)) -> D#(y),
                                      D#(*(x, y)) -> D#(x),
                                      D#(*(x, y)) -> D#(y),
                                        D#(ln(x)) -> D#(x)}
                                    SCC:
                                     Strict:
                                      {D#(+(x, y)) -> D#(y),
                                       D#(*(x, y)) -> D#(x),
                                       D#(*(x, y)) -> D#(y),
                                         D#(ln(x)) -> D#(x)}
                                     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)),
                                        D(minus(x)) -> minus(D(x)),
                                       D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
                                       D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
                                           D(ln(x)) -> div(D(x), x)}
                                     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)),
                                            D(minus(x)) -> minus(D(x)),
                                           D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
                                           D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
                                               D(ln(x)) -> div(D(x), x)}
                                         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)),
                                                D(minus(x)) -> minus(D(x)),
                                               D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
                                               D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
                                                   D(ln(x)) -> div(D(x), x)}
                                             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)),
                                                    D(minus(x)) -> minus(D(x)),
                                                   D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))),
                                                   D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))),
                                                       D(ln(x)) -> div(D(x), x)}
                                                 SPSC:
                                                  Simple Projection:
                                                   pi(D#) = 0
                                                  Strict:
                                                   {}
                                                  Qed