YES
TRS:
 {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))),
  a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))}
 DP:
  Strict:
   {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))),
    a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))),
    a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))),
    a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
  Weak:
  {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))),
   a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))}
  EDG:
   {(a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))))
    (a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))))
    (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))))
    (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))))
    (a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))))
    (a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))))
    (a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))))
    (a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))))}
   SCCS:
    Scc:
     {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))),
      a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))),
      a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))),
      a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
    SCC:
     Strict:
      {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))),
       a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))),
       a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))),
       a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
     Weak:
     {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))),
      a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))}
     BOUND:
      Bound: match(-raise)-DP-bounded by 0
      Automaton:
       {       g_0() -> 11*
               f_0() -> 10*
        a#_0(10, 14) -> 5*
         a_0(14, 14) -> 9*
         a_0(14, 13) -> 9*
         a_0(14, 12) -> 9*
         a_0(14, 11) -> 9*
         a_0(14, 10) -> 9*
          a_0(14, 9) -> 9*
         a_0(13, 14) -> 9*
         a_0(13, 13) -> 9*
         a_0(13, 12) -> 9*
         a_0(13, 11) -> 9*
         a_0(13, 10) -> 9*
          a_0(13, 9) -> 9*
         a_0(12, 14) -> 9*
         a_0(12, 13) -> 9*
         a_0(12, 12) -> 9*
         a_0(12, 11) -> 9*
         a_0(12, 10) -> 9*
          a_0(12, 9) -> 9*
         a_0(11, 14) -> 9*
         a_0(11, 13) -> 14*
         a_0(11, 12) -> 13*
         a_0(11, 11) -> 9*
         a_0(11, 10) -> 9*
          a_0(11, 9) -> 9*
         a_0(10, 14) -> 12*
         a_0(10, 13) -> 12*
         a_0(10, 12) -> 12*
         a_0(10, 11) -> 12*
         a_0(10, 10) -> 12*
          a_0(10, 9) -> 12*
          a_0(9, 14) -> 9*
          a_0(9, 13) -> 9*
          a_0(9, 12) -> 9*
          a_0(9, 11) -> 9*
          a_0(9, 10) -> 9*
           a_0(9, 9) -> 9*}
      Strict:
       {a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))),
        a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))),
        a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
      EDG:
       {(a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))))
        (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))))
        (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))))
        (a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))))
        (a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))))}
       SCCS:
        Scc:
         {a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))),
          a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))),
          a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
        SCC:
         Strict:
          {a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))),
           a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))),
           a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
         Weak:
         {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))),
          a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))}
         BOUND:
          Bound: match(-raise)-DP-bounded by 0
          Automaton:
           {       g_0() -> 10*
                   f_0() -> 9*
            a#_0(10, 12) -> 5*
             a_0(12, 12) -> 8*
             a_0(12, 11) -> 8*
             a_0(12, 10) -> 8*
              a_0(12, 9) -> 8*
              a_0(12, 8) -> 8*
             a_0(11, 12) -> 8*
             a_0(11, 11) -> 8*
             a_0(11, 10) -> 8*
              a_0(11, 9) -> 8*
              a_0(11, 8) -> 8*
             a_0(10, 12) -> 8*
             a_0(10, 11) -> 12*
             a_0(10, 10) -> 8*
              a_0(10, 9) -> 8*
              a_0(10, 8) -> 8*
              a_0(9, 12) -> 11*
              a_0(9, 11) -> 11*
              a_0(9, 10) -> 11*
               a_0(9, 9) -> 11*
               a_0(9, 8) -> 11*
              a_0(8, 12) -> 8*
              a_0(8, 11) -> 8*
              a_0(8, 10) -> 8*
               a_0(8, 9) -> 8*
               a_0(8, 8) -> 8*}
          Strict:
           {a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))),
            a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
          EDG:
           {(a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))))
            (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))))}
           SCCS:
            Scc:
             {a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
            SCC:
             Strict:
              {a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
             Weak:
             {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))),
              a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))}
             BOUND:
              Bound: match(-raise)-DP-bounded by 0
              Automaton:
               {       g_0() -> 11*
                       f_0() -> 10*
                a#_0(11, 14) -> 5*
                 a_0(14, 14) -> 9*
                 a_0(14, 13) -> 9*
                 a_0(14, 12) -> 9*
                 a_0(14, 11) -> 9*
                 a_0(14, 10) -> 9*
                  a_0(14, 9) -> 9*
                 a_0(13, 14) -> 9*
                 a_0(13, 13) -> 9*
                 a_0(13, 12) -> 9*
                 a_0(13, 11) -> 9*
                 a_0(13, 10) -> 9*
                  a_0(13, 9) -> 9*
                 a_0(12, 14) -> 9*
                 a_0(12, 13) -> 9*
                 a_0(12, 12) -> 9*
                 a_0(12, 11) -> 9*
                 a_0(12, 10) -> 9*
                  a_0(12, 9) -> 9*
                 a_0(11, 14) -> 12*
                 a_0(11, 13) -> 12*
                 a_0(11, 12) -> 12*
                 a_0(11, 11) -> 12*
                 a_0(11, 10) -> 12*
                  a_0(11, 9) -> 12*
                 a_0(10, 14) -> 9*
                 a_0(10, 13) -> 14*
                 a_0(10, 12) -> 13*
                 a_0(10, 11) -> 9*
                 a_0(10, 10) -> 9*
                  a_0(10, 9) -> 9*
                  a_0(9, 14) -> 9*
                  a_0(9, 13) -> 9*
                  a_0(9, 12) -> 9*
                  a_0(9, 11) -> 9*
                  a_0(9, 10) -> 9*
                   a_0(9, 9) -> 9*}
              Strict:
               {}
              Qed