(from AG01 4.32) (VAR x y) (RULES f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),s(y)) -> f(x,s(c(s(y)))) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend