YES (VAR x1 x0 x2 x y z) (RULES *(f(x1),*(g(x0),x2)) -> *(g(x0),*(f(x1),x2)) i(g(x0)) -> g(i(x0)) g(one()) -> one() i(*(x1,x0)) -> *(i(x0),i(x1)) i(f(x0)) -> f(i(x0)) i(h(x0)) -> h(i(x0)) i(k(x0)) -> k(i(x0)) f(one()) -> one() *(x1,*(i(x1),x0)) -> x0 *(x0,i(x0)) -> one() i(i(x0)) -> x0 i(one()) -> one() k(one()) -> one() h(one()) -> one() *(x0,one()) -> x0 *(f(x1),*(h(x0),x2)) -> *(h(x0),*(f(x1),x2)) *(h(x1),*(g(x0),x2)) -> *(g(x0),*(h(x1),x2)) *(k(x0),*(f(x1),x2)) -> *(f(x1),*(k(x0),x2)) *(k(x0),*(h(x1),x2)) -> *(h(x1),*(k(x0),x2)) *(k(x0),*(g(x1),x2)) -> *(g(x1),*(k(x0),x2)) *(k(x0),*(k(x1),x2)) -> *(k(*(x0,x1)),x2) *(f(x0),*(f(x1),x2)) -> *(f(*(x0,x1)),x2) *(g(x0),*(g(x1),x2)) -> *(g(*(x0,x1)),x2) *(h(x0),*(h(x1),x2)) -> *(h(*(x0,x1)),x2) *(i(x1),*(x1,x0)) -> x0 *(k(x),g(y)) -> *(g(y),k(x)) *(k(x),h(y)) -> *(h(y),k(x)) *(k(y),f(x)) -> *(f(x),k(y)) *(h(x),g(y)) -> *(g(y),h(x)) *(f(x),h(y)) -> *(h(y),f(x)) *(f(x),g(y)) -> *(g(y),f(x)) *(k(x),k(y)) -> k(*(x,y)) *(h(x),h(y)) -> h(*(x,y)) *(g(x),g(y)) -> g(*(x,y)) *(f(x),f(y)) -> f(*(x,y)) *(*(x,y),z) -> *(x,*(y,z)) *(i(x),x) -> one() *(one(),x) -> x ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers *_A(x1,x2) = x1 + x2 one_A = 0 i_A(x1) = x1 f_A(x1) = 2 g_A(x1) = 0 h_A(x1) = 1 k_A(x1) = 3 *#_A(x1,x2) = x1 one#_A = 0 weights w0 = 1 w(*) = 0 w(one) = 1 w(i) = 0 w(f) = 1 w(g) = 1 w(h) = 1 w(k) = 1 and precedence: i > g > h > k > f > * > one )