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))
    Subterm Criterion Processor:
     simple projection:
      pi(-#) = 0
     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))
    Subterm Criterion Processor:
     simple projection:
      pi(s) = [0,0]
      pi(+) = [1,1]
      pi(half) = 0
      pi(f#) = [1,1]
     problem:
      DPs:
       f#(x,s(y),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:
       f#(x,s(y),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)
      Matrix Interpretation Processor: dim=3
       
       usable rules:
        half(s(0())) -> 0()
        half(s(s(x))) -> s(half(x))
        half(0()) -> 0()
       interpretation:
        [f#](x0, x1, x2) = [1 0 0]x1,
        
                     [0 0 1]     [0]
        [half](x0) = [0 0 0]x0 + [1]
                     [1 0 0]     [0],
        
                      [0 0 0]  
        [+](x0, x1) = [0 0 0]x0
                      [1 1 0]  ,
        
                      [0 1 0]     [1]
        [*](x0, x1) = [0 0 1]x1 + [0]
                      [0 0 0]     [0],
        
                  [1 0 1]     [1]
        [s](x0) = [0 1 0]x0 + [0]
                  [1 0 0]     [0],
        
              [0]
        [0] = [0]
              [0]
       orientation:
        f#(x,s(y),z) = [1 0 1]y + [1] >= [1 0 0]y = f#(*(x,x),half(s(y)),z)
        
                       [0]    [0]      
        half(s(0())) = [1] >= [0] = 0()
                       [1]    [0]      
        
                        [1 0 1]    [1]    [1 0 1]    [1]             
        half(s(s(x))) = [0 0 0]x + [1] >= [0 0 0]x + [1] = s(half(x))
                        [2 0 1]    [2]    [0 0 1]    [0]             
        
                    [0]    [0]      
        half(0()) = [1] >= [0] = 0()
                    [0]    [0]      
        
                   [1]    [0]      
        *(x,0()) = [0] >= [0] = 0()
                   [0]    [0]      
        
                    [0 1 0]    [1]    [0 0 0]    [0]              
        *(x,s(y)) = [1 0 0]y + [0] >= [0 0 0]y + [0] = +(*(x,y),x)
                    [0 0 0]    [0]    [0 1 1]    [1]              
       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)
       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))
    Subterm Criterion Processor:
     simple projection:
      pi(odd#) = 0
     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))
    Subterm Criterion Processor:
     simple projection:
      pi(*#) = 1
     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))
    Subterm Criterion Processor:
     simple projection:
      pi(half#) = 0
     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