(VAR x) (RULES f(f(x)) -> g(f(x))) (COMMENT Example 3 in \cite{D33})
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend