YES
Time: 0.002119
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))}
   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}
     SPSC:
      Simple Projection:
       pi(h#) = 1, pi(f#) = 0
      Strict:
       { f#(g x, g y) -> h#(g y, x, g y),
        h#(g x, y, z) -> f#(y, h(x, y, z)),
        h#(g x, y, z) -> h#(x, y, z)}
      EDG:
       {(f#(g x, g y) -> h#(g y, x, g y), h#(g x, y, z) -> 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)))
        (h#(g x, y, z) -> h#(x, y, z), h#(g x, y, z) -> f#(y, 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))}
       SCCS (1):
        Scc:
         { f#(g x, g y) -> h#(g y, x, g y),
          h#(g x, y, z) -> f#(y, h(x, y, z)),
          h#(g x, y, z) -> h#(x, y, z)}
        SCC (3):
         Strict:
          { f#(g x, g y) -> h#(g y, x, g y),
           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}
         SPSC:
          Simple Projection:
           pi(h#) = 1, pi(f#) = 0
          Strict:
           {h#(g x, y, z) -> f#(y, h(x, y, z)),
            h#(g x, y, z) -> h#(x, y, z)}
          EDG:
           {(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)))}
           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}
             SPSC:
              Simple Projection:
               pi(h#) = 0
              Strict:
               {}
              Qed