(VAR N X X1 X2 Y Z )
(RULES 
        t(N) -> cs(r(q(N)), nt(ns(N)))
        q(0) -> 0
        q(s(X)) -> s(p(q(X), d(X)))
        d(0) -> 0
        d(s(X)) -> s(s(d(X)))
        p(0, X) -> X
        p(X, 0) -> X
        p(s(X), s(Y)) -> s(s(p(X, Y)))
        f(0, X) -> nil
        f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z)))
        t(X) -> nt(X)
        s(X) -> ns(X)
        f(X1, X2) -> nf(X1, X2)
        a(nt(X)) -> t(a(X))
        a(ns(X)) -> s(a(X))
        a(nf(X1, X2)) -> f(a(X1), a(X2))
        a(X) -> X
        
)