YES(?,O(n^1))

Problem:
 f(g(f(a()),h(a(),f(a())))) -> f(h(g(f(a()),a()),g(f(a()),f(a()))))

Proof:
 RT Transformation Processor:
  strict:
   f(g(f(a()),h(a(),f(a())))) -> f(h(g(f(a()),a()),g(f(a()),f(a()))))
  weak:
   
  Bounds Processor:
   bound: 1
   enrichment: match-rt
   automaton:
    final states: {4,3,2,1}
    transitions:
     f1(12) -> 1*
     f1(6) -> 10,8,7
     h1(11,9) -> 12*
     g1(8,7) -> 9*
     g1(10,6) -> 11*
     a1() -> 6*
     f0(2) -> 1*
     f0(4) -> 1*
     f0(1) -> 1*
     f0(3) -> 1*
     g0(3,1) -> 2*
     g0(3,3) -> 2*
     g0(4,2) -> 2*
     g0(4,4) -> 2*
     g0(1,2) -> 2*
     g0(1,4) -> 2*
     g0(2,1) -> 2*
     g0(2,3) -> 2*
     g0(3,2) -> 2*
     g0(3,4) -> 2*
     g0(4,1) -> 2*
     g0(4,3) -> 2*
     g0(1,1) -> 2*
     g0(1,3) -> 2*
     g0(2,2) -> 2*
     g0(2,4) -> 2*
     a0() -> 3*
     h0(3,1) -> 4*
     h0(3,3) -> 4*
     h0(4,2) -> 4*
     h0(4,4) -> 4*
     h0(1,2) -> 4*
     h0(1,4) -> 4*
     h0(2,1) -> 4*
     h0(2,3) -> 4*
     h0(3,2) -> 4*
     h0(3,4) -> 4*
     h0(4,1) -> 4*
     h0(4,3) -> 4*
     h0(1,1) -> 4*
     h0(1,3) -> 4*
     h0(2,2) -> 4*
     h0(2,4) -> 4*
   problem:
    strict:
     
    weak:
     f(g(f(a()),h(a(),f(a())))) -> f(h(g(f(a()),a()),g(f(a()),f(a()))))
   Qed