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

The program

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

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend