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