(VAR x) (RULES f(x) -> f(g(x)) ) (COMMENT Non-termiating. )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend