YES (VAR x y) (RULES *(x,s(y)) -> +(*(x,y),x) *(x,0()) -> 0() +(x,s(y)) -> s(+(x,y)) +(x,0()) -> x ) (COMMENT Termination is shown by LPO with precedence: 0 > * > + > s )