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)))
  CDG 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(),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)))
   Restore Modifier:
    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)))
    SCC Processor:
     #sccs: 1
     #rules: 1
     #arcs: 6/16
     DPs:
      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)))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [a#](x0, x1) = x0 + x1,
       
       [g] = 1,
       
       [a](x0, x1) = 0,
       
       [f] = 0
      orientation:
       a#(x,g()) = x + 1 >= x = a#(f(),x)
       
       a(f(),a(f(),x)) = 0 >= 0 = a(x,g())
       
       a(x,g()) = 0 >= 0 = a(f(),a(g(),a(f(),x)))
      problem:
       DPs:
        
       TRS:
        a(f(),a(f(),x)) -> a(x,g())
        a(x,g()) -> a(f(),a(g(),a(f(),x)))
      Qed