YES(?,O(n^1))

Problem:
 f(f(x,a()),a()) -> f(f(f(a(),a()),f(x,a())),a())

Proof:
 RT Transformation Processor:
  strict:
   f(f(x,a()),a()) -> f(f(f(a(),a()),f(x,a())),a())
  weak:
   
  Bounds Processor:
   bound: 2
   enrichment: match-rt
   automaton:
    final states: {2,1}
    transitions:
     f1(4,4) -> 6*
     f1(1,4) -> 5*
     f1(6,1) -> 7*
     f1(6,5) -> 7*
     f1(7,4) -> 5,1
     f1(2,4) -> 5*
     a1() -> 4*
     f2(7,16) -> 17*
     f2(18,17) -> 19*
     f2(19,16) -> 5*
     f2(16,16) -> 18*
     f0(1,2) -> 1*
     f0(2,1) -> 1*
     f0(1,1) -> 1*
     f0(2,2) -> 1*
     a2() -> 16*
     a0() -> 2*
   problem:
    strict:
     
    weak:
     f(f(x,a()),a()) -> f(f(f(a(),a()),f(x,a())),a())
   Qed