MAYBE
Time: 1.090009
TRS:
 {                a__dbl X -> dbl X,
                a__dbl 0() -> 0(),
                a__dbl s X -> s s dbl X,
                 a__dbls X -> dbls X,
             a__dbls nil() -> nil(),
        a__dbls cons(X, Y) -> cons(dbl X, dbls Y),
                  mark 0() -> 0(),
                  mark s X -> s X,
                mark dbl X -> a__dbl mark X,
                mark nil() -> nil(),
         mark cons(X1, X2) -> cons(X1, X2),
               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 01() -> 01(),
                 mark s1 X -> s1 mark X,
               mark dbl1 X -> a__dbl1 mark X,
         mark sel1(X1, X2) -> a__sel1(mark X1, mark X2),
              mark quote X -> a__quote mark X,
            a__sel(X1, X2) -> sel(X1, X2),
   a__sel(0(), cons(X, Y)) -> mark X,
   a__sel(s X, cons(Y, Z)) -> a__sel(mark X, mark Z),
           a__indx(X1, X2) -> indx(X1, X2),
         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),
                 a__from X -> from X,
                 a__dbl1 X -> dbl1 X,
               a__dbl1 0() -> 01(),
               a__dbl1 s X -> s1 s1 a__dbl1 mark X,
           a__sel1(X1, X2) -> sel1(X1, X2),
  a__sel1(0(), cons(X, Y)) -> mark X,
  a__sel1(s X, cons(Y, Z)) -> a__sel1(mark X, mark Z),
                a__quote X -> quote X,
              a__quote 0() -> 01(),
              a__quote s X -> s1 a__quote mark X,
            a__quote dbl X -> a__dbl1 mark X,
        a__quote sel(X, Y) -> a__sel1(mark X, mark Y)}
 DP:
  DP:
   {              mark# dbl X -> a__dbl# mark X,
                  mark# dbl X -> mark# X,
                 mark# dbls X -> a__dbls# mark X,
                 mark# dbls X -> mark# X,
            mark# sel(X1, X2) -> mark# X1,
            mark# sel(X1, X2) -> mark# X2,
            mark# sel(X1, X2) -> a__sel#(mark X1, mark X2),
           mark# indx(X1, X2) -> mark# X1,
           mark# indx(X1, X2) -> a__indx#(mark X1, X2),
                 mark# from X -> a__from# X,
                   mark# s1 X -> mark# X,
                 mark# dbl1 X -> mark# X,
                 mark# dbl1 X -> a__dbl1# mark X,
           mark# sel1(X1, X2) -> mark# X1,
           mark# sel1(X1, X2) -> mark# X2,
           mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2),
                mark# quote X -> mark# X,
                mark# quote X -> a__quote# mark X,
     a__sel#(0(), cons(X, Y)) -> mark# X,
     a__sel#(s X, cons(Y, Z)) -> mark# X,
     a__sel#(s X, cons(Y, Z)) -> mark# Z,
     a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z),
                 a__dbl1# s X -> mark# X,
                 a__dbl1# s X -> a__dbl1# mark X,
    a__sel1#(0(), cons(X, Y)) -> mark# X,
    a__sel1#(s X, cons(Y, Z)) -> mark# X,
    a__sel1#(s X, cons(Y, Z)) -> mark# Z,
    a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z),
                a__quote# s X -> mark# X,
                a__quote# s X -> a__quote# mark X,
              a__quote# dbl X -> mark# X,
              a__quote# dbl X -> a__dbl1# mark X,
          a__quote# sel(X, Y) -> mark# X,
          a__quote# sel(X, Y) -> mark# Y,
          a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y)}
  TRS:
  {                a__dbl X -> dbl X,
                 a__dbl 0() -> 0(),
                 a__dbl s X -> s s dbl X,
                  a__dbls X -> dbls X,
              a__dbls nil() -> nil(),
         a__dbls cons(X, Y) -> cons(dbl X, dbls Y),
                   mark 0() -> 0(),
                   mark s X -> s X,
                 mark dbl X -> a__dbl mark X,
                 mark nil() -> nil(),
          mark cons(X1, X2) -> cons(X1, X2),
                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 01() -> 01(),
                  mark s1 X -> s1 mark X,
                mark dbl1 X -> a__dbl1 mark X,
          mark sel1(X1, X2) -> a__sel1(mark X1, mark X2),
               mark quote X -> a__quote mark X,
             a__sel(X1, X2) -> sel(X1, X2),
    a__sel(0(), cons(X, Y)) -> mark X,
    a__sel(s X, cons(Y, Z)) -> a__sel(mark X, mark Z),
            a__indx(X1, X2) -> indx(X1, X2),
          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),
                  a__from X -> from X,
                  a__dbl1 X -> dbl1 X,
                a__dbl1 0() -> 01(),
                a__dbl1 s X -> s1 s1 a__dbl1 mark X,
            a__sel1(X1, X2) -> sel1(X1, X2),
   a__sel1(0(), cons(X, Y)) -> mark X,
   a__sel1(s X, cons(Y, Z)) -> a__sel1(mark X, mark Z),
                 a__quote X -> quote X,
               a__quote 0() -> 01(),
               a__quote s X -> s1 a__quote mark X,
             a__quote dbl X -> a__dbl1 mark X,
         a__quote sel(X, Y) -> a__sel1(mark X, mark Y)}
  EDG:
   {
    (mark# indx(X1, X2) -> mark# X1, mark# quote X -> a__quote# mark X)
    (mark# indx(X1, X2) -> mark# X1, mark# quote X -> mark# X)
    (mark# indx(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (mark# indx(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X2)
    (mark# indx(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X1)
    (mark# indx(X1, X2) -> mark# X1, mark# dbl1 X -> a__dbl1# mark X)
    (mark# indx(X1, X2) -> mark# X1, mark# dbl1 X -> mark# X)
    (mark# indx(X1, X2) -> mark# X1, mark# s1 X -> mark# X)
    (mark# indx(X1, X2) -> mark# X1, mark# from X -> a__from# X)
    (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> mark# X1)
    (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
    (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
    (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> mark# X)
    (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> a__dbls# mark X)
    (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> mark# X)
    (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X)
    (mark# dbl X -> mark# X, mark# quote X -> a__quote# mark X)
    (mark# dbl X -> mark# X, mark# quote X -> mark# X)
    (mark# dbl X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (mark# dbl X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (mark# dbl X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (mark# dbl X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (mark# dbl X -> mark# X, mark# dbl1 X -> mark# X)
    (mark# dbl X -> mark# X, mark# s1 X -> mark# X)
    (mark# dbl X -> mark# X, mark# from X -> a__from# X)
    (mark# dbl X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# dbl X -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (mark# dbl X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# dbl X -> mark# X, mark# dbls X -> mark# X)
    (mark# dbl X -> mark# X, mark# dbls X -> a__dbls# mark X)
    (mark# dbl X -> mark# X, mark# dbl X -> mark# X)
    (mark# dbl X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (mark# dbl1 X -> mark# X, mark# quote X -> a__quote# mark X)
    (mark# dbl1 X -> mark# X, mark# quote X -> mark# X)
    (mark# dbl1 X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (mark# dbl1 X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (mark# dbl1 X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (mark# dbl1 X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (mark# dbl1 X -> mark# X, mark# dbl1 X -> mark# X)
    (mark# dbl1 X -> mark# X, mark# s1 X -> mark# X)
    (mark# dbl1 X -> mark# X, mark# from X -> a__from# X)
    (mark# dbl1 X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# dbl1 X -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (mark# dbl1 X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# dbl1 X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# dbl1 X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# dbl1 X -> mark# X, mark# dbls X -> mark# X)
    (mark# dbl1 X -> mark# X, mark# dbls X -> a__dbls# mark X)
    (mark# dbl1 X -> mark# X, mark# dbl X -> mark# X)
    (mark# dbl1 X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# quote X -> a__quote# mark X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# quote X -> mark# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbl1 X -> mark# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# s1 X -> mark# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# from X -> a__from# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbls X -> mark# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbls X -> a__dbls# mark X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbl X -> mark# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__dbl1# s X -> mark# X, mark# quote X -> a__quote# mark X)
    (a__dbl1# s X -> mark# X, mark# quote X -> mark# X)
    (a__dbl1# s X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__dbl1# s X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (a__dbl1# s X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (a__dbl1# s X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (a__dbl1# s X -> mark# X, mark# dbl1 X -> mark# X)
    (a__dbl1# s X -> mark# X, mark# s1 X -> mark# X)
    (a__dbl1# s X -> mark# X, mark# from X -> a__from# X)
    (a__dbl1# s X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__dbl1# s X -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (a__dbl1# s X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__dbl1# s X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__dbl1# s X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__dbl1# s X -> mark# X, mark# dbls X -> mark# X)
    (a__dbl1# s X -> mark# X, mark# dbls X -> a__dbls# mark X)
    (a__dbl1# s X -> mark# X, mark# dbl X -> mark# X)
    (a__dbl1# s X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# quote X -> a__quote# mark X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# quote X -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbl1 X -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# s1 X -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# from X -> a__from# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbls X -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbls X -> a__dbls# mark X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbl X -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__quote# dbl X -> mark# X, mark# quote X -> a__quote# mark X)
    (a__quote# dbl X -> mark# X, mark# quote X -> mark# X)
    (a__quote# dbl X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__quote# dbl X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (a__quote# dbl X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (a__quote# dbl X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (a__quote# dbl X -> mark# X, mark# dbl1 X -> mark# X)
    (a__quote# dbl X -> mark# X, mark# s1 X -> mark# X)
    (a__quote# dbl X -> mark# X, mark# from X -> a__from# X)
    (a__quote# dbl X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__quote# dbl X -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (a__quote# dbl X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__quote# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__quote# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__quote# dbl X -> mark# X, mark# dbls X -> mark# X)
    (a__quote# dbl X -> mark# X, mark# dbls X -> a__dbls# mark X)
    (a__quote# dbl X -> mark# X, mark# dbl X -> mark# X)
    (a__quote# dbl X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# quote X -> a__quote# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# quote X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> mark# X2)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> mark# X1)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbl1 X -> a__dbl1# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbl1 X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# s1 X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# from X -> a__from# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# indx(X1, X2) -> mark# X1)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> mark# X2)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> mark# X1)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbls X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbls X -> a__dbls# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbl X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbl X -> a__dbl# mark X)
    (mark# sel1(X1, X2) -> mark# X2, mark# quote X -> a__quote# mark X)
    (mark# sel1(X1, X2) -> mark# X2, mark# quote X -> mark# X)
    (mark# sel1(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (mark# sel1(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> mark# X2)
    (mark# sel1(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> mark# X1)
    (mark# sel1(X1, X2) -> mark# X2, mark# dbl1 X -> a__dbl1# mark X)
    (mark# sel1(X1, X2) -> mark# X2, mark# dbl1 X -> mark# X)
    (mark# sel1(X1, X2) -> mark# X2, mark# s1 X -> mark# X)
    (mark# sel1(X1, X2) -> mark# X2, mark# from X -> a__from# X)
    (mark# sel1(X1, X2) -> mark# X2, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# sel1(X1, X2) -> mark# X2, mark# indx(X1, X2) -> mark# X1)
    (mark# sel1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# sel1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
    (mark# sel1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
    (mark# sel1(X1, X2) -> mark# X2, mark# dbls X -> mark# X)
    (mark# sel1(X1, X2) -> mark# X2, mark# dbls X -> a__dbls# mark X)
    (mark# sel1(X1, X2) -> mark# X2, mark# dbl X -> mark# X)
    (mark# sel1(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X)
    (mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2), a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z))
    (mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2), a__sel1#(s X, cons(Y, Z)) -> mark# Z)
    (mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2), a__sel1#(s X, cons(Y, Z)) -> mark# X)
    (mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2), a__sel1#(0(), cons(X, Y)) -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z), a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z))
    (a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z), a__sel1#(s X, cons(Y, Z)) -> mark# Z)
    (a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z), a__sel1#(s X, cons(Y, Z)) -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z), a__sel1#(0(), cons(X, Y)) -> mark# X)
    (a__quote# sel(X, Y) -> mark# Y, mark# quote X -> a__quote# mark X)
    (a__quote# sel(X, Y) -> mark# Y, mark# quote X -> mark# X)
    (a__quote# sel(X, Y) -> mark# Y, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__quote# sel(X, Y) -> mark# Y, mark# sel1(X1, X2) -> mark# X2)
    (a__quote# sel(X, Y) -> mark# Y, mark# sel1(X1, X2) -> mark# X1)
    (a__quote# sel(X, Y) -> mark# Y, mark# dbl1 X -> a__dbl1# mark X)
    (a__quote# sel(X, Y) -> mark# Y, mark# dbl1 X -> mark# X)
    (a__quote# sel(X, Y) -> mark# Y, mark# s1 X -> mark# X)
    (a__quote# sel(X, Y) -> mark# Y, mark# from X -> a__from# X)
    (a__quote# sel(X, Y) -> mark# Y, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__quote# sel(X, Y) -> mark# Y, mark# indx(X1, X2) -> mark# X1)
    (a__quote# sel(X, Y) -> mark# Y, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__quote# sel(X, Y) -> mark# Y, mark# sel(X1, X2) -> mark# X2)
    (a__quote# sel(X, Y) -> mark# Y, mark# sel(X1, X2) -> mark# X1)
    (a__quote# sel(X, Y) -> mark# Y, mark# dbls X -> mark# X)
    (a__quote# sel(X, Y) -> mark# Y, mark# dbls X -> a__dbls# mark X)
    (a__quote# sel(X, Y) -> mark# Y, mark# dbl X -> mark# X)
    (a__quote# sel(X, Y) -> mark# Y, mark# dbl X -> a__dbl# mark X)
    (mark# quote X -> a__quote# mark X, a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y))
    (mark# quote X -> a__quote# mark X, a__quote# sel(X, Y) -> mark# Y)
    (mark# quote X -> a__quote# mark X, a__quote# sel(X, Y) -> mark# X)
    (mark# quote X -> a__quote# mark X, a__quote# dbl X -> a__dbl1# mark X)
    (mark# quote X -> a__quote# mark X, a__quote# dbl X -> mark# X)
    (mark# quote X -> a__quote# mark X, a__quote# s X -> a__quote# mark X)
    (mark# quote X -> a__quote# mark X, a__quote# s X -> mark# X)
    (a__quote# s X -> a__quote# mark X, a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y))
    (a__quote# s X -> a__quote# mark X, a__quote# sel(X, Y) -> mark# Y)
    (a__quote# s X -> a__quote# mark X, a__quote# sel(X, Y) -> mark# X)
    (a__quote# s X -> a__quote# mark X, a__quote# dbl X -> a__dbl1# mark X)
    (a__quote# s X -> a__quote# mark X, a__quote# dbl X -> mark# X)
    (a__quote# s X -> a__quote# mark X, a__quote# s X -> a__quote# mark X)
    (a__quote# s X -> a__quote# mark X, a__quote# s X -> mark# X)
    (a__quote# dbl X -> a__dbl1# mark X, a__dbl1# s X -> mark# X)
    (a__quote# dbl X -> a__dbl1# mark X, a__dbl1# s X -> a__dbl1# mark X)
    (a__dbl1# s X -> a__dbl1# mark X, a__dbl1# s X -> mark# X)
    (a__dbl1# s X -> a__dbl1# mark X, a__dbl1# s X -> a__dbl1# mark X)
    (mark# dbl1 X -> a__dbl1# mark X, a__dbl1# s X -> mark# X)
    (mark# dbl1 X -> a__dbl1# mark X, a__dbl1# s X -> a__dbl1# mark X)
    (a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y), a__sel1#(0(), cons(X, Y)) -> mark# X)
    (a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y), a__sel1#(s X, cons(Y, Z)) -> mark# X)
    (a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y), a__sel1#(s X, cons(Y, Z)) -> mark# Z)
    (a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y), a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z))
    (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(0(), cons(X, Y)) -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(s X, cons(Y, Z)) -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(s X, cons(Y, Z)) -> mark# Z)
    (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z))
    (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(0(), cons(X, Y)) -> mark# X)
    (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s X, cons(Y, Z)) -> mark# X)
    (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s X, cons(Y, Z)) -> mark# Z)
    (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z))
    (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> a__dbls# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
    (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# sel(X1, X2) -> mark# X2, mark# from X -> a__from# X)
    (mark# sel(X1, X2) -> mark# X2, mark# s1 X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# dbl1 X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# dbl1 X -> a__dbl1# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> mark# X2)
    (mark# sel(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X2, mark# quote X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# quote X -> a__quote# mark X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbl X -> a__dbl# mark X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbl X -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbls X -> a__dbls# mark X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbls X -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> mark# X1)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> mark# X2)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# indx(X1, X2) -> mark# X1)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# from X -> a__from# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# s1 X -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbl1 X -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbl1 X -> a__dbl1# mark X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> mark# X1)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> mark# X2)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# quote X -> mark# X)
    (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# quote X -> a__quote# mark X)
    (a__quote# sel(X, Y) -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__quote# sel(X, Y) -> mark# X, mark# dbl X -> mark# X)
    (a__quote# sel(X, Y) -> mark# X, mark# dbls X -> a__dbls# mark X)
    (a__quote# sel(X, Y) -> mark# X, mark# dbls X -> mark# X)
    (a__quote# sel(X, Y) -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__quote# sel(X, Y) -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__quote# sel(X, Y) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__quote# sel(X, Y) -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (a__quote# sel(X, Y) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__quote# sel(X, Y) -> mark# X, mark# from X -> a__from# X)
    (a__quote# sel(X, Y) -> mark# X, mark# s1 X -> mark# X)
    (a__quote# sel(X, Y) -> mark# X, mark# dbl1 X -> mark# X)
    (a__quote# sel(X, Y) -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (a__quote# sel(X, Y) -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (a__quote# sel(X, Y) -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (a__quote# sel(X, Y) -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__quote# sel(X, Y) -> mark# X, mark# quote X -> mark# X)
    (a__quote# sel(X, Y) -> mark# X, mark# quote X -> a__quote# mark X)
    (a__quote# s X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__quote# s X -> mark# X, mark# dbl X -> mark# X)
    (a__quote# s X -> mark# X, mark# dbls X -> a__dbls# mark X)
    (a__quote# s X -> mark# X, mark# dbls X -> mark# X)
    (a__quote# s X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__quote# s X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__quote# s X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__quote# s X -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (a__quote# s X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__quote# s X -> mark# X, mark# from X -> a__from# X)
    (a__quote# s X -> mark# X, mark# s1 X -> mark# X)
    (a__quote# s X -> mark# X, mark# dbl1 X -> mark# X)
    (a__quote# s X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (a__quote# s X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (a__quote# s X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (a__quote# s X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__quote# s X -> mark# X, mark# quote X -> mark# X)
    (a__quote# s X -> mark# X, mark# quote X -> a__quote# mark X)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbl X -> mark# X)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbls X -> a__dbls# mark X)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbls X -> mark# X)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# from X -> a__from# X)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# s1 X -> mark# X)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbl1 X -> mark# X)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# quote X -> mark# X)
    (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# quote X -> a__quote# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbl X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbls X -> a__dbls# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbls X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# from X -> a__from# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# s1 X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbl1 X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# quote X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# quote X -> a__quote# mark X)
    (mark# quote X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (mark# quote X -> mark# X, mark# dbl X -> mark# X)
    (mark# quote X -> mark# X, mark# dbls X -> a__dbls# mark X)
    (mark# quote X -> mark# X, mark# dbls X -> mark# X)
    (mark# quote X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# quote X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# quote X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# quote X -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (mark# quote X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# quote X -> mark# X, mark# from X -> a__from# X)
    (mark# quote X -> mark# X, mark# s1 X -> mark# X)
    (mark# quote X -> mark# X, mark# dbl1 X -> mark# X)
    (mark# quote X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (mark# quote X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (mark# quote X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (mark# quote X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (mark# quote X -> mark# X, mark# quote X -> mark# X)
    (mark# quote X -> mark# X, mark# quote X -> a__quote# mark X)
    (mark# s1 X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (mark# s1 X -> mark# X, mark# dbl X -> mark# X)
    (mark# s1 X -> mark# X, mark# dbls X -> a__dbls# mark X)
    (mark# s1 X -> mark# X, mark# dbls X -> mark# X)
    (mark# s1 X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# s1 X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# s1 X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# s1 X -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (mark# s1 X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# s1 X -> mark# X, mark# from X -> a__from# X)
    (mark# s1 X -> mark# X, mark# s1 X -> mark# X)
    (mark# s1 X -> mark# X, mark# dbl1 X -> mark# X)
    (mark# s1 X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (mark# s1 X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (mark# s1 X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (mark# s1 X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (mark# s1 X -> mark# X, mark# quote X -> mark# X)
    (mark# s1 X -> mark# X, mark# quote X -> a__quote# mark X)
    (mark# dbls X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (mark# dbls X -> mark# X, mark# dbl X -> mark# X)
    (mark# dbls X -> mark# X, mark# dbls X -> a__dbls# mark X)
    (mark# dbls X -> mark# X, mark# dbls X -> mark# X)
    (mark# dbls X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# dbls X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# dbls X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# dbls X -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (mark# dbls X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# dbls X -> mark# X, mark# from X -> a__from# X)
    (mark# dbls X -> mark# X, mark# s1 X -> mark# X)
    (mark# dbls X -> mark# X, mark# dbl1 X -> mark# X)
    (mark# dbls X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
    (mark# dbls X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
    (mark# dbls X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
    (mark# dbls X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (mark# dbls X -> mark# X, mark# quote X -> mark# X)
    (mark# dbls X -> mark# X, mark# quote X -> a__quote# mark X)
    (mark# sel1(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X)
    (mark# sel1(X1, X2) -> mark# X1, mark# dbl X -> mark# X)
    (mark# sel1(X1, X2) -> mark# X1, mark# dbls X -> a__dbls# mark X)
    (mark# sel1(X1, X2) -> mark# X1, mark# dbls X -> mark# X)
    (mark# sel1(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
    (mark# sel1(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
    (mark# sel1(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# sel1(X1, X2) -> mark# X1, mark# indx(X1, X2) -> mark# X1)
    (mark# sel1(X1, X2) -> mark# X1, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# sel1(X1, X2) -> mark# X1, mark# from X -> a__from# X)
    (mark# sel1(X1, X2) -> mark# X1, mark# s1 X -> mark# X)
    (mark# sel1(X1, X2) -> mark# X1, mark# dbl1 X -> mark# X)
    (mark# sel1(X1, X2) -> mark# X1, mark# dbl1 X -> a__dbl1# mark X)
    (mark# sel1(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X1)
    (mark# sel1(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X2)
    (mark# sel1(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (mark# sel1(X1, X2) -> mark# X1, mark# quote X -> mark# X)
    (mark# sel1(X1, X2) -> mark# X1, mark# quote X -> a__quote# mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> mark# X)
    (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> a__dbls# mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> mark# X)
    (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
    (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X1, mark# indx(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X1, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# sel(X1, X2) -> mark# X1, mark# from X -> a__from# X)
    (mark# sel(X1, X2) -> mark# X1, mark# s1 X -> mark# X)
    (mark# sel(X1, X2) -> mark# X1, mark# dbl1 X -> mark# X)
    (mark# sel(X1, X2) -> mark# X1, mark# dbl1 X -> a__dbl1# mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X2)
    (mark# sel(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X1, mark# quote X -> mark# X)
    (mark# sel(X1, X2) -> mark# X1, mark# quote X -> a__quote# mark X)
   }
   EDG:
    {
     (mark# indx(X1, X2) -> mark# X1, mark# quote X -> a__quote# mark X)
     (mark# indx(X1, X2) -> mark# X1, mark# quote X -> mark# X)
     (mark# indx(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (mark# indx(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X2)
     (mark# indx(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X1)
     (mark# indx(X1, X2) -> mark# X1, mark# dbl1 X -> a__dbl1# mark X)
     (mark# indx(X1, X2) -> mark# X1, mark# dbl1 X -> mark# X)
     (mark# indx(X1, X2) -> mark# X1, mark# s1 X -> mark# X)
     (mark# indx(X1, X2) -> mark# X1, mark# from X -> a__from# X)
     (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> mark# X1)
     (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> mark# X)
     (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> a__dbls# mark X)
     (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> mark# X)
     (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X)
     (mark# dbl X -> mark# X, mark# quote X -> a__quote# mark X)
     (mark# dbl X -> mark# X, mark# quote X -> mark# X)
     (mark# dbl X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (mark# dbl X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (mark# dbl X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (mark# dbl X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (mark# dbl X -> mark# X, mark# dbl1 X -> mark# X)
     (mark# dbl X -> mark# X, mark# s1 X -> mark# X)
     (mark# dbl X -> mark# X, mark# from X -> a__from# X)
     (mark# dbl X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (mark# dbl X -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (mark# dbl X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# dbl X -> mark# X, mark# dbls X -> mark# X)
     (mark# dbl X -> mark# X, mark# dbls X -> a__dbls# mark X)
     (mark# dbl X -> mark# X, mark# dbl X -> mark# X)
     (mark# dbl X -> mark# X, mark# dbl X -> a__dbl# mark X)
     (mark# dbl1 X -> mark# X, mark# quote X -> a__quote# mark X)
     (mark# dbl1 X -> mark# X, mark# quote X -> mark# X)
     (mark# dbl1 X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (mark# dbl1 X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (mark# dbl1 X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (mark# dbl1 X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (mark# dbl1 X -> mark# X, mark# dbl1 X -> mark# X)
     (mark# dbl1 X -> mark# X, mark# s1 X -> mark# X)
     (mark# dbl1 X -> mark# X, mark# from X -> a__from# X)
     (mark# dbl1 X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (mark# dbl1 X -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (mark# dbl1 X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# dbl1 X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# dbl1 X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# dbl1 X -> mark# X, mark# dbls X -> mark# X)
     (mark# dbl1 X -> mark# X, mark# dbls X -> a__dbls# mark X)
     (mark# dbl1 X -> mark# X, mark# dbl X -> mark# X)
     (mark# dbl1 X -> mark# X, mark# dbl X -> a__dbl# mark X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# quote X -> a__quote# mark X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# quote X -> mark# X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbl1 X -> mark# X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# s1 X -> mark# X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# from X -> a__from# X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbls X -> mark# X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbls X -> a__dbls# mark X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbl X -> mark# X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbl X -> a__dbl# mark X)
     (a__dbl1# s X -> mark# X, mark# quote X -> a__quote# mark X)
     (a__dbl1# s X -> mark# X, mark# quote X -> mark# X)
     (a__dbl1# s X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__dbl1# s X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (a__dbl1# s X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (a__dbl1# s X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (a__dbl1# s X -> mark# X, mark# dbl1 X -> mark# X)
     (a__dbl1# s X -> mark# X, mark# s1 X -> mark# X)
     (a__dbl1# s X -> mark# X, mark# from X -> a__from# X)
     (a__dbl1# s X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__dbl1# s X -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (a__dbl1# s X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__dbl1# s X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__dbl1# s X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__dbl1# s X -> mark# X, mark# dbls X -> mark# X)
     (a__dbl1# s X -> mark# X, mark# dbls X -> a__dbls# mark X)
     (a__dbl1# s X -> mark# X, mark# dbl X -> mark# X)
     (a__dbl1# s X -> mark# X, mark# dbl X -> a__dbl# mark X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# quote X -> a__quote# mark X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# quote X -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbl1 X -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# s1 X -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# from X -> a__from# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbls X -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbls X -> a__dbls# mark X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbl X -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# X, mark# dbl X -> a__dbl# mark X)
     (a__quote# dbl X -> mark# X, mark# quote X -> a__quote# mark X)
     (a__quote# dbl X -> mark# X, mark# quote X -> mark# X)
     (a__quote# dbl X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__quote# dbl X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (a__quote# dbl X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (a__quote# dbl X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (a__quote# dbl X -> mark# X, mark# dbl1 X -> mark# X)
     (a__quote# dbl X -> mark# X, mark# s1 X -> mark# X)
     (a__quote# dbl X -> mark# X, mark# from X -> a__from# X)
     (a__quote# dbl X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__quote# dbl X -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (a__quote# dbl X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__quote# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__quote# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__quote# dbl X -> mark# X, mark# dbls X -> mark# X)
     (a__quote# dbl X -> mark# X, mark# dbls X -> a__dbls# mark X)
     (a__quote# dbl X -> mark# X, mark# dbl X -> mark# X)
     (a__quote# dbl X -> mark# X, mark# dbl X -> a__dbl# mark X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# quote X -> a__quote# mark X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# quote X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> mark# X2)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> mark# X1)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbl1 X -> a__dbl1# mark X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbl1 X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# s1 X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# from X -> a__from# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# indx(X1, X2) -> mark# X1)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> mark# X2)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> mark# X1)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbls X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbls X -> a__dbls# mark X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbl X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbl X -> a__dbl# mark X)
     (mark# sel1(X1, X2) -> mark# X2, mark# quote X -> a__quote# mark X)
     (mark# sel1(X1, X2) -> mark# X2, mark# quote X -> mark# X)
     (mark# sel1(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (mark# sel1(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> mark# X2)
     (mark# sel1(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> mark# X1)
     (mark# sel1(X1, X2) -> mark# X2, mark# dbl1 X -> a__dbl1# mark X)
     (mark# sel1(X1, X2) -> mark# X2, mark# dbl1 X -> mark# X)
     (mark# sel1(X1, X2) -> mark# X2, mark# s1 X -> mark# X)
     (mark# sel1(X1, X2) -> mark# X2, mark# from X -> a__from# X)
     (mark# sel1(X1, X2) -> mark# X2, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (mark# sel1(X1, X2) -> mark# X2, mark# indx(X1, X2) -> mark# X1)
     (mark# sel1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# sel1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
     (mark# sel1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
     (mark# sel1(X1, X2) -> mark# X2, mark# dbls X -> mark# X)
     (mark# sel1(X1, X2) -> mark# X2, mark# dbls X -> a__dbls# mark X)
     (mark# sel1(X1, X2) -> mark# X2, mark# dbl X -> mark# X)
     (mark# sel1(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X)
     (mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2), a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z))
     (mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2), a__sel1#(s X, cons(Y, Z)) -> mark# Z)
     (mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2), a__sel1#(s X, cons(Y, Z)) -> mark# X)
     (mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2), a__sel1#(0(), cons(X, Y)) -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z), a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z))
     (a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z), a__sel1#(s X, cons(Y, Z)) -> mark# Z)
     (a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z), a__sel1#(s X, cons(Y, Z)) -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z), a__sel1#(0(), cons(X, Y)) -> mark# X)
     (a__quote# sel(X, Y) -> mark# Y, mark# quote X -> a__quote# mark X)
     (a__quote# sel(X, Y) -> mark# Y, mark# quote X -> mark# X)
     (a__quote# sel(X, Y) -> mark# Y, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__quote# sel(X, Y) -> mark# Y, mark# sel1(X1, X2) -> mark# X2)
     (a__quote# sel(X, Y) -> mark# Y, mark# sel1(X1, X2) -> mark# X1)
     (a__quote# sel(X, Y) -> mark# Y, mark# dbl1 X -> a__dbl1# mark X)
     (a__quote# sel(X, Y) -> mark# Y, mark# dbl1 X -> mark# X)
     (a__quote# sel(X, Y) -> mark# Y, mark# s1 X -> mark# X)
     (a__quote# sel(X, Y) -> mark# Y, mark# from X -> a__from# X)
     (a__quote# sel(X, Y) -> mark# Y, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__quote# sel(X, Y) -> mark# Y, mark# indx(X1, X2) -> mark# X1)
     (a__quote# sel(X, Y) -> mark# Y, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__quote# sel(X, Y) -> mark# Y, mark# sel(X1, X2) -> mark# X2)
     (a__quote# sel(X, Y) -> mark# Y, mark# sel(X1, X2) -> mark# X1)
     (a__quote# sel(X, Y) -> mark# Y, mark# dbls X -> mark# X)
     (a__quote# sel(X, Y) -> mark# Y, mark# dbls X -> a__dbls# mark X)
     (a__quote# sel(X, Y) -> mark# Y, mark# dbl X -> mark# X)
     (a__quote# sel(X, Y) -> mark# Y, mark# dbl X -> a__dbl# mark X)
     (mark# quote X -> a__quote# mark X, a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y))
     (mark# quote X -> a__quote# mark X, a__quote# sel(X, Y) -> mark# Y)
     (mark# quote X -> a__quote# mark X, a__quote# sel(X, Y) -> mark# X)
     (mark# quote X -> a__quote# mark X, a__quote# dbl X -> a__dbl1# mark X)
     (mark# quote X -> a__quote# mark X, a__quote# dbl X -> mark# X)
     (mark# quote X -> a__quote# mark X, a__quote# s X -> a__quote# mark X)
     (mark# quote X -> a__quote# mark X, a__quote# s X -> mark# X)
     (a__quote# s X -> a__quote# mark X, a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y))
     (a__quote# s X -> a__quote# mark X, a__quote# sel(X, Y) -> mark# Y)
     (a__quote# s X -> a__quote# mark X, a__quote# sel(X, Y) -> mark# X)
     (a__quote# s X -> a__quote# mark X, a__quote# dbl X -> a__dbl1# mark X)
     (a__quote# s X -> a__quote# mark X, a__quote# dbl X -> mark# X)
     (a__quote# s X -> a__quote# mark X, a__quote# s X -> a__quote# mark X)
     (a__quote# s X -> a__quote# mark X, a__quote# s X -> mark# X)
     (a__quote# dbl X -> a__dbl1# mark X, a__dbl1# s X -> mark# X)
     (a__quote# dbl X -> a__dbl1# mark X, a__dbl1# s X -> a__dbl1# mark X)
     (a__dbl1# s X -> a__dbl1# mark X, a__dbl1# s X -> mark# X)
     (a__dbl1# s X -> a__dbl1# mark X, a__dbl1# s X -> a__dbl1# mark X)
     (mark# dbl1 X -> a__dbl1# mark X, a__dbl1# s X -> mark# X)
     (mark# dbl1 X -> a__dbl1# mark X, a__dbl1# s X -> a__dbl1# mark X)
     (a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y), a__sel1#(0(), cons(X, Y)) -> mark# X)
     (a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y), a__sel1#(s X, cons(Y, Z)) -> mark# X)
     (a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y), a__sel1#(s X, cons(Y, Z)) -> mark# Z)
     (a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y), a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z))
     (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(0(), cons(X, Y)) -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(s X, cons(Y, Z)) -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(s X, cons(Y, Z)) -> mark# Z)
     (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z))
     (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(0(), cons(X, Y)) -> mark# X)
     (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s X, cons(Y, Z)) -> mark# X)
     (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s X, cons(Y, Z)) -> mark# Z)
     (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z))
     (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> a__dbls# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (mark# sel(X1, X2) -> mark# X2, mark# from X -> a__from# X)
     (mark# sel(X1, X2) -> mark# X2, mark# s1 X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# dbl1 X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# dbl1 X -> a__dbl1# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X2, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X2, mark# quote X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# quote X -> a__quote# mark X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbl X -> a__dbl# mark X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbl X -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbls X -> a__dbls# mark X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbls X -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> mark# X1)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> mark# X2)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# indx(X1, X2) -> mark# X1)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# from X -> a__from# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# s1 X -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbl1 X -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# dbl1 X -> a__dbl1# mark X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> mark# X1)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> mark# X2)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# quote X -> mark# X)
     (a__sel1#(s X, cons(Y, Z)) -> mark# Z, mark# quote X -> a__quote# mark X)
     (a__quote# sel(X, Y) -> mark# X, mark# dbl X -> a__dbl# mark X)
     (a__quote# sel(X, Y) -> mark# X, mark# dbl X -> mark# X)
     (a__quote# sel(X, Y) -> mark# X, mark# dbls X -> a__dbls# mark X)
     (a__quote# sel(X, Y) -> mark# X, mark# dbls X -> mark# X)
     (a__quote# sel(X, Y) -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__quote# sel(X, Y) -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__quote# sel(X, Y) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__quote# sel(X, Y) -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (a__quote# sel(X, Y) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__quote# sel(X, Y) -> mark# X, mark# from X -> a__from# X)
     (a__quote# sel(X, Y) -> mark# X, mark# s1 X -> mark# X)
     (a__quote# sel(X, Y) -> mark# X, mark# dbl1 X -> mark# X)
     (a__quote# sel(X, Y) -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (a__quote# sel(X, Y) -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (a__quote# sel(X, Y) -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (a__quote# sel(X, Y) -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__quote# sel(X, Y) -> mark# X, mark# quote X -> mark# X)
     (a__quote# sel(X, Y) -> mark# X, mark# quote X -> a__quote# mark X)
     (a__quote# s X -> mark# X, mark# dbl X -> a__dbl# mark X)
     (a__quote# s X -> mark# X, mark# dbl X -> mark# X)
     (a__quote# s X -> mark# X, mark# dbls X -> a__dbls# mark X)
     (a__quote# s X -> mark# X, mark# dbls X -> mark# X)
     (a__quote# s X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__quote# s X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__quote# s X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__quote# s X -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (a__quote# s X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__quote# s X -> mark# X, mark# from X -> a__from# X)
     (a__quote# s X -> mark# X, mark# s1 X -> mark# X)
     (a__quote# s X -> mark# X, mark# dbl1 X -> mark# X)
     (a__quote# s X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (a__quote# s X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (a__quote# s X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (a__quote# s X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__quote# s X -> mark# X, mark# quote X -> mark# X)
     (a__quote# s X -> mark# X, mark# quote X -> a__quote# mark X)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbl X -> a__dbl# mark X)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbl X -> mark# X)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbls X -> a__dbls# mark X)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbls X -> mark# X)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# from X -> a__from# X)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# s1 X -> mark# X)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbl1 X -> mark# X)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# quote X -> mark# X)
     (a__sel1#(0(), cons(X, Y)) -> mark# X, mark# quote X -> a__quote# mark X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbl X -> a__dbl# mark X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbl X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbls X -> a__dbls# mark X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbls X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# from X -> a__from# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# s1 X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbl1 X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# quote X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# quote X -> a__quote# mark X)
     (mark# quote X -> mark# X, mark# dbl X -> a__dbl# mark X)
     (mark# quote X -> mark# X, mark# dbl X -> mark# X)
     (mark# quote X -> mark# X, mark# dbls X -> a__dbls# mark X)
     (mark# quote X -> mark# X, mark# dbls X -> mark# X)
     (mark# quote X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# quote X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# quote X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# quote X -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (mark# quote X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (mark# quote X -> mark# X, mark# from X -> a__from# X)
     (mark# quote X -> mark# X, mark# s1 X -> mark# X)
     (mark# quote X -> mark# X, mark# dbl1 X -> mark# X)
     (mark# quote X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (mark# quote X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (mark# quote X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (mark# quote X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (mark# quote X -> mark# X, mark# quote X -> mark# X)
     (mark# quote X -> mark# X, mark# quote X -> a__quote# mark X)
     (mark# s1 X -> mark# X, mark# dbl X -> a__dbl# mark X)
     (mark# s1 X -> mark# X, mark# dbl X -> mark# X)
     (mark# s1 X -> mark# X, mark# dbls X -> a__dbls# mark X)
     (mark# s1 X -> mark# X, mark# dbls X -> mark# X)
     (mark# s1 X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# s1 X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# s1 X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# s1 X -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (mark# s1 X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (mark# s1 X -> mark# X, mark# from X -> a__from# X)
     (mark# s1 X -> mark# X, mark# s1 X -> mark# X)
     (mark# s1 X -> mark# X, mark# dbl1 X -> mark# X)
     (mark# s1 X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (mark# s1 X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (mark# s1 X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (mark# s1 X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (mark# s1 X -> mark# X, mark# quote X -> mark# X)
     (mark# s1 X -> mark# X, mark# quote X -> a__quote# mark X)
     (mark# dbls X -> mark# X, mark# dbl X -> a__dbl# mark X)
     (mark# dbls X -> mark# X, mark# dbl X -> mark# X)
     (mark# dbls X -> mark# X, mark# dbls X -> a__dbls# mark X)
     (mark# dbls X -> mark# X, mark# dbls X -> mark# X)
     (mark# dbls X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# dbls X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# dbls X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# dbls X -> mark# X, mark# indx(X1, X2) -> mark# X1)
     (mark# dbls X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (mark# dbls X -> mark# X, mark# from X -> a__from# X)
     (mark# dbls X -> mark# X, mark# s1 X -> mark# X)
     (mark# dbls X -> mark# X, mark# dbl1 X -> mark# X)
     (mark# dbls X -> mark# X, mark# dbl1 X -> a__dbl1# mark X)
     (mark# dbls X -> mark# X, mark# sel1(X1, X2) -> mark# X1)
     (mark# dbls X -> mark# X, mark# sel1(X1, X2) -> mark# X2)
     (mark# dbls X -> mark# X, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (mark# dbls X -> mark# X, mark# quote X -> mark# X)
     (mark# dbls X -> mark# X, mark# quote X -> a__quote# mark X)
     (mark# sel1(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X)
     (mark# sel1(X1, X2) -> mark# X1, mark# dbl X -> mark# X)
     (mark# sel1(X1, X2) -> mark# X1, mark# dbls X -> a__dbls# mark X)
     (mark# sel1(X1, X2) -> mark# X1, mark# dbls X -> mark# X)
     (mark# sel1(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# sel1(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# sel1(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# sel1(X1, X2) -> mark# X1, mark# indx(X1, X2) -> mark# X1)
     (mark# sel1(X1, X2) -> mark# X1, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (mark# sel1(X1, X2) -> mark# X1, mark# from X -> a__from# X)
     (mark# sel1(X1, X2) -> mark# X1, mark# s1 X -> mark# X)
     (mark# sel1(X1, X2) -> mark# X1, mark# dbl1 X -> mark# X)
     (mark# sel1(X1, X2) -> mark# X1, mark# dbl1 X -> a__dbl1# mark X)
     (mark# sel1(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X1)
     (mark# sel1(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X2)
     (mark# sel1(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (mark# sel1(X1, X2) -> mark# X1, mark# quote X -> mark# X)
     (mark# sel1(X1, X2) -> mark# X1, mark# quote X -> a__quote# mark X)
     (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X)
     (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> a__dbls# mark X)
     (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X1, mark# indx(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
     (mark# sel(X1, X2) -> mark# X1, mark# from X -> a__from# X)
     (mark# sel(X1, X2) -> mark# X1, mark# s1 X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# dbl1 X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# dbl1 X -> a__dbl1# mark X)
     (mark# sel(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X1, mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X1, mark# quote X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# quote X -> a__quote# mark X)
    }
    STATUS:
     arrows: 0.658776
     SCCS (1):
      Scc:
       {              mark# dbl X -> mark# X,
                     mark# dbls X -> mark# X,
                mark# sel(X1, X2) -> mark# X1,
                mark# sel(X1, X2) -> mark# X2,
                mark# sel(X1, X2) -> a__sel#(mark X1, mark X2),
               mark# indx(X1, X2) -> mark# X1,
                       mark# s1 X -> mark# X,
                     mark# dbl1 X -> mark# X,
                     mark# dbl1 X -> a__dbl1# mark X,
               mark# sel1(X1, X2) -> mark# X1,
               mark# sel1(X1, X2) -> mark# X2,
               mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2),
                    mark# quote X -> mark# X,
                    mark# quote X -> a__quote# mark X,
         a__sel#(0(), cons(X, Y)) -> mark# X,
         a__sel#(s X, cons(Y, Z)) -> mark# X,
         a__sel#(s X, cons(Y, Z)) -> mark# Z,
         a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z),
                     a__dbl1# s X -> mark# X,
                     a__dbl1# s X -> a__dbl1# mark X,
        a__sel1#(0(), cons(X, Y)) -> mark# X,
        a__sel1#(s X, cons(Y, Z)) -> mark# X,
        a__sel1#(s X, cons(Y, Z)) -> mark# Z,
        a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z),
                    a__quote# s X -> mark# X,
                    a__quote# s X -> a__quote# mark X,
                  a__quote# dbl X -> mark# X,
                  a__quote# dbl X -> a__dbl1# mark X,
              a__quote# sel(X, Y) -> mark# X,
              a__quote# sel(X, Y) -> mark# Y,
              a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y)}
      
      SCC (31):
       Strict:
        {              mark# dbl X -> mark# X,
                      mark# dbls X -> mark# X,
                 mark# sel(X1, X2) -> mark# X1,
                 mark# sel(X1, X2) -> mark# X2,
                 mark# sel(X1, X2) -> a__sel#(mark X1, mark X2),
                mark# indx(X1, X2) -> mark# X1,
                        mark# s1 X -> mark# X,
                      mark# dbl1 X -> mark# X,
                      mark# dbl1 X -> a__dbl1# mark X,
                mark# sel1(X1, X2) -> mark# X1,
                mark# sel1(X1, X2) -> mark# X2,
                mark# sel1(X1, X2) -> a__sel1#(mark X1, mark X2),
                     mark# quote X -> mark# X,
                     mark# quote X -> a__quote# mark X,
          a__sel#(0(), cons(X, Y)) -> mark# X,
          a__sel#(s X, cons(Y, Z)) -> mark# X,
          a__sel#(s X, cons(Y, Z)) -> mark# Z,
          a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z),
                      a__dbl1# s X -> mark# X,
                      a__dbl1# s X -> a__dbl1# mark X,
         a__sel1#(0(), cons(X, Y)) -> mark# X,
         a__sel1#(s X, cons(Y, Z)) -> mark# X,
         a__sel1#(s X, cons(Y, Z)) -> mark# Z,
         a__sel1#(s X, cons(Y, Z)) -> a__sel1#(mark X, mark Z),
                     a__quote# s X -> mark# X,
                     a__quote# s X -> a__quote# mark X,
                   a__quote# dbl X -> mark# X,
                   a__quote# dbl X -> a__dbl1# mark X,
               a__quote# sel(X, Y) -> mark# X,
               a__quote# sel(X, Y) -> mark# Y,
               a__quote# sel(X, Y) -> a__sel1#(mark X, mark Y)}
       Weak:
       {                a__dbl X -> dbl X,
                      a__dbl 0() -> 0(),
                      a__dbl s X -> s s dbl X,
                       a__dbls X -> dbls X,
                   a__dbls nil() -> nil(),
              a__dbls cons(X, Y) -> cons(dbl X, dbls Y),
                        mark 0() -> 0(),
                        mark s X -> s X,
                      mark dbl X -> a__dbl mark X,
                      mark nil() -> nil(),
               mark cons(X1, X2) -> cons(X1, X2),
                     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 01() -> 01(),
                       mark s1 X -> s1 mark X,
                     mark dbl1 X -> a__dbl1 mark X,
               mark sel1(X1, X2) -> a__sel1(mark X1, mark X2),
                    mark quote X -> a__quote mark X,
                  a__sel(X1, X2) -> sel(X1, X2),
         a__sel(0(), cons(X, Y)) -> mark X,
         a__sel(s X, cons(Y, Z)) -> a__sel(mark X, mark Z),
                 a__indx(X1, X2) -> indx(X1, X2),
               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),
                       a__from X -> from X,
                       a__dbl1 X -> dbl1 X,
                     a__dbl1 0() -> 01(),
                     a__dbl1 s X -> s1 s1 a__dbl1 mark X,
                 a__sel1(X1, X2) -> sel1(X1, X2),
        a__sel1(0(), cons(X, Y)) -> mark X,
        a__sel1(s X, cons(Y, Z)) -> a__sel1(mark X, mark Z),
                      a__quote X -> quote X,
                    a__quote 0() -> 01(),
                    a__quote s X -> s1 a__quote mark X,
                  a__quote dbl X -> a__dbl1 mark X,
              a__quote sel(X, Y) -> a__sel1(mark X, mark Y)}
       Open