MAYBE
MAYBE
TRS:
 {
                      app(X1, X2) -> n__app(X1, X2),
                   app(nil(), YS) -> YS,
             app(cons(X, XS), YS) -> cons(X, n__app(activate(XS), YS)),
                            nil() -> n__nil(),
                      activate(X) -> X,
         activate(n__app(X1, X2)) -> app(activate(X1), activate(X2)),
             activate(n__from(X)) -> from(activate(X)),
                activate(n__s(X)) -> s(activate(X)),
               activate(n__nil()) -> nil(),
       activate(n__zWadr(X1, X2)) -> zWadr(activate(X1), activate(X2)),
           activate(n__prefix(X)) -> prefix(activate(X)),
                          from(X) -> cons(X, n__from(n__s(X))),
                          from(X) -> n__from(X),
                 zWadr(XS, nil()) -> nil(),
                    zWadr(X1, X2) -> n__zWadr(X1, X2),
                 zWadr(nil(), YS) -> nil(),
  zWadr(cons(X, XS), cons(Y, YS)) ->
  cons(app(Y, cons(X, n__nil())), n__zWadr(activate(XS), activate(YS))),
                        prefix(X) -> n__prefix(X),
                        prefix(L) -> cons(nil(), n__zWadr(L, n__prefix(L))),
                             s(X) -> n__s(X)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                        app(X1, X2) -> n__app(X1, X2),
                     app(nil(), YS) -> YS,
               app(cons(X, XS), YS) -> cons(X, n__app(activate(XS), YS)),
                              nil() -> n__nil(),
                        activate(X) -> X,
           activate(n__app(X1, X2)) -> app(activate(X1), activate(X2)),
               activate(n__from(X)) -> from(activate(X)),
                  activate(n__s(X)) -> s(activate(X)),
                 activate(n__nil()) -> nil(),
         activate(n__zWadr(X1, X2)) -> zWadr(activate(X1), activate(X2)),
             activate(n__prefix(X)) -> prefix(activate(X)),
                            from(X) -> cons(X, n__from(n__s(X))),
                            from(X) -> n__from(X),
                   zWadr(XS, nil()) -> nil(),
                      zWadr(X1, X2) -> n__zWadr(X1, X2),
                   zWadr(nil(), YS) -> nil(),
    zWadr(cons(X, XS), cons(Y, YS)) ->
    cons(app(Y, cons(X, n__nil())), n__zWadr(activate(XS), activate(YS))),
                          prefix(X) -> n__prefix(X),
                          prefix(L) -> cons(nil(), n__zWadr(L, n__prefix(L))),
                               s(X) -> n__s(X)
   }
  Fail