/home/nowonder/forschung/aprove/TPDB05/TRS/Rubio/gmnp.trs

The program

(VAR X)
(RULES

f(a) -> f(c(a))
f(c(X)) -> X
f(c(a)) -> f(d(b))
f(a) -> f(d(a))
f(d(X)) -> X
f(c(b)) -> f(d(a))
e(g(X)) -> e(X)
 
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend