YES
Time: 0.020131
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)-DP-bounded by 0
      Automaton:
       {       f_0() -> 10*
               g_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) -> 11 | 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) -> 11 | 8
          a_0(11, 8) -> 8*
         a_0(10, 12) -> 11 | 8
         a_0(10, 11) -> 11*
         a_0(10, 10) -> 11*
          a_0(10, 9) -> 11*
          a_0(10, 8) -> 11*
          a_0(9, 12) -> 8*
          a_0(9, 11) -> 12*
          a_0(9, 10) -> 8*
           a_0(9, 9) -> 11 | 8
           a_0(9, 8) -> 8*
          a_0(8, 12) -> 8*
          a_0(8, 11) -> 8*
          a_0(8, 10) -> 8*
           a_0(8, 9) -> 11 | 8
           a_0(8, 8) -> 8*}
      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 (1):
        Scc:
         {        a#(x, g()) -> a#(f(), x),
          a#(f(), a(f(), x)) -> a#(x, g())}
        SCC (2):
         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:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [a](x0, x1) = x0 + x1,
           
           [g] = 1,
           
           [f] = 1,
           
           [a#](x0, x1) = x0 + x1 + 1
          Strict:
           a#(f(), a(f(), x)) -> a#(x, g())
           3 + 1x >= 2 + 1x
           a#(x, g()) -> a#(f(), x)
           2 + 1x >= 2 + 1x
          Weak:
           
         EDG:
          {(a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), x))}
          SCCS (1):
           Scc:
            {a#(x, g()) -> a#(f(), x)}
           SCC (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())}
            POLY:
             Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
             Interpretation:
              [a](x0, x1) = 0,
              
              [g] = 1,
              
              [f] = 0,
              
              [a#](x0, x1) = x0 + x1 + 1
             Strict:
              a#(x, g()) -> a#(f(), x)
              2 + 1x >= 1 + 1x
             Weak:
              
            Qed