MAYBE
MAYBE
TRS:
 {
                        mark(app(X1, X2)) -> active(app(mark(X1), mark(X2))),
                              mark(nil()) -> active(nil()),
                       mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                            mark(from(X)) -> active(from(mark(X))),
                               mark(s(X)) -> active(s(mark(X))),
                      mark(zWadr(X1, X2)) ->
  active(zWadr(mark(X1), mark(X2))),
                          mark(prefix(X)) -> active(prefix(mark(X))),
                   active(app(nil(), YS)) -> mark(YS),
             active(app(cons(X, XS), YS)) -> mark(cons(X, app(XS, YS))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                 active(zWadr(XS, nil())) -> mark(nil()),
                 active(zWadr(nil(), YS)) -> mark(nil()),
  active(zWadr(cons(X, XS), cons(Y, YS))) ->
  mark(cons(app(Y, cons(X, nil())), zWadr(XS, YS))),
                        active(prefix(L)) ->
  mark(cons(nil(), zWadr(L, prefix(L)))),
                        app(X1, mark(X2)) -> app(X1, X2),
                      app(X1, active(X2)) -> app(X1, X2),
                        app(mark(X1), X2) -> app(X1, X2),
                      app(active(X1), X2) -> app(X1, X2),
                       cons(X1, mark(X2)) -> cons(X1, X2),
                     cons(X1, active(X2)) -> cons(X1, X2),
                       cons(mark(X1), X2) -> cons(X1, X2),
                     cons(active(X1), X2) -> cons(X1, X2),
                            from(mark(X)) -> from(X),
                          from(active(X)) -> from(X),
                               s(mark(X)) -> s(X),
                             s(active(X)) -> s(X),
                      zWadr(X1, mark(X2)) -> zWadr(X1, X2),
                    zWadr(X1, active(X2)) -> zWadr(X1, X2),
                      zWadr(mark(X1), X2) -> zWadr(X1, X2),
                    zWadr(active(X1), X2) -> zWadr(X1, X2),
                          prefix(mark(X)) -> prefix(X),
                        prefix(active(X)) -> prefix(X)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                          mark(app(X1, X2)) ->
    active(app(mark(X1), mark(X2))),
                                mark(nil()) -> active(nil()),
                         mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                              mark(from(X)) -> active(from(mark(X))),
                                 mark(s(X)) -> active(s(mark(X))),
                        mark(zWadr(X1, X2)) ->
    active(zWadr(mark(X1), mark(X2))),
                            mark(prefix(X)) -> active(prefix(mark(X))),
                     active(app(nil(), YS)) -> mark(YS),
               active(app(cons(X, XS), YS)) -> mark(cons(X, app(XS, YS))),
                            active(from(X)) -> mark(cons(X, from(s(X)))),
                   active(zWadr(XS, nil())) -> mark(nil()),
                   active(zWadr(nil(), YS)) -> mark(nil()),
    active(zWadr(cons(X, XS), cons(Y, YS))) ->
    mark(cons(app(Y, cons(X, nil())), zWadr(XS, YS))),
                          active(prefix(L)) ->
    mark(cons(nil(), zWadr(L, prefix(L)))),
                          app(X1, mark(X2)) -> app(X1, X2),
                        app(X1, active(X2)) -> app(X1, X2),
                          app(mark(X1), X2) -> app(X1, X2),
                        app(active(X1), X2) -> app(X1, X2),
                         cons(X1, mark(X2)) -> cons(X1, X2),
                       cons(X1, active(X2)) -> cons(X1, X2),
                         cons(mark(X1), X2) -> cons(X1, X2),
                       cons(active(X1), X2) -> cons(X1, X2),
                              from(mark(X)) -> from(X),
                            from(active(X)) -> from(X),
                                 s(mark(X)) -> s(X),
                               s(active(X)) -> s(X),
                        zWadr(X1, mark(X2)) -> zWadr(X1, X2),
                      zWadr(X1, active(X2)) -> zWadr(X1, X2),
                        zWadr(mark(X1), X2) -> zWadr(X1, X2),
                      zWadr(active(X1), X2) -> zWadr(X1, X2),
                            prefix(mark(X)) -> prefix(X),
                          prefix(active(X)) -> prefix(X)
   }
  Fail