MAYBE
MAYBE
TRS:
 {
                     dbl(X) -> n__dbl(X),
                   dbl(0()) -> 0(),
                  dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                       s(X) -> n__s(X),
                activate(X) -> X,
          activate(n__s(X)) -> s(X),
        activate(n__dbl(X)) -> dbl(activate(X)),
       activate(n__dbls(X)) -> dbls(activate(X)),
   activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)),
  activate(n__indx(X1, X2)) -> indx(activate(X1), X2),
       activate(n__from(X)) -> from(X),
                    dbls(X) -> n__dbls(X),
                dbls(nil()) -> nil(),
           dbls(cons(X, Y)) ->
  cons(n__dbl(activate(X)), n__dbls(activate(Y))),
                sel(X1, X2) -> n__sel(X1, X2),
       sel(0(), cons(X, Y)) -> activate(X),
      sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z)),
               indx(X1, X2) -> n__indx(X1, X2),
             indx(nil(), X) -> nil(),
        indx(cons(X, Y), Z) ->
  cons(n__sel(activate(X), activate(Z)), n__indx(activate(Y), activate(Z))),
                    from(X) -> cons(activate(X), n__from(n__s(activate(X)))),
                    from(X) -> n__from(X),
                  dbl1(0()) -> 01(),
                 dbl1(s(X)) -> s1(s1(dbl1(activate(X)))),
      sel1(0(), cons(X, Y)) -> activate(X),
     sel1(s(X), cons(Y, Z)) -> sel1(activate(X), activate(Z)),
                 quote(0()) -> 01(),
              quote(dbl(X)) -> dbl1(X),
                quote(s(X)) -> s1(quote(activate(X))),
           quote(sel(X, Y)) -> sel1(X, Y)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                       dbl(X) -> n__dbl(X),
                     dbl(0()) -> 0(),
                    dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                         s(X) -> n__s(X),
                  activate(X) -> X,
            activate(n__s(X)) -> s(X),
          activate(n__dbl(X)) -> dbl(activate(X)),
         activate(n__dbls(X)) -> dbls(activate(X)),
     activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)),
    activate(n__indx(X1, X2)) -> indx(activate(X1), X2),
         activate(n__from(X)) -> from(X),
                      dbls(X) -> n__dbls(X),
                  dbls(nil()) -> nil(),
             dbls(cons(X, Y)) ->
    cons(n__dbl(activate(X)), n__dbls(activate(Y))),
                  sel(X1, X2) -> n__sel(X1, X2),
         sel(0(), cons(X, Y)) -> activate(X),
        sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z)),
                 indx(X1, X2) -> n__indx(X1, X2),
               indx(nil(), X) -> nil(),
          indx(cons(X, Y), Z) ->
    cons(n__sel(activate(X), activate(Z)), n__indx(activate(Y), activate(Z))),
                      from(X) ->
    cons(activate(X), n__from(n__s(activate(X)))),
                      from(X) -> n__from(X),
                    dbl1(0()) -> 01(),
                   dbl1(s(X)) -> s1(s1(dbl1(activate(X)))),
        sel1(0(), cons(X, Y)) -> activate(X),
       sel1(s(X), cons(Y, Z)) -> sel1(activate(X), activate(Z)),
                   quote(0()) -> 01(),
                quote(dbl(X)) -> dbl1(X),
                  quote(s(X)) -> s1(quote(activate(X))),
             quote(sel(X, Y)) -> sel1(X, Y)
   }
  Fail