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