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)-bounded by 1
      Automaton:
       {       b_0() -> 2*
               f_1() -> 11*
               f_0() -> 5*
               g_1() -> 12*
               g_0() -> 3*
        a#_1(11, 14) -> 8*
         a#_1(11, 2) -> 8*
          a#_0(5, 7) -> 10 | 8
          a#_0(5, 5) -> 8*
          a#_0(5, 2) -> 9 | 8
          a#_0(2, 3) -> 8*
         a_1(12, 13) -> 14*
         a_1(11, 14) -> 1*
          a_1(11, 2) -> 13*
           a_0(5, 7) -> 4 | 1
           a_0(5, 5) -> 6*
           a_0(5, 2) -> 6*
           a_0(3, 6) -> 7*
           a_0(2, 3) -> 1*
                   8 -> 9*
                   1 -> 6*}
      Strict:
       {}
      Qed