(VAR x) (RULES f(a,x) -> f(g(x),x) h(g(x)) -> h(a) g(h(x)) -> g(x) h(h(x)) -> x )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend