YES
Trs:
 {a(f(), a(f(), x)) -> a(x, g()),
          a(x, g()) -> a(f(), a(g(), a(f(), x)))}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {        g_4() -> q26,
             g_3() -> q16,
             g_2() -> q11,
             g_1() -> q4,
             g_0() -> q3,
             f_4() -> q25,
             f_3() -> q20,
             f_2() -> q12,
             f_1() -> q6 | q3,
             f_0() -> q3,
     a_4(q26, q27) -> q28,
     a_4(q25, q28) -> q13,
     a_4(q25, q14) -> q27,
     a_3(q20, q22) -> q13 | q7,
     a_3(q20, q14) -> q21,
      a_3(q20, q4) -> q21,
     a_3(q16, q21) -> q22,
     a_3(q14, q16) -> q13,
     a_2(q14, q11) -> q7,
     a_2(q12, q24) -> q21,
     a_2(q12, q20) -> q23,
     a_2(q12, q14) -> q13 | q7 | q3,
     a_2(q12, q12) -> q13,
      a_2(q12, q4) -> q13,
      a_2(q12, q3) -> q13,
     a_2(q11, q23) -> q24,
     a_2(q11, q13) -> q14,
      a_2(q4, q11) -> q13 | q7,
      a_1(q14, q4) -> q3,
       a_1(q6, q3) -> q7,
       a_1(q4, q7) -> q4,
       a_1(q4, q4) -> q13 | q7 | q3,
      a_1(q3, q12) -> q7,
       a_1(q3, q6) -> q7,
       a_1(q3, q4) -> q13 | q7 | q3,
       a_0(q3, q3) -> q3}
   Strict:
   {}
   Qed