TRS:
 {             a__dbl(0()) -> 0(),
              a__dbl(s(X)) -> s(s(dbl(X))),
            a__dbls(nil()) -> nil(),
       a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)),
   a__sel(0(), cons(X, Y)) -> mark(X),
  a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)),
         a__indx(nil(), X) -> nil(),
    a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)),
                a__from(X) -> cons(X, from(s(X))),
              mark(dbl(X)) -> a__dbl(mark(X)),
             mark(dbls(X)) -> a__dbls(mark(X)),
         mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)),
        mark(indx(X1, X2)) -> a__indx(mark(X1), X2),
             mark(from(X)) -> a__from(X),
                 mark(0()) -> 0(),
                mark(s(X)) -> s(X),
               mark(nil()) -> nil(),
        mark(cons(X1, X2)) -> cons(X1, X2),
                 a__dbl(X) -> dbl(X),
                a__dbls(X) -> dbls(X),
            a__sel(X1, X2) -> sel(X1, X2),
           a__indx(X1, X2) -> indx(X1, X2),
                a__from(X) -> from(X)}
 Fail