YES (VAR x y z) (RULES +(x,-(x)) -> 0() +(x,+(-(x),y)) -> y +(-(x),x) -> 0() -(+(x,y)) -> +(-(y),-(x)) g(x,y) -> f(x,+(x,-(y)),y) +(-(x),+(x,y)) -> y -(0()) -> 0() +(0(),x) -> x +(x,0()) -> x -(-(x)) -> x +(+(x,y),z) -> +(x,+(y,z)) f(0(),x,y) -> x )