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