/home/nowonder/forschung/aprove/TPDB05/TRS/nontermin/AG01/#4.37a.trs

The program

(from AG01 4.37a)
(VAR x y)
(RULES
f(c(s(x),y)) -> f(c(x,s(y)))
g(c(x,s(y))) -> g(c(s(x),y))
g(s(f(x))) -> g(f(x)))