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))
  TDG 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))
   graph:
    f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z) ->
    f#(x,s(y),z) -> if#(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
    f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z) ->
    f#(x,s(y),z) -> odd#(s(y))
    f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z) ->
    f#(x,s(y),z) -> f#(x,y,*(x,z))
    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,x),half(s(y)),z) ->
    f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z)
    f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z) ->
    f#(x,s(y),z) -> *#(x,x)
    f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z) ->
    f#(x,s(y),z) -> half#(s(y))
    f#(x,s(y),z) -> f#(x,y,*(x,z)) ->
    f#(x,s(y),z) -> if#(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
    f#(x,s(y),z) -> f#(x,y,*(x,z)) -> f#(x,s(y),z) -> odd#(s(y))
    f#(x,s(y),z) -> f#(x,y,*(x,z)) -> f#(x,s(y),z) -> f#(x,y,*(x,z))
    f#(x,s(y),z) -> f#(x,y,*(x,z)) -> f#(x,s(y),z) -> *#(x,z)
    f#(x,s(y),z) -> f#(x,y,*(x,z)) ->
    f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z)
    f#(x,s(y),z) -> f#(x,y,*(x,z)) -> f#(x,s(y),z) -> *#(x,x)
    f#(x,s(y),z) -> f#(x,y,*(x,z)) -> f#(x,s(y),z) -> half#(s(y))
    f#(x,s(y),z) -> half#(s(y)) -> half#(s(s(x))) -> half#(x)
    f#(x,s(y),z) -> odd#(s(y)) -> odd#(s(s(x))) -> odd#(x)
    f#(x,s(y),z) -> *#(x,z) -> *#(x,s(y)) -> *#(x,y)
    f#(x,s(y),z) -> *#(x,x) -> *#(x,s(y)) -> *#(x,y)
    pow#(x,y) -> f#(x,y,s(0())) ->
    f#(x,s(y),z) -> if#(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z))
    pow#(x,y) -> f#(x,y,s(0())) -> f#(x,s(y),z) -> odd#(s(y))
    pow#(x,y) -> f#(x,y,s(0())) -> f#(x,s(y),z) -> f#(x,y,*(x,z))
    pow#(x,y) -> f#(x,y,s(0())) -> f#(x,s(y),z) -> *#(x,z)
    pow#(x,y) -> f#(x,y,s(0())) ->
    f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z)
    pow#(x,y) -> f#(x,y,s(0())) -> f#(x,s(y),z) -> *#(x,x)
    pow#(x,y) -> f#(x,y,s(0())) -> f#(x,s(y),z) -> half#(s(y))
    half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x)
    odd#(s(s(x))) -> odd#(x) -> odd#(s(s(x))) -> odd#(x)
    *#(x,s(y)) -> *#(x,y) -> *#(x,s(y)) -> *#(x,y)
    -#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y)
   SCC Processor:
    #sccs: 5
    #rules: 6
    #arcs: 29/144
    DPs:
     -#(s(x),s(y)) -> -#(x,y)
    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:
      [-#](x0, x1) = 2x1 + 1/2,
      
      [f](x0, x1, x2) = x2,
      
      [pow](x0, x1) = 2x0 + 2,
      
      [half](x0) = x0 + 1,
      
      [odd](x0) = x0 + 1,
      
      [false] = 0,
      
      [if](x0, x1, x2) = 2x1 + x2,
      
      [true] = 0,
      
      [+](x0, x1) = 0,
      
      [*](x0, x1) = 0,
      
      [s](x0) = 3x0 + 2,
      
      [-](x0, x1) = 2x0 + 3/2x1 + 7/2,
      
      [0] = 0
     orientation:
      -#(s(x),s(y)) = 6y + 9/2 >= 2y + 1/2 = -#(x,y)
      
      -(x,0()) = 2x + 7/2 >= x = x
      
      -(s(x),s(y)) = 6x + 9/2y + 21/2 >= 2x + 3/2y + 7/2 = -(x,y)
      
      *(x,0()) = 0 >= 0 = 0()
      
      *(x,s(y)) = 0 >= 0 = +(*(x,y),x)
      
      if(true(),x,y) = 2x + y >= x = x
      
      if(false(),x,y) = 2x + y >= y = y
      
      odd(0()) = 1 >= 0 = false()
      
      odd(s(0())) = 3 >= 0 = true()
      
      odd(s(s(x))) = 9x + 9 >= x + 1 = odd(x)
      
      half(0()) = 1 >= 0 = 0()
      
      half(s(0())) = 3 >= 0 = 0()
      
      half(s(s(x))) = 9x + 9 >= 3x + 5 = s(half(x))
      
      if(true(),x,y) = 2x + y >= 0 = true()
      
      if(false(),x,y) = 2x + y >= 0 = false()
      
      pow(x,y) = 2x + 2 >= 2 = f(x,y,s(0()))
      
      f(x,0(),z) = z >= z = z
      
      f(x,s(y),z) = z >= z = 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
    
    DPs:
     f#(x,s(y),z) -> f#(*(x,x),half(s(y)),z)
     f#(x,s(y),z) -> f#(x,y,*(x,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) = x1,
      
      [f](x0, x1, x2) = 2x2,
      
      [pow](x0, x1) = 2x0 + 2x1 + 2,
      
      [half](x0) = 1/2x0,
      
      [odd](x0) = x0 + 2,
      
      [false] = 0,
      
      [if](x0, x1, x2) = x1 + x2,
      
      [true] = 0,
      
      [+](x0, x1) = 0,
      
      [*](x0, x1) = 0,
      
      [s](x0) = x0 + 1,
      
      [-](x0, x1) = x0 + 3x1 + 1,
      
      [0] = 0
     orientation:
      f#(x,s(y),z) = y + 1 >= 1/2y + 1/2 = f#(*(x,x),half(s(y)),z)
      
      f#(x,s(y),z) = y + 1 >= y = f#(x,y,*(x,z))
      
      -(x,0()) = x + 1 >= x = x
      
      -(s(x),s(y)) = x + 3y + 5 >= x + 3y + 1 = -(x,y)
      
      *(x,0()) = 0 >= 0 = 0()
      
      *(x,s(y)) = 0 >= 0 = +(*(x,y),x)
      
      if(true(),x,y) = x + y >= x = x
      
      if(false(),x,y) = x + y >= y = y
      
      odd(0()) = 2 >= 0 = false()
      
      odd(s(0())) = 3 >= 0 = true()
      
      odd(s(s(x))) = x + 4 >= x + 2 = odd(x)
      
      half(0()) = 0 >= 0 = 0()
      
      half(s(0())) = 1/2 >= 0 = 0()
      
      half(s(s(x))) = 1/2x + 1 >= 1/2x + 1 = s(half(x))
      
      if(true(),x,y) = x + y >= 0 = true()
      
      if(false(),x,y) = x + y >= 0 = false()
      
      pow(x,y) = 2x + 2y + 2 >= 2 = f(x,y,s(0()))
      
      f(x,0(),z) = 2z >= z = z
      
      f(x,s(y),z) = 2z >= 2z = 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
    
    DPs:
     odd#(s(s(x))) -> odd#(x)
    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:
      [odd#](x0) = x0 + 2,
      
      [f](x0, x1, x2) = 4x2,
      
      [pow](x0, x1) = x0 + 2x1 + 4,
      
      [half](x0) = x0 + 1,
      
      [odd](x0) = 0,
      
      [false] = 0,
      
      [if](x0, x1, x2) = 4x1 + x2,
      
      [true] = 0,
      
      [+](x0, x1) = 0,
      
      [*](x0, x1) = 0,
      
      [s](x0) = 4x0 + 1,
      
      [-](x0, x1) = 2x0 + 4x1 + 2,
      
      [0] = 0
     orientation:
      odd#(s(s(x))) = 16x + 7 >= x + 2 = odd#(x)
      
      -(x,0()) = 2x + 2 >= x = x
      
      -(s(x),s(y)) = 8x + 16y + 8 >= 2x + 4y + 2 = -(x,y)
      
      *(x,0()) = 0 >= 0 = 0()
      
      *(x,s(y)) = 0 >= 0 = +(*(x,y),x)
      
      if(true(),x,y) = 4x + y >= x = x
      
      if(false(),x,y) = 4x + y >= y = y
      
      odd(0()) = 0 >= 0 = false()
      
      odd(s(0())) = 0 >= 0 = true()
      
      odd(s(s(x))) = 0 >= 0 = odd(x)
      
      half(0()) = 1 >= 0 = 0()
      
      half(s(0())) = 2 >= 0 = 0()
      
      half(s(s(x))) = 16x + 6 >= 4x + 5 = s(half(x))
      
      if(true(),x,y) = 4x + y >= 0 = true()
      
      if(false(),x,y) = 4x + y >= 0 = false()
      
      pow(x,y) = x + 2y + 4 >= 4 = f(x,y,s(0()))
      
      f(x,0(),z) = 4z >= z = z
      
      f(x,s(y),z) = 4z >= 4z = 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
   
   DPs:
    *#(x,s(y)) -> *#(x,y)
   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:
     [*#](x0, x1) = 4x1,
     
     [f](x0, x1, x2) = x2,
     
     [pow](x0, x1) = 4x1 + 4,
     
     [half](x0) = x0 + 2,
     
     [odd](x0) = 1,
     
     [false] = 0,
     
     [if](x0, x1, x2) = 2x1 + x2,
     
     [true] = 0,
     
     [+](x0, x1) = 0,
     
     [*](x0, x1) = 0,
     
     [s](x0) = 4x0 + 4,
     
     [-](x0, x1) = 2x0 + 4x1 + 2,
     
     [0] = 0
    orientation:
     *#(x,s(y)) = 16y + 16 >= 4y = *#(x,y)
     
     -(x,0()) = 2x + 2 >= x = x
     
     -(s(x),s(y)) = 8x + 16y + 26 >= 2x + 4y + 2 = -(x,y)
     
     *(x,0()) = 0 >= 0 = 0()
     
     *(x,s(y)) = 0 >= 0 = +(*(x,y),x)
     
     if(true(),x,y) = 2x + y >= x = x
     
     if(false(),x,y) = 2x + y >= y = y
     
     odd(0()) = 1 >= 0 = false()
     
     odd(s(0())) = 1 >= 0 = true()
     
     odd(s(s(x))) = 1 >= 1 = odd(x)
     
     half(0()) = 2 >= 0 = 0()
     
     half(s(0())) = 6 >= 0 = 0()
     
     half(s(s(x))) = 16x + 22 >= 4x + 12 = s(half(x))
     
     if(true(),x,y) = 2x + y >= 0 = true()
     
     if(false(),x,y) = 2x + y >= 0 = false()
     
     pow(x,y) = 4y + 4 >= 4 = f(x,y,s(0()))
     
     f(x,0(),z) = z >= z = z
     
     f(x,s(y),z) = z >= z = 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
   
   DPs:
    half#(s(s(x))) -> half#(x)
   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:
     [half#](x0) = x0 + 2,
     
     [f](x0, x1, x2) = 4x2,
     
     [pow](x0, x1) = x0 + 2x1 + 4,
     
     [half](x0) = x0 + 1,
     
     [odd](x0) = 0,
     
     [false] = 0,
     
     [if](x0, x1, x2) = 4x1 + x2,
     
     [true] = 0,
     
     [+](x0, x1) = 0,
     
     [*](x0, x1) = 0,
     
     [s](x0) = 4x0 + 1,
     
     [-](x0, x1) = 2x0 + 4x1 + 2,
     
     [0] = 0
    orientation:
     half#(s(s(x))) = 16x + 7 >= x + 2 = half#(x)
     
     -(x,0()) = 2x + 2 >= x = x
     
     -(s(x),s(y)) = 8x + 16y + 8 >= 2x + 4y + 2 = -(x,y)
     
     *(x,0()) = 0 >= 0 = 0()
     
     *(x,s(y)) = 0 >= 0 = +(*(x,y),x)
     
     if(true(),x,y) = 4x + y >= x = x
     
     if(false(),x,y) = 4x + y >= y = y
     
     odd(0()) = 0 >= 0 = false()
     
     odd(s(0())) = 0 >= 0 = true()
     
     odd(s(s(x))) = 0 >= 0 = odd(x)
     
     half(0()) = 1 >= 0 = 0()
     
     half(s(0())) = 2 >= 0 = 0()
     
     half(s(s(x))) = 16x + 6 >= 4x + 5 = s(half(x))
     
     if(true(),x,y) = 4x + y >= 0 = true()
     
     if(false(),x,y) = 4x + y >= 0 = false()
     
     pow(x,y) = x + 2y + 4 >= 4 = f(x,y,s(0()))
     
     f(x,0(),z) = 4z >= z = z
     
     f(x,s(y),z) = 4z >= 4z = 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