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