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