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(ln(x)) -> div(D(x), x),
   D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))}
 RPO Product:
  Quasi-Precedence:
  empty
  
  Qed


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(ln(x)) -> div(D(x), x),
   D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))}
 Cdiprover:
  Interpretation class: quasisimplemixed
  Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING
  ln(X12) = + 1*X12 + 1
  2 = + 0
  pow(X11, X10) = + 1*X10 + 1*X11 + 3
  div(X9, X8) = + 1*X8 + 1*X9 + 3
  minus(X7) = + 1*X7 + 1
  -(X6, X5) = + 1*X5 + 1*X6 + 4
  *(X4, X3) = + 1*X3 + 1*X4 + 1
  +(X2, X1) = + 1*X1 + 1*X2 + 1
  constant = + 0
  0 = + 0
  t = + 0
  D(X0) = + 1*X0^2 + 0 + 3*X0
  1 = + 0
  
  Qed