(from AG01 4.10) (VAR x) (RULES f(x,g(x)) -> f(1,g(x)) g(1) -> g(0) ) (STRATEGY INNERMOST)
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend