YES

Problem:
 a(f(),a(f(),x)) -> a(x,g())
 a(x,g()) -> a(f(),a(g(),a(f(),x)))

Proof:
 DP Processor:
  DPs:
   a#(f(),a(f(),x)) -> a#(x,g())
   a#(x,g()) -> a#(f(),x)
   a#(x,g()) -> a#(g(),a(f(),x))
   a#(x,g()) -> a#(f(),a(g(),a(f(),x)))
  TRS:
   a(f(),a(f(),x)) -> a(x,g())
   a(x,g()) -> a(f(),a(g(),a(f(),x)))
  EDG Processor:
   DPs:
    a#(f(),a(f(),x)) -> a#(x,g())
    a#(x,g()) -> a#(f(),x)
    a#(x,g()) -> a#(g(),a(f(),x))
    a#(x,g()) -> a#(f(),a(g(),a(f(),x)))
   TRS:
    a(f(),a(f(),x)) -> a(x,g())
    a(x,g()) -> a(f(),a(g(),a(f(),x)))
   graph:
    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#(f(),a(f(),x)) -> a#(x,g()) ->
    a#(x,g()) -> a#(f(),a(g(),a(f(),x)))
    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#(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(),x) -> a#(x,g()) -> a#(f(),a(g(),a(f(),x)))
   SCC Processor:
    #sccs: 1
    #rules: 3
    #arcs: 8/16
    DPs:
     a#(f(),a(f(),x)) -> a#(x,g())
     a#(x,g()) -> a#(f(),a(g(),a(f(),x)))
     a#(x,g()) -> a#(f(),x)
    TRS:
     a(f(),a(f(),x)) -> a(x,g())
     a(x,g()) -> a(f(),a(g(),a(f(),x)))
    Bounds Processor:
     bound: 4
     enrichment: match
     automaton:
      final states: {4}
      transitions:
       f3() -> 25*
       g3() -> 24*
       a{#,3}(32,24) -> 4*
       a{#,3}(27,24) -> 4*
       a{#,3}(17,24) -> 4*
       a{#,3}(25,1) -> 4*
       a{#,3}(25,7) -> 4*
       a{#,3}(25,13) -> 4*
       a{#,3}(25,17) -> 4*
       a{#,3}(25,25) -> 4*
       a{#,3}(25,27) -> 4*
       a{#,3}(1,24) -> 4*
       a{#,3}(18,24) -> 4*
       a{#,3}(25,18) -> 4*
       a{#,3}(25,20) -> 4*
       a{#,3}(25,24) -> 4*
       a{#,3}(20,24) -> 4*
       a{#,3}(25,32) -> 4*
       a4(32,18) -> 33*
       a4(32,20) -> 33*
       a4(32,32) -> 33*
       a4(32,1) -> 33*
       a4(32,17) -> 33*
       a4(32,25) -> 33*
       a4(32,27) -> 33*
       a4(32,35) -> 19*
       a4(34,33) -> 35*
       f4() -> 32*
       a{#,0}(3,1) -> 4*
       a{#,0}(3,3) -> 4*
       a{#,0}(1,2) -> 4*
       a{#,0}(2,1) -> 4*
       a{#,0}(2,3) -> 4*
       a{#,0}(3,2) -> 4*
       a{#,0}(1,1) -> 4*
       a{#,0}(1,3) -> 4*
       a{#,0}(2,2) -> 4*
       g4() -> 34*
       f0() -> 1*
       a{#,4}(32,18) -> 4*
       a{#,4}(32,20) -> 4*
       a{#,4}(32,32) -> 4*
       a{#,4}(32,1) -> 4*
       a{#,4}(32,17) -> 4*
       a{#,4}(32,25) -> 4*
       a{#,4}(32,27) -> 4*
       a{#,4}(32,35) -> 4*
       a0(3,1) -> 2*
       a0(3,3) -> 2*
       a0(1,2) -> 2*
       a0(2,1) -> 2*
       a0(2,3) -> 2*
       a0(3,2) -> 2*
       a0(1,1) -> 2*
       a0(1,3) -> 2*
       a0(2,2) -> 2*
       g0() -> 3*
       a1(18,7) -> 2,12
       a1(13,7) -> 2*
       a1(3,7) -> 19,12,2
       a1(25,7) -> 2*
       a1(20,7) -> 2*
       a1(11,2) -> 12*
       a1(11,18) -> 7*
       a1(32,7) -> 2*
       a1(27,7) -> 2*
       a1(17,7) -> 2*
       a1(7,7) -> 19,12,2
       a1(2,7) -> 19,12,2
       a1(11,1) -> 12*
       a1(11,3) -> 12*
       a1(1,7) -> 19,12,2
       a1(11,11) -> 12*
       a1(11,13) -> 12,2
       a1(7,12) -> 13*
       f1() -> 11*
       g1() -> 7*
       a{#,1}(13,7) -> 4*
       a{#,1}(3,7) -> 4*
       a{#,1}(20,7) -> 4*
       a{#,1}(11,2) -> 4*
       a{#,1}(11,18) -> 4*
       a{#,1}(27,7) -> 4*
       a{#,1}(17,7) -> 4*
       a{#,1}(7,7) -> 4*
       a{#,1}(2,7) -> 4*
       a{#,1}(11,1) -> 4*
       a{#,1}(11,3) -> 4*
       a{#,1}(1,7) -> 4*
       a{#,1}(11,11) -> 4*
       a{#,1}(11,13) -> 4*
       a2(18,1) -> 2,19
       a2(18,3) -> 19*
       a2(18,7) -> 19*
       a2(18,13) -> 19*
       a2(18,17) -> 26,2,12,19
       a2(13,17) -> 19,12
       a2(18,25) -> 2*
       a2(25,17) -> 12*
       a2(20,17) -> 12*
       a2(32,17) -> 12*
       a2(27,17) -> 12*
       a2(17,17) -> 12*
       a2(7,17) -> 19,12
       a2(17,19) -> 20*
       a2(18,2) -> 19*
       a2(18,18) -> 2*
       a2(18,20) -> 19,12,2
       a2(1,17) -> 12*
       a2(17,2) -> 1*
       f2() -> 18*
       g2() -> 17*
       a{#,2}(18,1) -> 4*
       a{#,2}(18,3) -> 4*
       a{#,2}(18,7) -> 4*
       a{#,2}(18,13) -> 4*
       a{#,2}(18,17) -> 4*
       a{#,2}(13,17) -> 4*
       a{#,2}(18,25) -> 4*
       a{#,2}(20,17) -> 4*
       a{#,2}(27,17) -> 4*
       a{#,2}(17,17) -> 4*
       a{#,2}(7,17) -> 4*
       a{#,2}(18,2) -> 4*
       a{#,2}(18,18) -> 4*
       a{#,2}(18,20) -> 4*
       a{#,2}(1,17) -> 4*
       a3(32,24) -> 19*
       a3(27,24) -> 19*
       a3(17,24) -> 19*
       a3(24,2) -> 1*
       a3(25,1) -> 12,26
       a3(24,26) -> 27*
       a3(25,7) -> 26*
       a3(25,13) -> 26*
       a3(25,17) -> 26*
       a3(25,25) -> 2*
       a3(25,27) -> 26,2,19,12
       a3(1,24) -> 19*
       a3(18,24) -> 19*
       a3(25,18) -> 26*
       a3(25,20) -> 26*
       a3(25,24) -> 19*
       a3(20,24) -> 19*
       a3(25,32) -> 2*
     problem:
      DPs:
       
      TRS:
       a(f(),a(f(),x)) -> a(x,g())
       a(x,g()) -> a(f(),a(g(),a(f(),x)))
     Qed