YES(?,O(n^1))

Problem:
 a() -> g(c())
 g(a()) -> b()
 f(g(X),b()) -> f(a(),X)

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {6}
   transitions:
    c3() -> 13*
    f1(10,6) -> 6*
    f1(10,8) -> 6*
    a1() -> 10*
    b1() -> 6*
    g1(8) -> 6*
    c1() -> 8*
    g2(11) -> 10*
    a0() -> 6*
    c2() -> 11*
    g0(6) -> 6*
    f2(12,11) -> 6*
    c0() -> 6*
    a2() -> 12*
    b0() -> 6*
    g3(13) -> 12*
    f0(6,6) -> 6*
  problem:
   
  Qed