YES
TRS:
 {                 dx(X) -> one(),
                 dx(a()) -> zero(),
   dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
  dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
  dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
          dx(neg(ALPHA)) -> neg(dx(ALPHA)),
    dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
    dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
           dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
 DP:
  Strict:
   { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA),
     dx#(plus(ALPHA, BETA)) -> dx#(BETA),
    dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
    dx#(times(ALPHA, BETA)) -> dx#(BETA),
    dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
    dx#(minus(ALPHA, BETA)) -> dx#(BETA),
            dx#(neg(ALPHA)) -> dx#(ALPHA),
      dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
      dx#(div(ALPHA, BETA)) -> dx#(BETA),
      dx#(exp(ALPHA, BETA)) -> dx#(ALPHA),
      dx#(exp(ALPHA, BETA)) -> dx#(BETA),
             dx#(ln(ALPHA)) -> dx#(ALPHA)}
  Weak:
  {                 dx(X) -> one(),
                  dx(a()) -> zero(),
    dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
   dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
   dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
           dx(neg(ALPHA)) -> neg(dx(ALPHA)),
     dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
     dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
            dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
  EDG:
   {
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(BETA))
    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
   }
   SCCS:
    Scc:
     { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA),
       dx#(plus(ALPHA, BETA)) -> dx#(BETA),
      dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
      dx#(times(ALPHA, BETA)) -> dx#(BETA),
      dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
      dx#(minus(ALPHA, BETA)) -> dx#(BETA),
              dx#(neg(ALPHA)) -> dx#(ALPHA),
        dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
        dx#(div(ALPHA, BETA)) -> dx#(BETA),
        dx#(exp(ALPHA, BETA)) -> dx#(ALPHA),
        dx#(exp(ALPHA, BETA)) -> dx#(BETA),
               dx#(ln(ALPHA)) -> dx#(ALPHA)}
    SCC:
     Strict:
      { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA),
        dx#(plus(ALPHA, BETA)) -> dx#(BETA),
       dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
       dx#(times(ALPHA, BETA)) -> dx#(BETA),
       dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
       dx#(minus(ALPHA, BETA)) -> dx#(BETA),
               dx#(neg(ALPHA)) -> dx#(ALPHA),
         dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
         dx#(div(ALPHA, BETA)) -> dx#(BETA),
         dx#(exp(ALPHA, BETA)) -> dx#(ALPHA),
         dx#(exp(ALPHA, BETA)) -> dx#(BETA),
                dx#(ln(ALPHA)) -> dx#(ALPHA)}
     Weak:
     {                 dx(X) -> one(),
                     dx(a()) -> zero(),
       dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
      dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
      dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
              dx(neg(ALPHA)) -> neg(dx(ALPHA)),
        dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
        dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
               dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
     SPSC:
      Simple Projection:
       pi(dx#) = 0
      Strict:
       { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA),
         dx#(plus(ALPHA, BETA)) -> dx#(BETA),
        dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
        dx#(times(ALPHA, BETA)) -> dx#(BETA),
        dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
        dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                dx#(neg(ALPHA)) -> dx#(ALPHA),
          dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
          dx#(div(ALPHA, BETA)) -> dx#(BETA),
          dx#(exp(ALPHA, BETA)) -> dx#(ALPHA),
                 dx#(ln(ALPHA)) -> dx#(ALPHA)}
      EDG:
       {(dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA))
        (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))}
       SCCS:
        Scc:
         { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA),
           dx#(plus(ALPHA, BETA)) -> dx#(BETA),
          dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
          dx#(times(ALPHA, BETA)) -> dx#(BETA),
          dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
          dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                  dx#(neg(ALPHA)) -> dx#(ALPHA),
            dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
            dx#(div(ALPHA, BETA)) -> dx#(BETA),
            dx#(exp(ALPHA, BETA)) -> dx#(ALPHA),
                   dx#(ln(ALPHA)) -> dx#(ALPHA)}
        SCC:
         Strict:
          { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA),
            dx#(plus(ALPHA, BETA)) -> dx#(BETA),
           dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
           dx#(times(ALPHA, BETA)) -> dx#(BETA),
           dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
           dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                   dx#(neg(ALPHA)) -> dx#(ALPHA),
             dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
             dx#(div(ALPHA, BETA)) -> dx#(BETA),
             dx#(exp(ALPHA, BETA)) -> dx#(ALPHA),
                    dx#(ln(ALPHA)) -> dx#(ALPHA)}
         Weak:
         {                 dx(X) -> one(),
                         dx(a()) -> zero(),
           dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
          dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
          dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                  dx(neg(ALPHA)) -> neg(dx(ALPHA)),
            dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
            dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                   dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
         SPSC:
          Simple Projection:
           pi(dx#) = 0
          Strict:
           { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA),
             dx#(plus(ALPHA, BETA)) -> dx#(BETA),
            dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
            dx#(times(ALPHA, BETA)) -> dx#(BETA),
            dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
            dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                    dx#(neg(ALPHA)) -> dx#(ALPHA),
              dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
              dx#(div(ALPHA, BETA)) -> dx#(BETA),
                     dx#(ln(ALPHA)) -> dx#(ALPHA)}
          EDG:
           {(dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
            (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
            (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
            (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
            (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
            (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
            (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
            (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
            (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
            (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
            (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))}
           SCCS:
            Scc:
             { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA),
               dx#(plus(ALPHA, BETA)) -> dx#(BETA),
              dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
              dx#(times(ALPHA, BETA)) -> dx#(BETA),
              dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
              dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                      dx#(neg(ALPHA)) -> dx#(ALPHA),
                dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
                dx#(div(ALPHA, BETA)) -> dx#(BETA),
                       dx#(ln(ALPHA)) -> dx#(ALPHA)}
            SCC:
             Strict:
              { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA),
                dx#(plus(ALPHA, BETA)) -> dx#(BETA),
               dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
               dx#(times(ALPHA, BETA)) -> dx#(BETA),
               dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
               dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                       dx#(neg(ALPHA)) -> dx#(ALPHA),
                 dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
                 dx#(div(ALPHA, BETA)) -> dx#(BETA),
                        dx#(ln(ALPHA)) -> dx#(ALPHA)}
             Weak:
             {                 dx(X) -> one(),
                             dx(a()) -> zero(),
               dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
              dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
              dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                      dx(neg(ALPHA)) -> neg(dx(ALPHA)),
                dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
                dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                       dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
             SPSC:
              Simple Projection:
               pi(dx#) = 0
              Strict:
               { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                dx#(times(ALPHA, BETA)) -> dx#(BETA),
                dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                        dx#(neg(ALPHA)) -> dx#(ALPHA),
                  dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
                  dx#(div(ALPHA, BETA)) -> dx#(BETA),
                         dx#(ln(ALPHA)) -> dx#(ALPHA)}
              EDG:
               {(dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
                (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
                (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
                (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
                (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA))
                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))}
               SCCS:
                Scc:
                 { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                  dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                  dx#(times(ALPHA, BETA)) -> dx#(BETA),
                  dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                  dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                          dx#(neg(ALPHA)) -> dx#(ALPHA),
                    dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
                    dx#(div(ALPHA, BETA)) -> dx#(BETA),
                           dx#(ln(ALPHA)) -> dx#(ALPHA)}
                SCC:
                 Strict:
                  { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                   dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                   dx#(times(ALPHA, BETA)) -> dx#(BETA),
                   dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                   dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                           dx#(neg(ALPHA)) -> dx#(ALPHA),
                     dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
                     dx#(div(ALPHA, BETA)) -> dx#(BETA),
                            dx#(ln(ALPHA)) -> dx#(ALPHA)}
                 Weak:
                 {                 dx(X) -> one(),
                                 dx(a()) -> zero(),
                   dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
                  dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
                  dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                          dx(neg(ALPHA)) -> neg(dx(ALPHA)),
                    dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
                    dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                           dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
                 SPSC:
                  Simple Projection:
                   pi(dx#) = 0
                  Strict:
                   { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                    dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                    dx#(times(ALPHA, BETA)) -> dx#(BETA),
                    dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                    dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                            dx#(neg(ALPHA)) -> dx#(ALPHA),
                      dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
                             dx#(ln(ALPHA)) -> dx#(ALPHA)}
                  EDG:
                   {(dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA))
                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))}
                   SCCS:
                    Scc:
                     { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                      dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                      dx#(times(ALPHA, BETA)) -> dx#(BETA),
                      dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                      dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                              dx#(neg(ALPHA)) -> dx#(ALPHA),
                        dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
                               dx#(ln(ALPHA)) -> dx#(ALPHA)}
                    SCC:
                     Strict:
                      { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                       dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                       dx#(times(ALPHA, BETA)) -> dx#(BETA),
                       dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                       dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                               dx#(neg(ALPHA)) -> dx#(ALPHA),
                         dx#(div(ALPHA, BETA)) -> dx#(ALPHA),
                                dx#(ln(ALPHA)) -> dx#(ALPHA)}
                     Weak:
                     {                 dx(X) -> one(),
                                     dx(a()) -> zero(),
                       dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
                      dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
                      dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                              dx(neg(ALPHA)) -> neg(dx(ALPHA)),
                        dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
                        dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                               dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
                     SPSC:
                      Simple Projection:
                       pi(dx#) = 0
                      Strict:
                       { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                        dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                        dx#(times(ALPHA, BETA)) -> dx#(BETA),
                        dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                        dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                                dx#(neg(ALPHA)) -> dx#(ALPHA),
                                 dx#(ln(ALPHA)) -> dx#(ALPHA)}
                      EDG:
                       {(dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                        (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                        (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA))
                        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))}
                       SCCS:
                        Scc:
                         { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                          dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                          dx#(times(ALPHA, BETA)) -> dx#(BETA),
                          dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                          dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                                  dx#(neg(ALPHA)) -> dx#(ALPHA),
                                   dx#(ln(ALPHA)) -> dx#(ALPHA)}
                        SCC:
                         Strict:
                          { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                           dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                           dx#(times(ALPHA, BETA)) -> dx#(BETA),
                           dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                           dx#(minus(ALPHA, BETA)) -> dx#(BETA),
                                   dx#(neg(ALPHA)) -> dx#(ALPHA),
                                    dx#(ln(ALPHA)) -> dx#(ALPHA)}
                         Weak:
                         {                 dx(X) -> one(),
                                         dx(a()) -> zero(),
                           dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
                          dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
                          dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                                  dx(neg(ALPHA)) -> neg(dx(ALPHA)),
                            dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
                            dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                                   dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
                         SPSC:
                          Simple Projection:
                           pi(dx#) = 0
                          Strict:
                           { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                            dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                            dx#(times(ALPHA, BETA)) -> dx#(BETA),
                            dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                                    dx#(neg(ALPHA)) -> dx#(ALPHA),
                                     dx#(ln(ALPHA)) -> dx#(ALPHA)}
                          EDG:
                           {(dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                            (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                            (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA))
                            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))}
                           SCCS:
                            Scc:
                             { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                              dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                              dx#(times(ALPHA, BETA)) -> dx#(BETA),
                              dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                                      dx#(neg(ALPHA)) -> dx#(ALPHA),
                                       dx#(ln(ALPHA)) -> dx#(ALPHA)}
                            SCC:
                             Strict:
                              { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                               dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                               dx#(times(ALPHA, BETA)) -> dx#(BETA),
                               dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                                       dx#(neg(ALPHA)) -> dx#(ALPHA),
                                        dx#(ln(ALPHA)) -> dx#(ALPHA)}
                             Weak:
                             {                 dx(X) -> one(),
                                             dx(a()) -> zero(),
                               dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
                              dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
                              dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                                      dx(neg(ALPHA)) -> neg(dx(ALPHA)),
                                dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
                                dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                                       dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
                             SPSC:
                              Simple Projection:
                               pi(dx#) = 0
                              Strict:
                               { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                                dx#(times(ALPHA, BETA)) -> dx#(BETA),
                                dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                                         dx#(ln(ALPHA)) -> dx#(ALPHA)}
                              EDG:
                               {(dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                                (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                                (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA))
                                (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))}
                               SCCS:
                                Scc:
                                 { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                  dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                                  dx#(times(ALPHA, BETA)) -> dx#(BETA),
                                  dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                                           dx#(ln(ALPHA)) -> dx#(ALPHA)}
                                SCC:
                                 Strict:
                                  { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                   dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                                   dx#(times(ALPHA, BETA)) -> dx#(BETA),
                                   dx#(minus(ALPHA, BETA)) -> dx#(ALPHA),
                                            dx#(ln(ALPHA)) -> dx#(ALPHA)}
                                 Weak:
                                 {                 dx(X) -> one(),
                                                 dx(a()) -> zero(),
                                   dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
                                  dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
                                  dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                                          dx(neg(ALPHA)) -> neg(dx(ALPHA)),
                                    dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
                                    dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                                           dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
                                 SPSC:
                                  Simple Projection:
                                   pi(dx#) = 0
                                  Strict:
                                   { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                    dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                                    dx#(times(ALPHA, BETA)) -> dx#(BETA),
                                             dx#(ln(ALPHA)) -> dx#(ALPHA)}
                                  EDG:
                                   {(dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                    (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                    (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                    (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))
                                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                    (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))}
                                   SCCS:
                                    Scc:
                                     { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                      dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                                      dx#(times(ALPHA, BETA)) -> dx#(BETA),
                                               dx#(ln(ALPHA)) -> dx#(ALPHA)}
                                    SCC:
                                     Strict:
                                      { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                       dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                                       dx#(times(ALPHA, BETA)) -> dx#(BETA),
                                                dx#(ln(ALPHA)) -> dx#(ALPHA)}
                                     Weak:
                                     {                 dx(X) -> one(),
                                                     dx(a()) -> zero(),
                                       dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
                                      dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
                                      dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                                              dx(neg(ALPHA)) -> neg(dx(ALPHA)),
                                        dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
                                        dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                                               dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
                                     SPSC:
                                      Simple Projection:
                                       pi(dx#) = 0
                                      Strict:
                                       { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                        dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                                        dx#(times(ALPHA, BETA)) -> dx#(BETA)}
                                      EDG:
                                       {(dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                        (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                        (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA))
                                        (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))}
                                       SCCS:
                                        Scc:
                                         { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                          dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                                          dx#(times(ALPHA, BETA)) -> dx#(BETA)}
                                        SCC:
                                         Strict:
                                          { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                           dx#(times(ALPHA, BETA)) -> dx#(ALPHA),
                                           dx#(times(ALPHA, BETA)) -> dx#(BETA)}
                                         Weak:
                                         {                 dx(X) -> one(),
                                                         dx(a()) -> zero(),
                                           dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
                                          dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
                                          dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                                                  dx(neg(ALPHA)) -> neg(dx(ALPHA)),
                                            dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
                                            dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                                                   dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
                                         SPSC:
                                          Simple Projection:
                                           pi(dx#) = 0
                                          Strict:
                                           { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                            dx#(times(ALPHA, BETA)) -> dx#(BETA)}
                                          EDG:
                                           {(dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))
                                            (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA))
                                            (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))}
                                           SCCS:
                                            Scc:
                                             { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                              dx#(times(ALPHA, BETA)) -> dx#(BETA)}
                                            SCC:
                                             Strict:
                                              { dx#(plus(ALPHA, BETA)) -> dx#(BETA),
                                               dx#(times(ALPHA, BETA)) -> dx#(BETA)}
                                             Weak:
                                             {                 dx(X) -> one(),
                                                             dx(a()) -> zero(),
                                               dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
                                              dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
                                              dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                                                      dx(neg(ALPHA)) -> neg(dx(ALPHA)),
                                                dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
                                                dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                                                       dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
                                             SPSC:
                                              Simple Projection:
                                               pi(dx#) = 0
                                              Strict:
                                               {dx#(times(ALPHA, BETA)) -> dx#(BETA)}
                                              EDG:
                                               {(dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))}
                                               SCCS:
                                                Scc:
                                                 {dx#(times(ALPHA, BETA)) -> dx#(BETA)}
                                                SCC:
                                                 Strict:
                                                  {dx#(times(ALPHA, BETA)) -> dx#(BETA)}
                                                 Weak:
                                                 {                 dx(X) -> one(),
                                                                 dx(a()) -> zero(),
                                                   dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)),
                                                  dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))),
                                                  dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)),
                                                          dx(neg(ALPHA)) -> neg(dx(ALPHA)),
                                                    dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))),
                                                    dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))),
                                                           dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)}
                                                 SPSC:
                                                  Simple Projection:
                                                   pi(dx#) = 0
                                                  Strict:
                                                   {}
                                                  Qed