MAYBE
MAYBE
TRS:
 {
             q(0()) -> 0(),
            q(s(X)) -> s(p(q(X), d(X))),
               t(N) -> cs(r(q(N)), nt(ns(N))),
               t(X) -> nt(X),
               s(X) -> ns(X),
          p(X, 0()) -> X,
          p(0(), X) -> X,
      p(s(X), s(Y)) -> s(s(p(X, Y))),
             d(0()) -> 0(),
            d(s(X)) -> s(s(d(X))),
          f(X1, X2) -> nf(X1, X2),
          f(0(), X) -> nil(),
  f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
               a(X) -> X,
           a(nt(X)) -> t(a(X)),
           a(ns(X)) -> s(a(X)),
      a(nf(X1, X2)) -> f(a(X1), a(X2))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
               q(0()) -> 0(),
              q(s(X)) -> s(p(q(X), d(X))),
                 t(N) -> cs(r(q(N)), nt(ns(N))),
                 t(X) -> nt(X),
                 s(X) -> ns(X),
            p(X, 0()) -> X,
            p(0(), X) -> X,
        p(s(X), s(Y)) -> s(s(p(X, Y))),
               d(0()) -> 0(),
              d(s(X)) -> s(s(d(X))),
            f(X1, X2) -> nf(X1, X2),
            f(0(), X) -> nil(),
    f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
                 a(X) -> X,
             a(nt(X)) -> t(a(X)),
             a(ns(X)) -> s(a(X)),
        a(nf(X1, X2)) -> f(a(X1), a(X2))
   }
  Fail