YES
Time: 0.000999
TRS:
 {a(f(), a(f(), x)) -> a(x, x),
          a(h(), x) -> a(f(), a(g(), a(f(), x)))}
 DP:
  DP:
   {a#(f(), a(f(), x)) -> a#(x, x),
            a#(h(), x) -> a#(f(), x),
            a#(h(), x) -> a#(f(), a(g(), a(f(), x))),
            a#(h(), x) -> a#(g(), a(f(), x))}
  TRS:
  {a(f(), a(f(), x)) -> a(x, x),
           a(h(), x) -> a(f(), a(g(), a(f(), x)))}
  EDG:
   {(a#(f(), a(f(), x)) -> a#(x, x), a#(h(), x) -> a#(g(), a(f(), x)))
    (a#(f(), a(f(), x)) -> a#(x, x), a#(h(), x) -> a#(f(), a(g(), a(f(), x))))
    (a#(f(), a(f(), x)) -> a#(x, x), a#(h(), x) -> a#(f(), x))
    (a#(f(), a(f(), x)) -> a#(x, x), a#(f(), a(f(), x)) -> a#(x, x))
    (a#(h(), x) -> a#(f(), x), a#(f(), a(f(), x)) -> a#(x, x))}
   SCCS (1):
    Scc:
     {a#(f(), a(f(), x)) -> a#(x, x),
              a#(h(), x) -> a#(f(), x)}
    SCC (2):
     Strict:
      {a#(f(), a(f(), x)) -> a#(x, x),
               a#(h(), x) -> a#(f(), x)}
     Weak:
     {a(f(), a(f(), x)) -> a(x, x),
              a(h(), x) -> a(f(), a(g(), a(f(), x)))}
     SPSC:
      Simple Projection:
       pi(a#) = 1
      Strict:
       {a#(h(), x) -> a#(f(), x)}
      EDG:
       {}
       SCCS (0):
        
        Qed