YES(?,O(n^1))

Problem:
 f(0()) -> s(0())
 f(s(0())) -> s(0())
 f(s(s(x))) -> f(f(s(x)))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    f1(10) -> 11*
    f1(9) -> 10*
    s1(6) -> 7*
    s1(18) -> 19*
    s1(8) -> 9*
    01() -> 6*
    s2(20) -> 21*
    f0(2) -> 3*
    f0(1) -> 3*
    02() -> 20*
    00() -> 1*
    s0(2) -> 2*
    s0(1) -> 2*
    1 -> 18*
    2 -> 8*
    7 -> 10,3
    11 -> 10,3
    19 -> 9*
    21 -> 11,10,3
  problem:
   
  Qed