YES(?,O(n^1))

Problem:
 not(true()) -> false()
 not(false()) -> true()
 odd(0()) -> false()
 odd(s(x)) -> not(odd(x))
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 +(s(x),y) -> s(+(x,y))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {7,6,5}
   transitions:
    s1(10) -> 10,7
    +1(3,1) -> 10*
    +1(3,3) -> 10*
    +1(4,2) -> 10*
    +1(4,4) -> 10*
    +1(1,2) -> 10*
    +1(1,4) -> 10*
    +1(2,1) -> 10*
    +1(2,3) -> 10*
    +1(3,2) -> 10*
    +1(3,4) -> 10*
    +1(4,1) -> 10*
    +1(4,3) -> 10*
    +1(1,1) -> 10*
    +1(1,3) -> 10*
    +1(2,2) -> 10*
    +1(2,4) -> 10*
    not1(8) -> 8,6
    odd1(2) -> 8*
    odd1(4) -> 8*
    odd1(1) -> 8*
    odd1(3) -> 8*
    false1() -> 8,6,5
    true1() -> 5*
    true2() -> 6,8
    false2() -> 6,8
    not0(2) -> 5*
    not0(4) -> 5*
    not0(1) -> 5*
    not0(3) -> 5*
    true0() -> 1*
    false0() -> 2*
    odd0(2) -> 6*
    odd0(4) -> 6*
    odd0(1) -> 6*
    odd0(3) -> 6*
    00() -> 3*
    s0(2) -> 4*
    s0(4) -> 4*
    s0(1) -> 4*
    s0(3) -> 4*
    +0(3,1) -> 7*
    +0(3,3) -> 7*
    +0(4,2) -> 7*
    +0(4,4) -> 7*
    +0(1,2) -> 7*
    +0(1,4) -> 7*
    +0(2,1) -> 7*
    +0(2,3) -> 7*
    +0(3,2) -> 7*
    +0(3,4) -> 7*
    +0(4,1) -> 7*
    +0(4,3) -> 7*
    +0(1,1) -> 7*
    +0(1,3) -> 7*
    +0(2,2) -> 7*
    +0(2,4) -> 7*
    1 -> 10,7
    2 -> 10,7
    3 -> 10,7
    4 -> 10,7
  problem:
   
  Qed