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