/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/4.41.trs

The program

(VAR x y z)
(RULES
f(a,y) -> f(y,g(y))
g(a) -> b
g(b) -> b
)
(COMMENT Example 4.41 (Forward Chains) in \cite{SK90})