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