YES
Time: 0.005018
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)}
  UR:
   {}
   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))}
    STATUS:
     arrows: 0.500000
     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)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [h](x0, x1) = 0,
         
         [g](x0, x1) = x0 + 1,
         
         [f](x0) = x0 + 1,
         
         [h#](x0, x1) = x0,
         
         [g#](x0, x1) = x0
        Strict:
         g#(f x, y) -> h#(x, y)
         1 + 1x + 0y >= 0 + 1x + 0y
         h#(x, y) -> g#(x, f y)
         0 + 1x + 0y >= 0 + 1x + 0y
        Weak:
         g(f x, y) -> f h(x, y)
         2 + 1x + 0y >= 1 + 0x + 0y
         h(x, y) -> g(x, f y)
         0 + 0x + 0y >= 1 + 1x + 0y
       SCCS (0):