YES(?,O(n^1))

Problem:
 c(b(a(X))) -> a(a(b(b(c(c(X))))))
 a(X) -> e()
 b(X) -> e()
 c(X) -> e()

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {5}
   transitions:
    e1() -> 20*
    a1(17) -> 18*
    a1(18) -> 19*
    b1(15) -> 16*
    b1(16) -> 17*
    c1(25) -> 26*
    c1(14) -> 15*
    c1(13) -> 14*
    e2() -> 30*
    c0(5) -> 5*
    b0(5) -> 5*
    a0(5) -> 5*
    e0() -> 5*
    5 -> 13*
    18 -> 25*
    19 -> 14,5
    20 -> 5*
    26 -> 14*
    30 -> 26,15,16,17,18,19
  problem:
   
  Qed