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