YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {9,8}
   transitions:
    e1(20) -> 21*
    e1(22) -> 23*
    f1(14) -> 15*
    d1(16) -> 17*
    d1(18) -> 19*
    a1() -> 13*
    b1() -> 16*
    c1(13) -> 14*
    f2(29) -> 30*
    d2(28) -> 29*
    f0(9) -> 8*
    f0(8) -> 8*
    b2() -> 28*
    a0() -> 8*
    c0(9) -> 8*
    c0(8) -> 8*
    d0(9) -> 8*
    d0(8) -> 8*
    b0() -> 8*
    e0(9) -> 8*
    e0(8) -> 8*
    g0(9) -> 9*
    g0(8) -> 9*
    8 -> 22*
    9 -> 20,8
    13 -> 15,8,18
    15 -> 8*
    16 -> 15,8
    17 -> 14*
    18 -> 15,8
    19 -> 14*
    21 -> 8*
    23 -> 21,8
    28 -> 30,15
    30 -> 15,8
  problem:
   
  Qed