YES(?,O(n^1))

Problem:
 f(s(X)) -> f(X)
 g(cons(0(),Y)) -> g(Y)
 g(cons(s(X),Y)) -> s(X)
 h(cons(X,Y)) -> h(g(cons(X,Y)))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {7,8}
   transitions:
    h1(10) -> 7*
    g1(7) -> 10,7
    g1(9) -> 10*
    g1(8) -> 10,7
    cons1(8,7) -> 9*
    cons1(7,7) -> 9*
    cons1(8,8) -> 9*
    cons1(7,8) -> 9*
    s1(7) -> 10,7
    s1(8) -> 10,7
    f1(7) -> 7*
    f1(8) -> 7*
    s2(7) -> 10*
    s2(8) -> 10*
    f2(7) -> 7*
    f2(8) -> 7*
    f0(7) -> 7*
    f0(8) -> 7*
    s0(7) -> 7*
    s0(8) -> 7*
    g0(7) -> 7*
    g0(8) -> 7*
    cons0(8,7) -> 7*
    cons0(7,7) -> 7*
    cons0(8,8) -> 7*
    cons0(7,8) -> 7*
    00() -> 8*
    h0(7) -> 7*
    h0(8) -> 7*
  problem:
   
  Qed