YES (VAR x1 x0 y z x) (RULES -(+(x1,x0)) -> +(-(x0),-(x1)) +(-(x0),+(x0,x1)) -> x1 g(x0,x1) -> f(x0,+(x0,-(x1)),x1) +(-(x0),x0) -> 0() -(0()) -> 0() -(-(x0)) -> x0 +(0(),x0) -> x0 +(x0,0()) -> x0 +(x1,+(-(x1),x0)) -> x0 f(0(),y,z) -> y +(x,-(x)) -> 0() +(+(x,y),z) -> +(x,+(y,z)) ) (COMMENT Termination is shown by ELPO with interpretations on natural numbers +_A(x1,x2) = x1 + x2 + 1 0_A = 0 -_A(x1) = x1 f_A(x1,x2,x3) = x2 + 2 g_A(x1,x2) = x1 + x2 + 3 0#_A = 0 g#_A(x1,x2) = x1 and precedence: g > - > + > f > 0 )