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)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [-#](x0, x1) = 2x0 + x1 + 1/2,
    
    [*#](x0, x1) = x0,
    
    [exp#](x0, x1) = 2x0 + x1 + 1/2,
    
    [-](x0, x1) = x0 + 3/2,
    
    [+](x0, x1) = x1,
    
    [*](x0, x1) = 3x0,
    
    [s](x0) = 3/2x0 + 1/2,
    
    [exp](x0, x1) = 3x0 + 1/2,
    
    [0] = 0
   orientation:
    exp#(x,s(y)) = 2x + 3/2y + 1 >= 2x + y + 1/2 = exp#(x,y)
    
    exp#(x,s(y)) = 2x + 3/2y + 1 >= x = *#(x,exp(x,y))
    
    *#(s(x),y) = 3/2x + 1/2 >= x = *#(x,y)
    
    -#(s(x),s(y)) = 3x + 3/2y + 2 >= 2x + y + 1/2 = -#(x,y)
    
    exp(x,0()) = 3x + 1/2 >= 1/2 = s(0())
    
    exp(x,s(y)) = 3x + 1/2 >= 3x = *(x,exp(x,y))
    
    *(0(),y) = 0 >= 0 = 0()
    
    *(s(x),y) = 9/2x + 3/2 >= 3x = +(y,*(x,y))
    
    -(0(),y) = 3/2 >= 0 = 0()
    
    -(x,0()) = x + 3/2 >= x = x
    
    -(s(x),s(y)) = 3/2x + 2 >= x + 3/2 = -(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))
     -(0(),y) -> 0()
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
   Qed