YES

Problem:
 -(x,0()) -> x
 -(s(x),s(y)) -> -(x,y)
 *(x,0()) -> 0()
 *(x,s(y)) -> +(*(x,y),x)
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 odd(0()) -> false()
 odd(s(0())) -> true()
 odd(s(s(x))) -> odd(x)
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 if(true(),x,y) -> true()
 if(false(),x,y) -> false()
 pow(x,y) -> f(x,y,s(0()))
 f(x,0(),z) -> z
 f(x,s(y),z) -> if(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))

Proof:
 DP Processor:
  DPs:
   -#(s(x),s(y)) -> -#(x,y)
   *#(x,s(y)) -> *#(x,y)
   odd#(s(s(x))) -> odd#(x)
   half#(s(s(x))) -> half#(x)
   pow#(x,y) -> f#(x,y,s(0()))
   f#(x,s(y),z) -> half#(s(y))
   f#(x,s(y),z) -> *#(x,x)
   f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z)
   f#(x,s(y),z) -> *#(x,z)
   f#(x,s(y),z) -> f#(x,y,*(x,z))
   f#(x,s(y),z) -> odd#(s(y))
   f#(x,s(y),z) -> if#(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
  TRS:
   -(x,0()) -> x
   -(s(x),s(y)) -> -(x,y)
   *(x,0()) -> 0()
   *(x,s(y)) -> +(*(x,y),x)
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   odd(0()) -> false()
   odd(s(0())) -> true()
   odd(s(s(x))) -> odd(x)
   half(0()) -> 0()
   half(s(0())) -> 0()
   half(s(s(x))) -> s(half(x))
   if(true(),x,y) -> true()
   if(false(),x,y) -> false()
   pow(x,y) -> f(x,y,s(0()))
   f(x,0(),z) -> z
   f(x,s(y),z) -> if(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
  Usable Rule Processor:
   DPs:
    -#(s(x),s(y)) -> -#(x,y)
    *#(x,s(y)) -> *#(x,y)
    odd#(s(s(x))) -> odd#(x)
    half#(s(s(x))) -> half#(x)
    pow#(x,y) -> f#(x,y,s(0()))
    f#(x,s(y),z) -> half#(s(y))
    f#(x,s(y),z) -> *#(x,x)
    f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z)
    f#(x,s(y),z) -> *#(x,z)
    f#(x,s(y),z) -> f#(x,y,*(x,z))
    f#(x,s(y),z) -> odd#(s(y))
    f#(x,s(y),z) -> if#(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
   TRS:
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
    half(0()) -> 0()
    *(x,0()) -> 0()
    *(x,s(y)) -> +(*(x,y),x)
    f(x,0(),z) -> z
    f(x,s(y),z) -> if(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    if(true(),x,y) -> true()
    if(false(),x,y) -> false()
    odd(s(0())) -> true()
    odd(s(s(x))) -> odd(x)
    odd(0()) -> false()
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
     half(0()) -> 0()
     *(x,0()) -> 0()
     *(x,s(y)) -> +(*(x,y),x)
    interpretation:
     [f#](x0, x1, x2) = 2x0 + 3x1 + x2,
     
     [pow#](x0, x1) = 5/2x0 + 3x1 + 3/2,
     
     [half#](x0) = x0 + 1/2,
     
     [odd#](x0) = 5/2x0,
     
     [if#](x0, x1, x2) = 3/2,
     
     [*#](x0, x1) = 1/2x1 + 2,
     
     [-#](x0, x1) = 3x0 + 2x1 + 7/2,
     
     [f](x0, x1, x2) = 2x0 + x2 + 1,
     
     [half](x0) = 1/2x0,
     
     [odd](x0) = x0,
     
     [false] = 2,
     
     [if](x0, x1, x2) = 1/2x0 + x1 + 5/2x2 + 3/2,
     
     [true] = 3,
     
     [+](x0, x1) = 0,
     
     [*](x0, x1) = 1/2x1 + 1/2,
     
     [s](x0) = 2x0 + 1,
     
     [0] = 0
    orientation:
     -#(s(x),s(y)) = 6x + 4y + 17/2 >= 3x + 2y + 7/2 = -#(x,y)
     
     *#(x,s(y)) = y + 5/2 >= 1/2y + 2 = *#(x,y)
     
     odd#(s(s(x))) = 10x + 15/2 >= 5/2x = odd#(x)
     
     half#(s(s(x))) = 4x + 7/2 >= x + 1/2 = half#(x)
     
     pow#(x,y) = 5/2x + 3y + 3/2 >= 2x + 3y + 1 = f#(x,y,s(0()))
     
     f#(x,s(y),z) = 2x + 6y + z + 3 >= 2y + 3/2 = half#(s(y))
     
     f#(x,s(y),z) = 2x + 6y + z + 3 >= 1/2x + 2 = *#(x,x)
     
     f#(x,s(y),z) = 2x + 6y + z + 3 >= x + 3y + z + 5/2 = f#(*(x,x),half(s(y)),z)
     
     f#(x,s(y),z) = 2x + 6y + z + 3 >= 1/2z + 2 = *#(x,z)
     
     f#(x,s(y),z) = 2x + 6y + z + 3 >= 2x + 3y + 1/2z + 1/2 = f#(x,y,*(x,z))
     
     f#(x,s(y),z) = 2x + 6y + z + 3 >= 5y + 5/2 = odd#(s(y))
     
     f#(x,s(y),z) = 2x + 6y + z + 3 >= 3/2 = if#(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
     
     half(s(0())) = 1/2 >= 0 = 0()
     
     half(s(s(x))) = 2x + 3/2 >= x + 1 = s(half(x))
     
     half(0()) = 0 >= 0 = 0()
     
     *(x,0()) = 1/2 >= 0 = 0()
     
     *(x,s(y)) = y + 1 >= 0 = +(*(x,y),x)
     
     f(x,0(),z) = 2x + z + 1 >= z = z
     
     f(x,s(y),z) = 2x + z + 1 >= 9/2x + y + 3z + 17/2 = if(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
     
     if(true(),x,y) = x + 5/2y + 3 >= x = x
     
     if(false(),x,y) = x + 5/2y + 5/2 >= y = y
     
     if(true(),x,y) = x + 5/2y + 3 >= 3 = true()
     
     if(false(),x,y) = x + 5/2y + 5/2 >= 2 = false()
     
     odd(s(0())) = 1 >= 3 = true()
     
     odd(s(s(x))) = 4x + 3 >= x = odd(x)
     
     odd(0()) = 0 >= 2 = false()
    problem:
     DPs:
      
     TRS:
      half(s(0())) -> 0()
      half(s(s(x))) -> s(half(x))
      half(0()) -> 0()
      *(x,0()) -> 0()
      *(x,s(y)) -> +(*(x,y),x)
      f(x,0(),z) -> z
      f(x,s(y),z) -> if(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
      if(true(),x,y) -> x
      if(false(),x,y) -> y
      if(true(),x,y) -> true()
      if(false(),x,y) -> false()
      odd(s(0())) -> true()
      odd(s(s(x))) -> odd(x)
      odd(0()) -> false()
    Qed