YES (VAR x y) (RULES f(f(x,0()),0()) -> x s(s(x)) -> x f(0(),x) -> x f(s(x),y) -> s(f(x,y)) g(0(),x) -> x g(s(x),y) -> f(g(x,y),0()) h(0()) -> s(0()) )