MAYBE

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:
    
   Restore Modifier:
    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))
    SCC Processor:
     #sccs: 1
     #rules: 6
     #arcs: 36/36
     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))
     Open