MAYBE
Time: 0.034419
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(true(), x, y) -> true(),
  if(false(), x, y) -> y,
  if(false(), x, y) -> false(),
            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,
       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)),
          pow(x, y) -> f(x, y, s 0())}
 DP:
  DP:
   { -#(s x, s y) -> -#(x, y),
       *#(x, s y) -> *#(x, y),
       odd# s s x -> odd# x,
      half# s s x -> half# x,
    f#(x, s y, z) -> *#(x, x),
    f#(x, s y, z) -> *#(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) -> odd# s y,
    f#(x, s y, z) -> half# s y,
    f#(x, s y, z) -> f#(x, y, *(x, z)),
    f#(x, s y, z) -> f#(*(x, x), half s y, z),
       pow#(x, y) -> f#(x, y, s 0())}
  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(true(), x, y) -> true(),
   if(false(), x, y) -> y,
   if(false(), x, y) -> false(),
             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,
        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)),
           pow(x, y) -> f(x, y, s 0())}
  EDG:
   {(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) -> f#(x, y, *(x, z)))
    (pow#(x, y) -> f#(x, y, s 0()), f#(x, s y, z) -> half# s y)
    (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) -> 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) -> *#(x, z))
    (pow#(x, y) -> f#(x, y, s 0()), f#(x, s y, z) -> *#(x, x))
    (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
    (f#(x, s y, z) -> *#(x, x), *#(x, s y) -> *#(x, y))
    (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) -> f#(x, y, *(x, z)))
    (f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> half# s y)
    (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) -> 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) -> *#(x, z))
    (f#(x, s y, z) -> f#(x, y, *(x, z)), f#(x, s y, z) -> *#(x, x))
    (half# s s x -> half# x, half# s s x -> half# x)
    (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)
    (odd# s s x -> odd# x, odd# s s x -> odd# x)
    (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y))
    (f#(x, s y, z) -> *#(x, z), *#(x, s y) -> *#(x, y))
    (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) -> *#(x, z))
    (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) -> half# 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) -> f#(*(x, x), half s y, z))}
   SCCS (5):
    Scc:
     {f#(x, s y, z) -> f#(x, y, *(x, z)),
      f#(x, s y, z) -> f#(*(x, x), half s y, z)}
    Scc:
     {half# s s x -> half# x}
    Scc:
     {odd# s s x -> odd# x}
    Scc:
     {*#(x, s y) -> *#(x, y)}
    Scc:
     {-#(s x, s y) -> -#(x, y)}
    SCC (2):
     Strict:
      {f#(x, s y, z) -> f#(x, y, *(x, z)),
       f#(x, s y, z) -> f#(*(x, x), half s y, z)}
     Weak:
     {        -(x, 0()) -> x,
            -(s x, s y) -> -(x, y),
              *(x, 0()) -> 0(),
              *(x, s y) -> +(*(x, y), x),
       if(true(), x, y) -> x,
       if(true(), x, y) -> true(),
      if(false(), x, y) -> y,
      if(false(), x, y) -> false(),
                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,
           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)),
              pow(x, y) -> f(x, y, s 0())}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2) = x0 + 1,
       
       [f](x0, x1, x2) = x0 + x1 + 1,
       
       [-](x0, x1) = x0 + 1,
       
       [*](x0, x1) = x0 + x1 + 1,
       
       [+](x0, x1) = x0 + x1 + 1,
       
       [pow](x0, x1) = 0,
       
       [s](x0) = x0 + 1,
       
       [odd](x0) = x0 + 1,
       
       [half](x0) = x0,
       
       [0] = 1,
       
       [true] = 1,
       
       [false] = 1,
       
       [f#](x0, x1, x2) = x0
      Strict:
       f#(x, s y, z) -> f#(*(x, x), half s y, z)
       1 + 0x + 1y + 0z >= 1 + 0x + 1y + 0z
       f#(x, s y, z) -> f#(x, y, *(x, z))
       1 + 0x + 1y + 0z >= 0 + 0x + 1y + 0z
      Weak:
       
     EDG:
      {(f#(x, s y, z) -> f#(*(x, x), half s y, z), f#(x, s y, z) -> f#(*(x, x), half s y, z))}
      SCCS (1):
       Scc:
        {f#(x, s y, z) -> f#(*(x, x), half s y, z)}
       SCC (1):
        Strict:
         {f#(x, s y, z) -> f#(*(x, x), half s y, z)}
        Weak:
        {        -(x, 0()) -> x,
               -(s x, s y) -> -(x, y),
                 *(x, 0()) -> 0(),
                 *(x, s y) -> +(*(x, y), x),
          if(true(), x, y) -> x,
          if(true(), x, y) -> true(),
         if(false(), x, y) -> y,
         if(false(), x, y) -> false(),
                   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,
              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)),
                 pow(x, y) -> f(x, y, s 0())}
        Fail
   SCC (1):
    Strict:
     {half# s s x -> half# x}
    Weak:
    {        -(x, 0()) -> x,
           -(s x, s y) -> -(x, y),
             *(x, 0()) -> 0(),
             *(x, s y) -> +(*(x, y), x),
      if(true(), x, y) -> x,
      if(true(), x, y) -> true(),
     if(false(), x, y) -> y,
     if(false(), x, y) -> false(),
               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,
          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)),
             pow(x, y) -> f(x, y, s 0())}
    SPSC:
     Simple Projection:
      pi(half#) = 0
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {odd# s s x -> odd# x}
    Weak:
    {        -(x, 0()) -> x,
           -(s x, s y) -> -(x, y),
             *(x, 0()) -> 0(),
             *(x, s y) -> +(*(x, y), x),
      if(true(), x, y) -> x,
      if(true(), x, y) -> true(),
     if(false(), x, y) -> y,
     if(false(), x, y) -> false(),
               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,
          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)),
             pow(x, y) -> f(x, y, s 0())}
    SPSC:
     Simple Projection:
      pi(odd#) = 0
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {*#(x, s y) -> *#(x, y)}
    Weak:
    {        -(x, 0()) -> x,
           -(s x, s y) -> -(x, y),
             *(x, 0()) -> 0(),
             *(x, s y) -> +(*(x, y), x),
      if(true(), x, y) -> x,
      if(true(), x, y) -> true(),
     if(false(), x, y) -> y,
     if(false(), x, y) -> false(),
               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,
          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)),
             pow(x, y) -> f(x, y, s 0())}
    SPSC:
     Simple Projection:
      pi(*#) = 1
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {-#(s x, s y) -> -#(x, y)}
    Weak:
    {        -(x, 0()) -> x,
           -(s x, s y) -> -(x, y),
             *(x, 0()) -> 0(),
             *(x, s y) -> +(*(x, y), x),
      if(true(), x, y) -> x,
      if(true(), x, y) -> true(),
     if(false(), x, y) -> y,
     if(false(), x, y) -> false(),
               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,
          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)),
             pow(x, y) -> f(x, y, s 0())}
    SPSC:
     Simple Projection:
      pi(-#) = 1
     Strict:
      {}
     Qed