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))
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [f#](x0, x1, x2) = 2x0 + 2x1 + 1/2x2,
    
    [pow#](x0, x1) = 5/2x0 + 5/2x1 + 1,
    
    [half#](x0) = 1/2x0,
    
    [odd#](x0) = x0 + 1/2,
    
    [if#](x0, x1, x2) = 1/2x2 + 1/2,
    
    [*#](x0, x1) = 3/2x0 + 1/2x1,
    
    [-#](x0, x1) = 5/2x1,
    
    [f](x0, x1, x2) = 2x0 + 2x1 + x2,
    
    [pow](x0, x1) = 2x0 + 5/2x1 + 1,
    
    [half](x0) = 1/2x0,
    
    [odd](x0) = 0,
    
    [false] = 0,
    
    [if](x0, x1, x2) = x1 + x2 + 1,
    
    [true] = 0,
    
    [+](x0, x1) = 0,
    
    [*](x0, x1) = 0,
    
    [s](x0) = 2x0 + 1,
    
    [-](x0, x1) = 7/2x0 + 3/2x1 + 1,
    
    [0] = 0
   orientation:
    -#(s(x),s(y)) = 5y + 5/2 >= 5/2y = -#(x,y)
    
    *#(x,s(y)) = 3/2x + y + 1/2 >= 3/2x + 1/2y = *#(x,y)
    
    odd#(s(s(x))) = 4x + 7/2 >= x + 1/2 = odd#(x)
    
    half#(s(s(x))) = 2x + 3/2 >= 1/2x = half#(x)
    
    pow#(x,y) = 5/2x + 5/2y + 1 >= 2x + 2y + 1/2 = f#(x,y,s(0()))
    
    f#(x,s(y),z) = 2x + 4y + 1/2z + 2 >= y + 1/2 = half#(s(y))
    
    f#(x,s(y),z) = 2x + 4y + 1/2z + 2 >= 2x = *#(x,x)
    
    f#(x,s(y),z) = 2x + 4y + 1/2z + 2 >= 2y + 1/2z + 1 = f#(*(x,x),half(s(y)),z)
    
    f#(x,s(y),z) = 2x + 4y + 1/2z + 2 >= 3/2x + 1/2z = *#(x,z)
    
    f#(x,s(y),z) = 2x + 4y + 1/2z + 2 >= 2x + 2y = f#(x,y,*(x,z))
    
    f#(x,s(y),z) = 2x + 4y + 1/2z + 2 >= 2y + 3/2 = odd#(s(y))
    
    f#(x,s(y),z) = 2x + 4y + 1/2z + 2 >= y + 1/2z + 1 = if#(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
    
    -(x,0()) = 7/2x + 1 >= x = x
    
    -(s(x),s(y)) = 7x + 3y + 6 >= 7/2x + 3/2y + 1 = -(x,y)
    
    *(x,0()) = 0 >= 0 = 0()
    
    *(x,s(y)) = 0 >= 0 = +(*(x,y),x)
    
    if(true(),x,y) = x + y + 1 >= x = x
    
    if(false(),x,y) = x + y + 1 >= y = y
    
    odd(0()) = 0 >= 0 = false()
    
    odd(s(0())) = 0 >= 0 = true()
    
    odd(s(s(x))) = 0 >= 0 = odd(x)
    
    half(0()) = 0 >= 0 = 0()
    
    half(s(0())) = 1/2 >= 0 = 0()
    
    half(s(s(x))) = 2x + 3/2 >= x + 1 = s(half(x))
    
    if(true(),x,y) = x + y + 1 >= 0 = true()
    
    if(false(),x,y) = x + y + 1 >= 0 = false()
    
    pow(x,y) = 2x + 5/2y + 1 >= 2x + 2y + 1 = f(x,y,s(0()))
    
    f(x,0(),z) = 2x + z >= z = z
    
    f(x,s(y),z) = 2x + 4y + z + 2 >= 2x + 4y + z + 2 = if(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
   problem:
    DPs:
     
    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))
   Qed