(COMMENT Slight modified version of a system from Lucas02 Currently needs complex graph criteria, mixing polynomial orderings and RPO) (VAR N X Y Z X1 X2 x 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 )