(from AG01 4.20) (VAR x) (RULES f(f(x)) -> f(x) g(0) -> g(f(0)) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend