YES(?,O(n^1))

Problem:
 not(true()) -> false()
 not(false()) -> true()
 evenodd(x,0()) -> not(evenodd(x,s(0())))
 evenodd(0(),s(0())) -> false()
 evenodd(s(x),s(0())) -> evenodd(x,0())

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {7}
   transitions:
    false3() -> 7,16,13
    evenodd1(7,12) -> 13*
    evenodd1(7,11) -> 16,13,7
    true3() -> 13,7,16
    01() -> 11*
    false1() -> 16,13,7
    not1(13) -> 7*
    s1(11) -> 12*
    true1() -> 7*
    not2(16) -> 16,13,7
    not0(7) -> 7*
    evenodd2(7,15) -> 16*
    true0() -> 7*
    s2(14) -> 15*
    false0() -> 7*
    02() -> 14*
    evenodd0(7,7) -> 7*
    true2() -> 16,13,7
    00() -> 7*
    false2() -> 7*
    s0(7) -> 7*
  problem:
   
  Qed