MAYBE
MAYBE
TRS:
 {
                       mark(0()) -> active(0()),
                    mark(dbl(X)) -> active(dbl(mark(X))),
                      mark(s(X)) -> active(s(X)),
                     mark(nil()) -> active(nil()),
                   mark(dbls(X)) -> active(dbls(mark(X))),
              mark(cons(X1, X2)) -> active(cons(X1, X2)),
               mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
              mark(indx(X1, X2)) -> active(indx(mark(X1), X2)),
                   mark(from(X)) -> active(from(X)),
                      mark(01()) -> active(01()),
                   mark(dbl1(X)) -> active(dbl1(mark(X))),
                     mark(s1(X)) -> active(s1(mark(X))),
              mark(sel1(X1, X2)) -> active(sel1(mark(X1), mark(X2))),
                  mark(quote(X)) -> active(quote(mark(X))),
                active(dbl(0())) -> mark(0()),
               active(dbl(s(X))) -> mark(s(s(dbl(X)))),
             active(dbls(nil())) -> mark(nil()),
        active(dbls(cons(X, Y))) -> mark(cons(dbl(X), dbls(Y))),
    active(sel(0(), cons(X, Y))) -> mark(X),
   active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
          active(indx(nil(), X)) -> mark(nil()),
     active(indx(cons(X, Y), Z)) -> mark(cons(sel(X, Z), indx(Y, Z))),
                 active(from(X)) -> mark(cons(X, from(s(X)))),
               active(dbl1(0())) -> mark(01()),
              active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))),
   active(sel1(0(), cons(X, Y))) -> mark(X),
  active(sel1(s(X), cons(Y, Z))) -> mark(sel1(X, Z)),
              active(quote(0())) -> mark(01()),
           active(quote(dbl(X))) -> mark(dbl1(X)),
             active(quote(s(X))) -> mark(s1(quote(X))),
        active(quote(sel(X, Y))) -> mark(sel1(X, Y)),
                    dbl(mark(X)) -> dbl(X),
                  dbl(active(X)) -> dbl(X),
                      s(mark(X)) -> s(X),
                    s(active(X)) -> s(X),
                   dbls(mark(X)) -> dbls(X),
                 dbls(active(X)) -> dbls(X),
              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),
               sel(X1, mark(X2)) -> sel(X1, X2),
             sel(X1, active(X2)) -> sel(X1, X2),
               sel(mark(X1), X2) -> sel(X1, X2),
             sel(active(X1), X2) -> sel(X1, X2),
              indx(X1, mark(X2)) -> indx(X1, X2),
            indx(X1, active(X2)) -> indx(X1, X2),
              indx(mark(X1), X2) -> indx(X1, X2),
            indx(active(X1), X2) -> indx(X1, X2),
                   from(mark(X)) -> from(X),
                 from(active(X)) -> from(X),
                   dbl1(mark(X)) -> dbl1(X),
                 dbl1(active(X)) -> dbl1(X),
                     s1(mark(X)) -> s1(X),
                   s1(active(X)) -> s1(X),
              sel1(X1, mark(X2)) -> sel1(X1, X2),
            sel1(X1, active(X2)) -> sel1(X1, X2),
              sel1(mark(X1), X2) -> sel1(X1, X2),
            sel1(active(X1), X2) -> sel1(X1, X2),
                  quote(mark(X)) -> quote(X),
                quote(active(X)) -> quote(X)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                         mark(0()) -> active(0()),
                      mark(dbl(X)) -> active(dbl(mark(X))),
                        mark(s(X)) -> active(s(X)),
                       mark(nil()) -> active(nil()),
                     mark(dbls(X)) -> active(dbls(mark(X))),
                mark(cons(X1, X2)) -> active(cons(X1, X2)),
                 mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                mark(indx(X1, X2)) -> active(indx(mark(X1), X2)),
                     mark(from(X)) -> active(from(X)),
                        mark(01()) -> active(01()),
                     mark(dbl1(X)) -> active(dbl1(mark(X))),
                       mark(s1(X)) -> active(s1(mark(X))),
                mark(sel1(X1, X2)) -> active(sel1(mark(X1), mark(X2))),
                    mark(quote(X)) -> active(quote(mark(X))),
                  active(dbl(0())) -> mark(0()),
                 active(dbl(s(X))) -> mark(s(s(dbl(X)))),
               active(dbls(nil())) -> mark(nil()),
          active(dbls(cons(X, Y))) -> mark(cons(dbl(X), dbls(Y))),
      active(sel(0(), cons(X, Y))) -> mark(X),
     active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)),
            active(indx(nil(), X)) -> mark(nil()),
       active(indx(cons(X, Y), Z)) -> mark(cons(sel(X, Z), indx(Y, Z))),
                   active(from(X)) -> mark(cons(X, from(s(X)))),
                 active(dbl1(0())) -> mark(01()),
                active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))),
     active(sel1(0(), cons(X, Y))) -> mark(X),
    active(sel1(s(X), cons(Y, Z))) -> mark(sel1(X, Z)),
                active(quote(0())) -> mark(01()),
             active(quote(dbl(X))) -> mark(dbl1(X)),
               active(quote(s(X))) -> mark(s1(quote(X))),
          active(quote(sel(X, Y))) -> mark(sel1(X, Y)),
                      dbl(mark(X)) -> dbl(X),
                    dbl(active(X)) -> dbl(X),
                        s(mark(X)) -> s(X),
                      s(active(X)) -> s(X),
                     dbls(mark(X)) -> dbls(X),
                   dbls(active(X)) -> dbls(X),
                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),
                 sel(X1, mark(X2)) -> sel(X1, X2),
               sel(X1, active(X2)) -> sel(X1, X2),
                 sel(mark(X1), X2) -> sel(X1, X2),
               sel(active(X1), X2) -> sel(X1, X2),
                indx(X1, mark(X2)) -> indx(X1, X2),
              indx(X1, active(X2)) -> indx(X1, X2),
                indx(mark(X1), X2) -> indx(X1, X2),
              indx(active(X1), X2) -> indx(X1, X2),
                     from(mark(X)) -> from(X),
                   from(active(X)) -> from(X),
                     dbl1(mark(X)) -> dbl1(X),
                   dbl1(active(X)) -> dbl1(X),
                       s1(mark(X)) -> s1(X),
                     s1(active(X)) -> s1(X),
                sel1(X1, mark(X2)) -> sel1(X1, X2),
              sel1(X1, active(X2)) -> sel1(X1, X2),
                sel1(mark(X1), X2) -> sel1(X1, X2),
              sel1(active(X1), X2) -> sel1(X1, X2),
                    quote(mark(X)) -> quote(X),
                  quote(active(X)) -> quote(X)
   }
  Fail