YES(?,O(n^1))

Problem:
 f(f(a())) -> c()

Proof:
 RT Transformation Processor:
  strict:
   f(f(a())) -> c()
  weak:
   
  Bounds Processor:
   bound: 1
   enrichment: match-rt
   automaton:
    final states: {3,2,1}
    transitions:
     c1() -> 6*
     f0(2) -> 1*
     f0(1) -> 1*
     f0(3) -> 1*
     a0() -> 2*
     c0() -> 3*
     6 -> 1*
   problem:
    strict:
     
    weak:
     f(f(a())) -> c()
   Qed