(VAR x y)
(REPLACEMENT-MAP
  (s )
)
(HORN-CLAUSES
   x === y | x ->* y
)
(RULES
  g(s(x)) -> g(x)
  f(g(x)) -> x | x === s(0)
)
(COMMENT
  Example 56, right, Lucas JLAMP'24
  https://doi.org/10.1016/j.jlamp.2023.100926
)