YES (VAR x y z) (RULES exp(+(x,y)) -> *(exp(x),exp(y)) exp(0()) -> 1() *(x,1()) -> x *(x,*(y,z)) -> *(*(x,y),z) +(x,0()) -> x +(x,+(y,z)) -> +(+(x,y),z) ) (COMMENT Termination is shown by ELPO with interpretations on natural numbers +_A(x1,x2) = x1 + x2 + 2 0_A = 1 *_A(x1,x2) = x1 + x2 + 1 1_A = 2 exp_A(x1) = x1 + 1 +#_A(x1,x2) = x2 0#_A = 0 *#_A(x1,x2) = x2 1#_A = 0 and precedence: + > * > exp > 1 > 0 )