YES
Time: 0.039238
TRS:
 {not false() -> true(),
   not true() -> false(),
      odd 0() -> false(),
      odd s x -> not odd x,
    +(x, 0()) -> x,
    +(x, s y) -> s +(x, y),
    +(s x, y) -> s +(x, y)}
 DP:
  DP:
   {  odd# s x -> not# odd x,
      odd# s x -> odd# x,
    +#(x, s y) -> +#(x, y),
    +#(s x, y) -> +#(x, y)}
  TRS:
  {not false() -> true(),
    not true() -> false(),
       odd 0() -> false(),
       odd s x -> not odd x,
     +(x, 0()) -> x,
     +(x, s y) -> s +(x, y),
     +(s x, y) -> s +(x, y)}
  EDG:
   {(+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
    (+#(s x, y) -> +#(x, y), +#(x, s y) -> +#(x, y))
    (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
    (+#(x, s y) -> +#(x, y), +#(s x, y) -> +#(x, y))
    (odd# s x -> odd# x, odd# s x -> not# odd x)
    (odd# s x -> odd# x, odd# s x -> odd# x)}
   STATUS:
    arrows: 0.625000
    SCCS (2):
     Scc:
      {+#(x, s y) -> +#(x, y),
       +#(s x, y) -> +#(x, y)}
     Scc:
      {odd# s x -> odd# x}
     
     SCC (2):
      Strict:
       {+#(x, s y) -> +#(x, y),
        +#(s x, y) -> +#(x, y)}
      Weak:
      {not false() -> true(),
        not true() -> false(),
           odd 0() -> false(),
           odd s x -> not odd x,
         +(x, 0()) -> x,
         +(x, s y) -> s +(x, y),
         +(s x, y) -> s +(x, y)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [+](x0, x1) = x0 + 1,
        
        [not](x0) = x0 + 1,
        
        [odd](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [false] = 1,
        
        [true] = 1,
        
        [0] = 1,
        
        [+#](x0, x1) = x0
       Strict:
        +#(s x, y) -> +#(x, y)
        0 + 0x + 1y >= 0 + 0x + 1y
        +#(x, s y) -> +#(x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        +(s x, y) -> s +(x, y)
        1 + 0x + 1y >= 2 + 0x + 1y
        +(x, s y) -> s +(x, y)
        2 + 0x + 1y >= 2 + 0x + 1y
        +(x, 0()) -> x
        2 + 0x >= 1x
        odd s x -> not odd x
        0 + 0x >= 1 + 0x
        odd 0() -> false()
        0 >= 1
        not true() -> false()
        2 >= 1
        not false() -> true()
        2 >= 1
      SCCS (1):
       Scc:
        {+#(s x, y) -> +#(x, y)}
       
       SCC (1):
        Strict:
         {+#(s x, y) -> +#(x, y)}
        Weak:
        {not false() -> true(),
          not true() -> false(),
             odd 0() -> false(),
             odd s x -> not odd x,
           +(x, 0()) -> x,
           +(x, s y) -> s +(x, y),
           +(s x, y) -> s +(x, y)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [+](x0, x1) = x0 + 1,
          
          [not](x0) = x0 + 1,
          
          [odd](x0) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [false] = 1,
          
          [true] = 1,
          
          [0] = 1,
          
          [+#](x0, x1) = x0
         Strict:
          +#(s x, y) -> +#(x, y)
          1 + 1x + 0y >= 0 + 1x + 0y
         Weak:
          +(s x, y) -> s +(x, y)
          1 + 0x + 1y >= 2 + 0x + 1y
          +(x, s y) -> s +(x, y)
          2 + 0x + 1y >= 2 + 0x + 1y
          +(x, 0()) -> x
          2 + 0x >= 1x
          odd s x -> not odd x
          2 + 1x >= 2 + 1x
          odd 0() -> false()
          2 >= 1
          not true() -> false()
          2 >= 1
          not false() -> true()
          2 >= 1
        Qed
    SCC (1):
     Strict:
      {odd# s x -> odd# x}
     Weak:
     {not false() -> true(),
       not true() -> false(),
          odd 0() -> false(),
          odd s x -> not odd x,
        +(x, 0()) -> x,
        +(x, s y) -> s +(x, y),
        +(s x, y) -> s +(x, y)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [+](x0, x1) = x0 + 1,
       
       [not](x0) = x0 + 1,
       
       [odd](x0) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [false] = 1,
       
       [true] = 1,
       
       [0] = 1,
       
       [odd#](x0) = x0
      Strict:
       odd# s x -> odd# x
       1 + 1x >= 0 + 1x
      Weak:
       +(s x, y) -> s +(x, y)
       1 + 0x + 1y >= 2 + 0x + 1y
       +(x, s y) -> s +(x, y)
       2 + 0x + 1y >= 2 + 0x + 1y
       +(x, 0()) -> x
       2 + 0x >= 1x
       odd s x -> not odd x
       2 + 1x >= 2 + 1x
       odd 0() -> false()
       2 >= 1
       not true() -> false()
       2 >= 1
       not false() -> true()
       2 >= 1
     Qed