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