YES (VAR x0 x1 x y z) (RULES *(x0,*(1(),x1)) -> *(x0,x1) 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 + 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) = x1 + x2 1#_A = 0 exp#_A(x1) = x1 weights w0 = 1 w(+) = 1 w(0) = 1 w(*) = 0 w(1) = 1 w(exp) = 1 and precedence: exp > * > 1 > + > 0 )