YES (VAR x) (RULES fac(s(x)) -> *(s(x),fac(x)) fac(0()) -> s(0()) *(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: fac > * > + > s > y > 0 )