YES
TRS:
 {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
  a(f(), a(f(), x)) -> a(x, g())}
 DP:
  Strict:
   {        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())}
  Weak:
  {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
   a(f(), a(f(), x)) -> a(x, g())}
  EDG:
   {(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#(f(), a(f(), x)) -> a#(x, g()))
    (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), 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#(g(), a(f(), x)))
    (a#(x, g()) -> a#(f(), a(g(), a(f(), x))), a#(f(), a(f(), x)) -> a#(x, g()))}
   SCCS:
    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:
     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)-DP-bounded by 0
      Automaton:
       {     b_0() -> 4*
             f_0() -> 2*
             g_0() -> 3*
        a#_0(2, 6) -> 1*
         a_0(4, 3) -> 5*
         a_0(3, 5) -> 6*
         a_0(2, 6) -> 5*
         a_0(2, 4) -> 5*
         a_0(2, 2) -> 5*}
      Strict:
       {        a#(x, g()) -> a#(f(), x),
        a#(f(), a(f(), x)) -> a#(x, g())}
      EDG:
       {(a#(f(), a(f(), x)) -> a#(x, g()), a#(x, g()) -> a#(f(), x))
        (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), x))
        (a#(x, g()) -> a#(f(), x), a#(f(), a(f(), x)) -> a#(x, g()))}
       SCCS:
        Scc:
         {        a#(x, g()) -> a#(f(), x),
          a#(f(), a(f(), x)) -> a#(x, g())}
        SCC:
         Strict:
          {        a#(x, 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())}
         POLY:
          Argument Filtering:
           pi(f) = [], pi(g) = [], pi(a#) = [0,1], pi(a) = [0,1]
          Usable Rules:
           {}
          Interpretation:
           [a#](x0, x1) = x0 + x1,
           [a](x0, x1) = x0 + x1,
           [f] = 1,
           [g] = 1
          Strict:
           {a#(x, g()) -> a#(f(), x)}
          Weak:
           {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
            a(f(), a(f(), x)) -> a(x, g())}
          EDG:
           {(a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), x))}
           SCCS:
            Scc:
             {a#(x, g()) -> a#(f(), x)}
            SCC:
             Strict:
              {a#(x, g()) -> a#(f(), x)}
             Weak:
             {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
              a(f(), a(f(), x)) -> a(x, g())}
             POLY:
              Argument Filtering:
               pi(f) = [], pi(g) = [], pi(a#) = [0,1], pi(a) = []
              Usable Rules:
               {}
              Interpretation:
               [a#](x0, x1) = x0 + x1,
               [f] = 0,
               [g] = 1
              Strict:
               {}
              Weak:
               {        a(x, g()) -> a(f(), a(g(), a(f(), x))),
                a(f(), a(f(), x)) -> a(x, g())}
              Qed