YES(?,O(n^1))
TRS:
 {
          a(x, g()) -> a(f(), a(g(), a(f(), x))),
  a(f(), a(f(), x)) -> a(x, g())
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
            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:
    {
     a_4(15, 16) -> 17*
     a_4(14, 17) -> 6*
      a_4(14, 7) -> 16*
      a_3(9, 11) -> 6 | 3
       a_3(9, 7) -> 10*
       a_3(9, 2) -> 10*
      a_3(8, 10) -> 11*
       a_3(7, 8) -> 6*
       a_2(7, 4) -> 3*
      a_2(5, 13) -> 10*
       a_2(5, 9) -> 12*
       a_2(5, 7) -> 6 | 3 | 1
       a_2(5, 5) -> 6*
       a_2(5, 2) -> 6*
       a_2(5, 1) -> 6*
      a_2(4, 12) -> 13*
       a_2(4, 6) -> 7*
       a_2(2, 4) -> 6 | 3
       a_1(7, 2) -> 3 | 1
       a_1(2, 3) -> 2*
       a_1(2, 2) -> 6 | 3 | 1
       a_1(1, 5) -> 3*
       a_1(1, 2) -> 6 | 3 | 1
       a_1(1, 1) -> 3*
       a_0(1, 1) -> 1*
           g_4() -> 15*
           g_3() -> 8*
           g_2() -> 4*
           g_1() -> 2*
           g_0() -> 1*
           f_4() -> 14*
           f_3() -> 9*
           f_2() -> 5*
           f_1() -> 1*
           f_0() -> 1*
    }
   Strict:
    {}
   Qed