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 KBO with weight w0 = 1 w(f) = 0 w(*) = 0 w(g) = 0 w(one) = 1 and precedence: * > f > g > one )