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)))}
 LMPO:
  Quasi-Precedence:
  empty
  
Normal:
   pi(D) = [1]
  
Safe:
   
  
Predicative System:
   {       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;););)}
  

   
  

  Qed