MAYBE
Time: 3.350660
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 X,
        activate n__dbls X -> dbls X,
   activate n__sel(X1, X2) -> sel(X1, X2),
  activate n__indx(X1, X2) -> indx(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)}
 DP:
  DP:
   {                 dbl# s X -> s# n__s n__dbl activate X,
                     dbl# s X -> activate# X,
             activate# n__s X -> s# X,
           activate# n__dbl X -> dbl# X,
          activate# n__dbls X -> dbls# X,
     activate# n__sel(X1, X2) -> sel#(X1, X2),
    activate# n__indx(X1, X2) -> indx#(X1, X2),
          activate# n__from X -> from# X,
             dbls# cons(X, Y) -> activate# X,
             dbls# cons(X, Y) -> activate# Y,
        sel#(0(), cons(X, Y)) -> activate# X,
        sel#(s X, cons(Y, Z)) -> activate# X,
        sel#(s X, cons(Y, Z)) -> activate# Z,
        sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z),
         indx#(cons(X, Y), Z) -> activate# X,
         indx#(cons(X, Y), Z) -> activate# Y,
         indx#(cons(X, Y), Z) -> activate# Z,
                      from# X -> activate# X,
                    dbl1# s X -> activate# X,
                    dbl1# s X -> dbl1# activate X,
       sel1#(0(), cons(X, Y)) -> activate# X,
       sel1#(s X, cons(Y, Z)) -> activate# X,
       sel1#(s X, cons(Y, Z)) -> activate# Z,
       sel1#(s X, cons(Y, Z)) -> sel1#(activate X, activate Z),
                 quote# dbl X -> dbl1# X,
                   quote# s X -> activate# X,
                   quote# s X -> quote# activate X,
             quote# sel(X, Y) -> sel1#(X, Y)}
  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 X,
         activate n__dbls X -> dbls X,
    activate n__sel(X1, X2) -> sel(X1, X2),
   activate n__indx(X1, X2) -> indx(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)}
  UR:
   {                   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 X,
          activate n__dbls X -> dbls X,
     activate n__sel(X1, X2) -> sel(X1, X2),
    activate n__indx(X1, X2) -> indx(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,
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {(indx#(cons(X, Y), Z) -> activate# Y, activate# n__from X -> from# X)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__dbls X -> dbls# X)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__dbl X -> dbl# X)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__s X -> s# X)
     (dbl# s X -> activate# X, activate# n__from X -> from# X)
     (dbl# s X -> activate# X, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (dbl# s X -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (dbl# s X -> activate# X, activate# n__dbls X -> dbls# X)
     (dbl# s X -> activate# X, activate# n__dbl X -> dbl# X)
     (dbl# s X -> activate# X, activate# n__s X -> s# X)
     (activate# n__dbl X -> dbl# X, dbl# s X -> activate# X)
     (activate# n__dbl X -> dbl# X, dbl# s X -> s# n__s n__dbl activate X)
     (activate# n__from X -> from# X, from# X -> activate# X)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__from X -> from# X)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__dbls X -> dbls# X)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__dbl X -> dbl# X)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__s X -> s# X)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__from X -> from# X)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__dbls X -> dbls# X)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__dbl X -> dbl# X)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__s X -> s# X)
     (dbl1# s X -> activate# X, activate# n__from X -> from# X)
     (dbl1# s X -> activate# X, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (dbl1# s X -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (dbl1# s X -> activate# X, activate# n__dbls X -> dbls# X)
     (dbl1# s X -> activate# X, activate# n__dbl X -> dbl# X)
     (dbl1# s X -> activate# X, activate# n__s X -> s# X)
     (sel1#(s X, cons(Y, Z)) -> activate# X, activate# n__from X -> from# X)
     (sel1#(s X, cons(Y, Z)) -> activate# X, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (sel1#(s X, cons(Y, Z)) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (sel1#(s X, cons(Y, Z)) -> activate# X, activate# n__dbls X -> dbls# X)
     (sel1#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> dbl# X)
     (sel1#(s X, cons(Y, Z)) -> activate# X, activate# n__s X -> s# X)
     (quote# s X -> activate# X, activate# n__from X -> from# X)
     (quote# s X -> activate# X, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (quote# s X -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (quote# s X -> activate# X, activate# n__dbls X -> dbls# X)
     (quote# s X -> activate# X, activate# n__dbl X -> dbl# X)
     (quote# s X -> activate# X, activate# n__s X -> s# X)
     (quote# s X -> quote# activate X, quote# sel(X, Y) -> sel1#(X, Y))
     (quote# s X -> quote# activate X, quote# s X -> quote# activate X)
     (quote# s X -> quote# activate X, quote# s X -> activate# X)
     (quote# s X -> quote# activate X, quote# dbl X -> dbl1# X)
     (activate# n__indx(X1, X2) -> indx#(X1, X2), indx#(cons(X, Y), Z) -> activate# Z)
     (activate# n__indx(X1, X2) -> indx#(X1, X2), indx#(cons(X, Y), Z) -> activate# Y)
     (activate# n__indx(X1, X2) -> indx#(X1, X2), indx#(cons(X, Y), Z) -> activate# X)
     (sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z), sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z))
     (sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z), sel#(s X, cons(Y, Z)) -> activate# Z)
     (sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z), sel#(s X, cons(Y, Z)) -> activate# X)
     (sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z), sel#(0(), cons(X, Y)) -> activate# X)
     (sel1#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# X)
     (sel1#(s X, cons(Y, Z)) -> activate# Z, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (sel1#(s X, cons(Y, Z)) -> activate# Z, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (sel1#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbls X -> dbls# X)
     (sel1#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> dbl# X)
     (sel1#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# X)
     (sel1#(s X, cons(Y, Z)) -> sel1#(activate X, activate Z), sel1#(0(), cons(X, Y)) -> activate# X)
     (sel1#(s X, cons(Y, Z)) -> sel1#(activate X, activate Z), sel1#(s X, cons(Y, Z)) -> activate# X)
     (sel1#(s X, cons(Y, Z)) -> sel1#(activate X, activate Z), sel1#(s X, cons(Y, Z)) -> activate# Z)
     (sel1#(s X, cons(Y, Z)) -> sel1#(activate X, activate Z), sel1#(s X, cons(Y, Z)) -> sel1#(activate X, activate Z))
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__s X -> s# X)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__dbl X -> dbl# X)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__dbls X -> dbls# X)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__from X -> from# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> dbl# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbls X -> dbls# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# X)
     (activate# n__sel(X1, X2) -> sel#(X1, X2), sel#(0(), cons(X, Y)) -> activate# X)
     (activate# n__sel(X1, X2) -> sel#(X1, X2), sel#(s X, cons(Y, Z)) -> activate# X)
     (activate# n__sel(X1, X2) -> sel#(X1, X2), sel#(s X, cons(Y, Z)) -> activate# Z)
     (activate# n__sel(X1, X2) -> sel#(X1, X2), sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z))
     (dbl1# s X -> dbl1# activate X, dbl1# s X -> activate# X)
     (dbl1# s X -> dbl1# activate X, dbl1# s X -> dbl1# activate X)
     (quote# dbl X -> dbl1# X, dbl1# s X -> activate# X)
     (quote# dbl X -> dbl1# X, dbl1# s X -> dbl1# activate X)
     (sel1#(0(), cons(X, Y)) -> activate# X, activate# n__s X -> s# X)
     (sel1#(0(), cons(X, Y)) -> activate# X, activate# n__dbl X -> dbl# X)
     (sel1#(0(), cons(X, Y)) -> activate# X, activate# n__dbls X -> dbls# X)
     (sel1#(0(), cons(X, Y)) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (sel1#(0(), cons(X, Y)) -> activate# X, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (sel1#(0(), cons(X, Y)) -> activate# X, activate# n__from X -> from# X)
     (from# X -> activate# X, activate# n__s X -> s# X)
     (from# X -> activate# X, activate# n__dbl X -> dbl# X)
     (from# X -> activate# X, activate# n__dbls X -> dbls# X)
     (from# X -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (from# X -> activate# X, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (from# X -> activate# X, activate# n__from X -> from# X)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__s X -> s# X)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> dbl# X)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__dbls X -> dbls# X)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__from X -> from# X)
     (dbls# cons(X, Y) -> activate# X, activate# n__s X -> s# X)
     (dbls# cons(X, Y) -> activate# X, activate# n__dbl X -> dbl# X)
     (dbls# cons(X, Y) -> activate# X, activate# n__dbls X -> dbls# X)
     (dbls# cons(X, Y) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (dbls# cons(X, Y) -> activate# X, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (dbls# cons(X, Y) -> activate# X, activate# n__from X -> from# X)
     (activate# n__dbls X -> dbls# X, dbls# cons(X, Y) -> activate# X)
     (activate# n__dbls X -> dbls# X, dbls# cons(X, Y) -> activate# Y)
     (quote# sel(X, Y) -> sel1#(X, Y), sel1#(0(), cons(X, Y)) -> activate# X)
     (quote# sel(X, Y) -> sel1#(X, Y), sel1#(s X, cons(Y, Z)) -> activate# X)
     (quote# sel(X, Y) -> sel1#(X, Y), sel1#(s X, cons(Y, Z)) -> activate# Z)
     (quote# sel(X, Y) -> sel1#(X, Y), sel1#(s X, cons(Y, Z)) -> sel1#(activate X, activate Z))
     (dbls# cons(X, Y) -> activate# Y, activate# n__s X -> s# X)
     (dbls# cons(X, Y) -> activate# Y, activate# n__dbl X -> dbl# X)
     (dbls# cons(X, Y) -> activate# Y, activate# n__dbls X -> dbls# X)
     (dbls# cons(X, Y) -> activate# Y, activate# n__sel(X1, X2) -> sel#(X1, X2))
     (dbls# cons(X, Y) -> activate# Y, activate# n__indx(X1, X2) -> indx#(X1, X2))
     (dbls# cons(X, Y) -> activate# Y, activate# n__from X -> from# X)}
    STATUS:
     arrows: 0.844388
     SCCS (4):
      Scc:
       {quote# s X -> quote# activate X}
      Scc:
       {dbl1# s X -> dbl1# activate X}
      Scc:
       {sel1#(s X, cons(Y, Z)) -> sel1#(activate X, activate Z)}
      Scc:
       {                 dbl# s X -> activate# X,
               activate# n__dbl X -> dbl# X,
              activate# n__dbls X -> dbls# X,
         activate# n__sel(X1, X2) -> sel#(X1, X2),
        activate# n__indx(X1, X2) -> indx#(X1, X2),
              activate# n__from X -> from# X,
                 dbls# cons(X, Y) -> activate# X,
                 dbls# cons(X, Y) -> activate# Y,
            sel#(0(), cons(X, Y)) -> activate# X,
            sel#(s X, cons(Y, Z)) -> activate# X,
            sel#(s X, cons(Y, Z)) -> activate# Z,
            sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z),
             indx#(cons(X, Y), Z) -> activate# X,
             indx#(cons(X, Y), Z) -> activate# Y,
             indx#(cons(X, Y), Z) -> activate# Z,
                          from# X -> activate# X}
      
      SCC (1):
       Strict:
        {quote# s X -> quote# activate X}
       Weak:
       {                   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 X,
              activate n__dbls X -> dbls X,
         activate n__sel(X1, X2) -> sel(X1, X2),
        activate n__indx(X1, X2) -> indx(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)}
       Open
      
      
      SCC (1):
       Strict:
        {dbl1# s X -> dbl1# activate X}
       Weak:
       {                   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 X,
              activate n__dbls X -> dbls X,
         activate n__sel(X1, X2) -> sel(X1, X2),
        activate n__indx(X1, X2) -> indx(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)}
       Open
      
      
      SCC (1):
       Strict:
        {sel1#(s X, cons(Y, Z)) -> sel1#(activate X, activate Z)}
       Weak:
       {                   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 X,
              activate n__dbls X -> dbls X,
         activate n__sel(X1, X2) -> sel(X1, X2),
        activate n__indx(X1, X2) -> indx(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)}
       Open
      
      
      
      SCC (16):
       Strict:
        {                 dbl# s X -> activate# X,
                activate# n__dbl X -> dbl# X,
               activate# n__dbls X -> dbls# X,
          activate# n__sel(X1, X2) -> sel#(X1, X2),
         activate# n__indx(X1, X2) -> indx#(X1, X2),
               activate# n__from X -> from# X,
                  dbls# cons(X, Y) -> activate# X,
                  dbls# cons(X, Y) -> activate# Y,
             sel#(0(), cons(X, Y)) -> activate# X,
             sel#(s X, cons(Y, Z)) -> activate# X,
             sel#(s X, cons(Y, Z)) -> activate# Z,
             sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z),
              indx#(cons(X, Y), Z) -> activate# X,
              indx#(cons(X, Y), Z) -> activate# Y,
              indx#(cons(X, Y), Z) -> activate# Z,
                           from# X -> activate# X}
       Weak:
       {                   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 X,
              activate n__dbls X -> dbls X,
         activate n__sel(X1, X2) -> sel(X1, X2),
        activate n__indx(X1, X2) -> indx(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)}
       Open