(VAR x x' x'' y y' y'')
(HORN-CLAUSES
  x === y | x ->* y
)
(RULES
  f(x',x'') -> h(x,f(x,b)) | x' === x, x'' === x
  f(g(y'),y'') -> h(y,f(g(y),a)) | y' === y, y'' === y
  a -> b 
)
(COMMENT
  Example 5, Lucas FSCD'24
  https://doi.org/10.4230/LIPIcs.FSCD.2024.32
)