YES

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

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