YES

Problem:
 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))

Proof:
 DP Processor:
  DPs:
   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#(-(x,y)) -> D#(x)
  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))
  Usable Rule Processor:
   DPs:
    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#(-(x,y)) -> D#(x)
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [D#](x0) = 4x0 + -16,
     
     [-](x0, x1) = 2x0 + 1x1 + -1,
     
     [*](x0, x1) = 2x0 + 2x1 + -4,
     
     [+](x0, x1) = 1x0 + 2x1 + -4
    orientation:
     D#(+(x,y)) = 5x + 6y + 0 >= 4y + -16 = D#(y)
     
     D#(+(x,y)) = 5x + 6y + 0 >= 4x + -16 = D#(x)
     
     D#(*(x,y)) = 6x + 6y + 0 >= 4y + -16 = D#(y)
     
     D#(*(x,y)) = 6x + 6y + 0 >= 4x + -16 = D#(x)
     
     D#(-(x,y)) = 6x + 5y + 3 >= 4y + -16 = D#(y)
     
     D#(-(x,y)) = 6x + 5y + 3 >= 4x + -16 = D#(x)
    problem:
     DPs:
      
     TRS:
      
    Qed