(VAR x y z )
(RULES 
        plus(0, x) -> x
        plus(s(x), y) -> s(plus(x, y))
        times(0, y) -> 0
        times(s(x), y) -> plus(y, times(x, y))
        p(s(x)) -> x
        p(0) -> 0
        minus(x, 0) -> x
        minus(0, x) -> 0
        minus(x, s(y)) -> p(minus(x, y))
        isZero(0) -> true
        isZero(s(x)) -> false
        facIter(x, y) -> if(isZero(x), minus(x, s(0)), y, times(y, x))
        if(true, x, y, z) -> y
        if(false, x, y, z) -> facIter(x, z)
        factorial(x) -> facIter(x, s(0))
        
)