YES

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

Proof:
 Uncurry Processor (mirror):
  a2(a1(x),x6) -> f(f(x,a1(a2(a(),a()))),x6)
  a1(a1(x)) -> f(x,a1(a2(a(),a())))
  f(a1(x4),x5) -> a2(x4,x5)
  f(a(),x5) -> a1(x5)
  Bounds Processor:
   bound: 1
   enrichment: match
   automaton:
    final states: {8,7,6,1}
    transitions:
     a0() -> 3*
     a{2,1}(5,5) -> 6*
     a{2,1}(2,5) -> 6*
     a{2,1}(9,9) -> 10*
     a{2,1}(5,2) -> 1,7
     a{2,1}(2,2) -> 1,7
     f1(12,5) -> 6*
     f1(4,11) -> 8,12
     f1(12,2) -> 1*
     a{1,1}(10) -> 11*
     a1() -> 9*
     f50() -> 2*
     f0(6,2) -> 1*
     f0(2,5) -> 6*
     f0(4,5) -> 6,8
     f0(6,5) -> 8*
     a{1,0}(5) -> 6*
     a{1,0}(2) -> 8*
     a{1,0}(4) -> 5*
     a{2,0}(3,3) -> 4*
     a{2,0}(5,5) -> 8*
     a{2,0}(2,5) -> 6*
     a{2,0}(5,2) -> 1,7
     a{2,0}(2,2) -> 1,7
     1 -> 7*
     6 -> 8*
     8 -> 6*
   problem:
    
   Qed