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 LPO with precedence: * > f > g > one )