YES
(VAR x)
(RULES
+(x,s(y())) -> s(+(x,y()))
+(x,0()) -> x
*(x,0()) -> 0()
*(x,s(y())) -> +(*(x,y()),x)
fac(0()) -> s(0())
fac(s(x)) -> *(s(x),fac(x))
)