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 EKBO with interpretations on natural numbers +_A(x1,x2) = x1 + x2 + 1 0_A = 1 *_A(x1,x2) = x1 + x2 + 1 1_A = 1 exp_A(x1) = x1 +#_A(x1,x2) = x2 0#_A = 0 *#_A(x1,x2) = x2 1#_A = 0 weights w0 = 1 w(+) = 1 w(0) = 1 w(*) = 0 w(1) = 2 w(exp) = 1 and precedence: + > exp > * > 0 > 1 )