YES
Time: 0.084532
TRS:
 {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
  a(f(), a(f(), x)) -> a(x, g())}
 DP:
  DP:
   {        a#(x, g()) -> a#(g(), a(f(), x)),
            a#(x, g()) -> a#(f(), x),
            a#(x, g()) -> a#(f(), a(g(), a(f(), x))),
    a#(f(), a(f(), x)) -> a#(x, g())}
  TRS:
  {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
   a(f(), a(f(), x)) -> a(x, g())}
  EDG:
   {(a#(x, g()) -> a#(f(), a(g(), a(f(), x))), a#(f(), a(f(), x)) -> a#(x, g()))
    (a#(f(), a(f(), x)) -> a#(x, g()), a#(x, g()) -> a#(f(), a(g(), a(f(), x))))
    (a#(f(), a(f(), x)) -> a#(x, g()), a#(x, g()) -> a#(f(), x))
    (a#(f(), a(f(), x)) -> a#(x, g()), a#(x, g()) -> a#(g(), a(f(), x)))
    (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(g(), a(f(), x)))
    (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), x))
    (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), a(g(), a(f(), x))))
    (a#(x, g()) -> a#(f(), x), a#(f(), a(f(), x)) -> a#(x, g()))}
   SCCS (1):
    Scc:
     {        a#(x, g()) -> a#(f(), x),
              a#(x, g()) -> a#(f(), a(g(), a(f(), x))),
      a#(f(), a(f(), x)) -> a#(x, g())}
    SCC (3):
     Strict:
      {        a#(x, g()) -> a#(f(), x),
               a#(x, g()) -> a#(f(), a(g(), a(f(), x))),
       a#(f(), a(f(), x)) -> a#(x, g())}
     Weak:
     {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
      a(f(), a(f(), x)) -> a(x, g())}
     BOUND:
      Bound: match(-raise)-bounded by 4
      Automaton:
       {       f_4() -> 16*
               f_3() -> 11*
               f_2() -> 7*
               f_1() -> 3*
               f_0() -> 1*
               g_4() -> 17*
               g_3() -> 10*
               g_2() -> 6*
               g_1() -> 2*
               g_0() -> 1*
        a#_4(16, 21) -> 1*
        a#_4(16, 19) -> 1*
         a#_4(16, 9) -> 1*
        a#_3(21, 10) -> 1*
        a#_3(11, 21) -> 1*
        a#_3(11, 15) -> 1*
        a#_3(11, 11) -> 1*
         a#_3(11, 9) -> 1*
         a#_3(11, 7) -> 1*
         a#_3(11, 6) -> 1*
         a#_3(11, 5) -> 1*
         a#_3(11, 3) -> 1*
         a#_3(11, 2) -> 1*
         a#_3(9, 10) -> 1*
         a#_2(21, 6) -> 1*
          a#_2(9, 6) -> 1*
         a#_2(7, 23) -> 1*
         a#_2(7, 11) -> 1*
          a#_2(7, 9) -> 1*
          a#_2(7, 7) -> 1*
          a#_2(7, 6) -> 1*
          a#_2(7, 5) -> 1*
          a#_2(7, 3) -> 1*
          a#_2(7, 2) -> 1*
          a#_2(7, 1) -> 1*
          a#_2(6, 6) -> 1*
          a#_2(5, 6) -> 1*
          a#_2(3, 6) -> 1*
          a#_2(2, 6) -> 1*
         a#_1(21, 2) -> 1*
          a#_1(9, 2) -> 1*
          a#_1(6, 2) -> 1*
          a#_1(5, 2) -> 1*
         a#_1(3, 13) -> 1*
          a#_1(3, 7) -> 1*
          a#_1(3, 5) -> 1*
          a#_1(3, 3) -> 1*
          a#_1(3, 2) -> 1*
          a#_1(3, 1) -> 1*
          a#_1(2, 2) -> 1*
          a#_1(1, 2) -> 1*
          a#_0(1, 1) -> 1*
         a_4(17, 18) -> 19*
         a_4(16, 21) -> 18*
         a_4(16, 19) -> 8*
          a_4(16, 9) -> 18*
         a_3(21, 10) -> 8*
         a_3(11, 21) -> 14 | 8 | 4 | 1
         a_3(11, 15) -> 8 | 4
         a_3(11, 11) -> 24*
          a_3(11, 9) -> 14*
          a_3(11, 7) -> 20*
          a_3(11, 6) -> 20*
          a_3(11, 5) -> 14*
          a_3(11, 3) -> 20*
          a_3(11, 2) -> 14*
         a_3(10, 24) -> 7*
         a_3(10, 20) -> 21*
         a_3(10, 14) -> 15*
          a_3(9, 10) -> 8*
          a_2(21, 6) -> 4*
           a_2(9, 6) -> 4*
          a_2(7, 23) -> 14*
          a_2(7, 11) -> 22*
           a_2(7, 9) -> 8 | 4 | 1
           a_2(7, 7) -> 8*
           a_2(7, 6) -> 8*
           a_2(7, 5) -> 8*
           a_2(7, 3) -> 8*
           a_2(7, 2) -> 8*
           a_2(7, 1) -> 8*
          a_2(6, 22) -> 23*
           a_2(6, 8) -> 9*
           a_2(6, 6) -> 8 | 4
           a_2(5, 6) -> 8 | 4
           a_2(3, 6) -> 14 | 8 | 4 | 1
           a_2(2, 6) -> 8 | 4
          a_1(21, 2) -> 1*
           a_1(9, 2) -> 1*
           a_1(6, 2) -> 1*
           a_1(5, 2) -> 1*
          a_1(3, 13) -> 8*
           a_1(3, 7) -> 12*
           a_1(3, 5) -> 1*
           a_1(3, 3) -> 2*
           a_1(3, 2) -> 8 | 4 | 1
           a_1(3, 1) -> 4*
          a_1(2, 12) -> 13*
           a_1(2, 4) -> 5*
           a_1(2, 2) -> 8 | 4 | 1
           a_1(1, 2) -> 8 | 4 | 1
           a_0(1, 1) -> 1*}
      Strict:
       {}
      Qed