(VAR x )
(RULES 
        p(s(x)) -> x
        fac(0) -> s(0)
        fac(s(x)) -> times(s(x), fac(p(s(x))))
        
)