YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    01() -> 15*
    s1(15) -> 16*
    s1(18) -> 19*
    g1(25) -> 26*
    g1(17) -> 18*
    f1(7) -> 8*
    f1(9) -> 10*
    g0(2) -> 3*
    g0(1) -> 3*
    s0(2) -> 1*
    s0(1) -> 1*
    f0(2) -> 4*
    f0(1) -> 4*
    00() -> 2*
    1 -> 25,9
    2 -> 17,7
    8 -> 26,18,3
    10 -> 26,18,3
    15 -> 18,3
    16 -> 10,8,3,4
    19 -> 15*
    26 -> 18*
  problem:
   
  Qed