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))}
 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;);)}
  

   
  

  Qed