YES
Time: 0.030864
TRS:
 { f(g x, g y) -> h(g y, x, g y),
   f(g x, a()) -> f(x, g a()),
   f(a(), g y) -> g g y,
  h(g x, y, z) -> f(y, h(x, y, z)),
  h(a(), y, z) -> z}
 DP:
  DP:
   { f#(g x, g y) -> h#(g y, x, g y),
     f#(g x, a()) -> f#(x, g a()),
    h#(g x, y, z) -> f#(y, h(x, y, z)),
    h#(g x, y, z) -> h#(x, y, z)}
  TRS:
  { f(g x, g y) -> h(g y, x, g y),
    f(g x, a()) -> f(x, g a()),
    f(a(), g y) -> g g y,
   h(g x, y, z) -> f(y, h(x, y, z)),
   h(a(), y, z) -> z}
  EDG:
   {(h#(g x, y, z) -> f#(y, h(x, y, z)), f#(g x, a()) -> f#(x, g a()))
    (h#(g x, y, z) -> f#(y, h(x, y, z)), f#(g x, g y) -> h#(g y, x, g y))
    (h#(g x, y, z) -> h#(x, y, z), h#(g x, y, z) -> h#(x, y, z))
    (h#(g x, y, z) -> h#(x, y, z), h#(g x, y, z) -> f#(y, h(x, y, z)))
    (f#(g x, g y) -> h#(g y, x, g y), h#(g x, y, z) -> f#(y, h(x, y, z)))
    (f#(g x, g y) -> h#(g y, x, g y), h#(g x, y, z) -> h#(x, y, z))
    (f#(g x, a()) -> f#(x, g a()), f#(g x, g y) -> h#(g y, x, g y))}
   STATUS:
    arrows: 0.562500
    SCCS (1):
     Scc:
      { f#(g x, g y) -> h#(g y, x, g y),
        f#(g x, a()) -> f#(x, g a()),
       h#(g x, y, z) -> f#(y, h(x, y, z)),
       h#(g x, y, z) -> h#(x, y, z)}
     
     SCC (4):
      Strict:
       { f#(g x, g y) -> h#(g y, x, g y),
         f#(g x, a()) -> f#(x, g a()),
        h#(g x, y, z) -> f#(y, h(x, y, z)),
        h#(g x, y, z) -> h#(x, y, z)}
      Weak:
      { f(g x, g y) -> h(g y, x, g y),
        f(g x, a()) -> f(x, g a()),
        f(a(), g y) -> g g y,
       h(g x, y, z) -> f(y, h(x, y, z)),
       h(a(), y, z) -> z}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [h](x0, x1, x2) = 1,
        
        [f](x0, x1) = x0 + 1,
        
        [g](x0) = x0 + 1,
        
        [a] = 1,
        
        [h#](x0, x1, x2) = x0,
        
        [f#](x0, x1) = x0
       Strict:
        h#(g x, y, z) -> h#(x, y, z)
        0 + 1y + 0x + 0z >= 0 + 1y + 0x + 0z
        h#(g x, y, z) -> f#(y, h(x, y, z))
        0 + 1y + 0x + 0z >= 0 + 1y + 0x + 0z
        f#(g x, a()) -> f#(x, g a())
        1 + 1x >= 0 + 1x
        f#(g x, g y) -> h#(g y, x, g y)
        1 + 0y + 1x >= 0 + 0y + 1x
       Weak:
        h(a(), y, z) -> z
        1 + 0y + 0z >= 1z
        h(g x, y, z) -> f(y, h(x, y, z))
        1 + 0y + 0x + 0z >= 2 + 0y + 0x + 0z
        f(a(), g y) -> g g y
        2 + 1y >= 2 + 1y
        f(g x, a()) -> f(x, g a())
        2 + 0x >= 3 + 0x
        f(g x, g y) -> h(g y, x, g y)
        2 + 1y + 0x >= 1 + 0y + 0x
      SCCS (1):
       Scc:
        {h#(g x, y, z) -> h#(x, y, z)}
       
       SCC (1):
        Strict:
         {h#(g x, y, z) -> h#(x, y, z)}
        Weak:
        { f(g x, g y) -> h(g y, x, g y),
          f(g x, a()) -> f(x, g a()),
          f(a(), g y) -> g g y,
         h(g x, y, z) -> f(y, h(x, y, z)),
         h(a(), y, z) -> z}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [h](x0, x1, x2) = 0,
          
          [f](x0, x1) = x0 + 1,
          
          [g](x0) = x0 + 1,
          
          [a] = 1,
          
          [h#](x0, x1, x2) = x0
         Strict:
          h#(g x, y, z) -> h#(x, y, z)
          1 + 0y + 1x + 0z >= 0 + 0y + 1x + 0z
         Weak:
          h(a(), y, z) -> z
          0 + 0y + 0z >= 1z
          h(g x, y, z) -> f(y, h(x, y, z))
          0 + 0y + 0x + 0z >= 1 + 1y + 0x + 0z
          f(a(), g y) -> g g y
          2 + 0y >= 2 + 1y
          f(g x, a()) -> f(x, g a())
          2 + 1x >= 1 + 1x
          f(g x, g y) -> h(g y, x, g y)
          2 + 0y + 1x >= 0 + 0y + 0x
        Qed