(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