YES

Problem:
 add(0(),x) -> x
 add(s(x),y) -> s(add(x,y))
 mult(0(),x) -> 0()
 mult(s(x),y) -> add(y,mult(x,y))

Proof:
 DP Processor:
  DPs:
   add#(s(x),y) -> add#(x,y)
   mult#(s(x),y) -> mult#(x,y)
   mult#(s(x),y) -> add#(y,mult(x,y))
  TRS:
   add(0(),x) -> x
   add(s(x),y) -> s(add(x,y))
   mult(0(),x) -> 0()
   mult(s(x),y) -> add(y,mult(x,y))
  TDG Processor:
   DPs:
    add#(s(x),y) -> add#(x,y)
    mult#(s(x),y) -> mult#(x,y)
    mult#(s(x),y) -> add#(y,mult(x,y))
   TRS:
    add(0(),x) -> x
    add(s(x),y) -> s(add(x,y))
    mult(0(),x) -> 0()
    mult(s(x),y) -> add(y,mult(x,y))
   graph:
    mult#(s(x),y) -> mult#(x,y) -> mult#(s(x),y) -> add#(y,mult(x,y))
    mult#(s(x),y) -> mult#(x,y) -> mult#(s(x),y) -> mult#(x,y)
    mult#(s(x),y) -> add#(y,mult(x,y)) -> add#(s(x),y) -> add#(x,y)
    add#(s(x),y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 4/9
    DPs:
     mult#(s(x),y) -> mult#(x,y)
    TRS:
     add(0(),x) -> x
     add(s(x),y) -> s(add(x,y))
     mult(0(),x) -> 0()
     mult(s(x),y) -> add(y,mult(x,y))
    Subterm Criterion Processor:
     simple projection:
      pi(mult#) = 0
     problem:
      DPs:
       
      TRS:
       add(0(),x) -> x
       add(s(x),y) -> s(add(x,y))
       mult(0(),x) -> 0()
       mult(s(x),y) -> add(y,mult(x,y))
     Qed
    
    DPs:
     add#(s(x),y) -> add#(x,y)
    TRS:
     add(0(),x) -> x
     add(s(x),y) -> s(add(x,y))
     mult(0(),x) -> 0()
     mult(s(x),y) -> add(y,mult(x,y))
    Subterm Criterion Processor:
     simple projection:
      pi(add#) = 0
     problem:
      DPs:
       
      TRS:
       add(0(),x) -> x
       add(s(x),y) -> s(add(x,y))
       mult(0(),x) -> 0()
       mult(s(x),y) -> add(y,mult(x,y))
     Qed