YES

Problem:
 exp(x,0()) -> s(0())
 exp(x,s(y)) -> *(x,exp(x,y))
 *(0(),y) -> 0()
 *(s(x),y) -> +(y,*(x,y))
 -(0(),y) -> 0()
 -(x,0()) -> x
 -(s(x),s(y)) -> -(x,y)

Proof:
 DP Processor:
  DPs:
   exp#(x,s(y)) -> exp#(x,y)
   exp#(x,s(y)) -> *#(x,exp(x,y))
   *#(s(x),y) -> *#(x,y)
   -#(s(x),s(y)) -> -#(x,y)
  TRS:
   exp(x,0()) -> s(0())
   exp(x,s(y)) -> *(x,exp(x,y))
   *(0(),y) -> 0()
   *(s(x),y) -> +(y,*(x,y))
   -(0(),y) -> 0()
   -(x,0()) -> x
   -(s(x),s(y)) -> -(x,y)
  Usable Rule Processor:
   DPs:
    exp#(x,s(y)) -> exp#(x,y)
    exp#(x,s(y)) -> *#(x,exp(x,y))
    *#(s(x),y) -> *#(x,y)
    -#(s(x),s(y)) -> -#(x,y)
   TRS:
    exp(x,0()) -> s(0())
    exp(x,s(y)) -> *(x,exp(x,y))
    *(0(),y) -> 0()
    *(s(x),y) -> +(y,*(x,y))
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     exp(x,0()) -> s(0())
     exp(x,s(y)) -> *(x,exp(x,y))
     *(0(),y) -> 0()
     *(s(x),y) -> +(y,*(x,y))
    interpretation:
     [-#](x0, x1) = 6x0 + 1,
     
     [*#](x0, x1) = 2x0 + 4x1,
     
     [exp#](x0, x1) = 2x0 + 4x1 + 6,
     
     [+](x0, x1) = x0 + 4,
     
     [*](x0, x1) = 2x1 + 4,
     
     [s](x0) = 2x0 + 5,
     
     [exp](x0, x1) = 2x1 + 6,
     
     [0] = 4
    orientation:
     exp#(x,s(y)) = 2x + 8y + 26 >= 2x + 4y + 6 = exp#(x,y)
     
     exp#(x,s(y)) = 2x + 8y + 26 >= 2x + 8y + 24 = *#(x,exp(x,y))
     
     *#(s(x),y) = 4x + 4y + 10 >= 2x + 4y = *#(x,y)
     
     -#(s(x),s(y)) = 12x + 31 >= 6x + 1 = -#(x,y)
     
     exp(x,0()) = 14 >= 13 = s(0())
     
     exp(x,s(y)) = 4y + 16 >= 4y + 16 = *(x,exp(x,y))
     
     *(0(),y) = 2y + 4 >= 4 = 0()
     
     *(s(x),y) = 2y + 4 >= y + 4 = +(y,*(x,y))
    problem:
     DPs:
      
     TRS:
      exp(x,0()) -> s(0())
      exp(x,s(y)) -> *(x,exp(x,y))
      *(0(),y) -> 0()
      *(s(x),y) -> +(y,*(x,y))
    Qed