(from AG01 4.25) (VAR x) (RULES f(x,x) -> f(g(x),x) g(x) -> s(x) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend