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: 3
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    s3(37) -> 38*
    f1(10) -> 11*
    f1(19) -> 20*
    f1(11) -> 12*
    03() -> 37*
    s1(7) -> 8*
    s1(9) -> 10*
    01() -> 7*
    f2(25) -> 26*
    f2(24) -> 25*
    f2(41) -> 42*
    f0(4) -> 4*
    s2(33) -> 34*
    s2(23) -> 24*
    00() -> 4*
    02() -> 33*
    s0(4) -> 4*
    4 -> 9*
    7 -> 23*
    8 -> 11,4
    12 -> 11,19,4
    20 -> 4*
    26 -> 41,11
    34 -> 20,25,12
    38 -> 42,26,11
    42 -> 11*
  problem:
   
  Qed