MAYBE
Time: 0.141446
TRS:
 {                active dbl X -> dbl active X,
                active dbl 0() -> mark 0(),
                active dbl s X -> mark s s dbl X,
                 active dbls X -> dbls active X,
             active dbls nil() -> mark nil(),
        active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
            active sel(X1, X2) -> sel(X1, active X2),
            active sel(X1, X2) -> sel(active X1, X2),
   active sel(0(), cons(X, Y)) -> mark X,
   active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
           active indx(X1, X2) -> indx(active X1, X2),
         active indx(nil(), X) -> mark nil(),
    active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                 active from X -> mark cons(X, from s X),
                 active dbl1 X -> dbl1 active X,
               active dbl1 0() -> mark 01(),
               active dbl1 s X -> mark s1 s1 dbl1 X,
                   active s1 X -> s1 active X,
           active sel1(X1, X2) -> sel1(X1, active X2),
           active sel1(X1, X2) -> sel1(active X1, X2),
  active sel1(0(), cons(X, Y)) -> mark X,
  active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                active quote X -> quote active X,
              active quote 0() -> mark 01(),
            active quote dbl X -> mark dbl1 X,
              active quote s X -> mark s1 quote X,
        active quote sel(X, Y) -> mark sel1(X, Y),
                    dbl mark X -> mark dbl X,
                      dbl ok X -> ok dbl X,
                        s ok X -> ok s X,
                   dbls mark X -> mark dbls X,
                     dbls ok X -> ok dbls X,
            cons(ok X1, ok X2) -> ok cons(X1, X2),
              sel(X1, mark X2) -> mark sel(X1, X2),
              sel(mark X1, X2) -> mark sel(X1, X2),
             sel(ok X1, ok X2) -> ok sel(X1, X2),
             indx(mark X1, X2) -> mark indx(X1, X2),
            indx(ok X1, ok X2) -> ok indx(X1, X2),
                     from ok X -> ok from X,
                   dbl1 mark X -> mark dbl1 X,
                     dbl1 ok X -> ok dbl1 X,
                     s1 mark X -> mark s1 X,
                       s1 ok X -> ok s1 X,
             sel1(X1, mark X2) -> mark sel1(X1, X2),
             sel1(mark X1, X2) -> mark sel1(X1, X2),
            sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                  quote mark X -> mark quote X,
                    quote ok X -> ok quote X,
                    proper 0() -> ok 0(),
                  proper dbl X -> dbl proper X,
                    proper s X -> s proper X,
                  proper nil() -> ok nil(),
                 proper dbls X -> dbls proper X,
           proper cons(X1, X2) -> cons(proper X1, proper X2),
            proper sel(X1, X2) -> sel(proper X1, proper X2),
           proper indx(X1, X2) -> indx(proper X1, proper X2),
                 proper from X -> from proper X,
                   proper 01() -> ok 01(),
                 proper dbl1 X -> dbl1 proper X,
                   proper s1 X -> s1 proper X,
           proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                proper quote X -> quote proper X,
                    top mark X -> top proper X,
                      top ok X -> top active X}
 DP:
  DP:
   {                active# dbl X -> active# X,
                    active# dbl X -> dbl# active X,
                  active# dbl s X -> dbl# X,
                  active# dbl s X -> s# dbl X,
                  active# dbl s X -> s# s dbl X,
                   active# dbls X -> active# X,
                   active# dbls X -> dbls# active X,
          active# dbls cons(X, Y) -> dbl# X,
          active# dbls cons(X, Y) -> dbls# Y,
          active# dbls cons(X, Y) -> cons#(dbl X, dbls Y),
              active# sel(X1, X2) -> active# X1,
              active# sel(X1, X2) -> active# X2,
              active# sel(X1, X2) -> sel#(X1, active X2),
              active# sel(X1, X2) -> sel#(active X1, X2),
     active# sel(s X, cons(Y, Z)) -> sel#(X, Z),
             active# indx(X1, X2) -> active# X1,
             active# indx(X1, X2) -> indx#(active X1, X2),
      active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)),
      active# indx(cons(X, Y), Z) -> sel#(X, Z),
      active# indx(cons(X, Y), Z) -> indx#(Y, Z),
                   active# from X -> s# X,
                   active# from X -> cons#(X, from s X),
                   active# from X -> from# s X,
                   active# dbl1 X -> active# X,
                   active# dbl1 X -> dbl1# active X,
                 active# dbl1 s X -> dbl1# X,
                 active# dbl1 s X -> s1# dbl1 X,
                 active# dbl1 s X -> s1# s1 dbl1 X,
                     active# s1 X -> active# X,
                     active# s1 X -> s1# active X,
             active# sel1(X1, X2) -> active# X1,
             active# sel1(X1, X2) -> active# X2,
             active# sel1(X1, X2) -> sel1#(X1, active X2),
             active# sel1(X1, X2) -> sel1#(active X1, X2),
    active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z),
                  active# quote X -> active# X,
                  active# quote X -> quote# active X,
              active# quote dbl X -> dbl1# X,
                active# quote s X -> s1# quote X,
                active# quote s X -> quote# X,
          active# quote sel(X, Y) -> sel1#(X, Y),
                      dbl# mark X -> dbl# X,
                        dbl# ok X -> dbl# X,
                          s# ok X -> s# X,
                     dbls# mark X -> dbls# X,
                       dbls# ok X -> dbls# X,
              cons#(ok X1, ok X2) -> cons#(X1, X2),
                sel#(X1, mark X2) -> sel#(X1, X2),
                sel#(mark X1, X2) -> sel#(X1, X2),
               sel#(ok X1, ok X2) -> sel#(X1, X2),
               indx#(mark X1, X2) -> indx#(X1, X2),
              indx#(ok X1, ok X2) -> indx#(X1, X2),
                       from# ok X -> from# X,
                     dbl1# mark X -> dbl1# X,
                       dbl1# ok X -> dbl1# X,
                       s1# mark X -> s1# X,
                         s1# ok X -> s1# X,
               sel1#(X1, mark X2) -> sel1#(X1, X2),
               sel1#(mark X1, X2) -> sel1#(X1, X2),
              sel1#(ok X1, ok X2) -> sel1#(X1, X2),
                    quote# mark X -> quote# X,
                      quote# ok X -> quote# X,
                    proper# dbl X -> dbl# proper X,
                    proper# dbl X -> proper# X,
                      proper# s X -> s# proper X,
                      proper# s X -> proper# X,
                   proper# dbls X -> dbls# proper X,
                   proper# dbls X -> proper# X,
             proper# cons(X1, X2) -> cons#(proper X1, proper X2),
             proper# cons(X1, X2) -> proper# X1,
             proper# cons(X1, X2) -> proper# X2,
              proper# sel(X1, X2) -> sel#(proper X1, proper X2),
              proper# sel(X1, X2) -> proper# X1,
              proper# sel(X1, X2) -> proper# X2,
             proper# indx(X1, X2) -> indx#(proper X1, proper X2),
             proper# indx(X1, X2) -> proper# X1,
             proper# indx(X1, X2) -> proper# X2,
                   proper# from X -> from# proper X,
                   proper# from X -> proper# X,
                   proper# dbl1 X -> dbl1# proper X,
                   proper# dbl1 X -> proper# X,
                     proper# s1 X -> s1# proper X,
                     proper# s1 X -> proper# X,
             proper# sel1(X1, X2) -> sel1#(proper X1, proper X2),
             proper# sel1(X1, X2) -> proper# X1,
             proper# sel1(X1, X2) -> proper# X2,
                  proper# quote X -> quote# proper X,
                  proper# quote X -> proper# X,
                      top# mark X -> proper# X,
                      top# mark X -> top# proper X,
                        top# ok X -> active# X,
                        top# ok X -> top# active X}
  TRS:
  {                active dbl X -> dbl active X,
                 active dbl 0() -> mark 0(),
                 active dbl s X -> mark s s dbl X,
                  active dbls X -> dbls active X,
              active dbls nil() -> mark nil(),
         active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
             active sel(X1, X2) -> sel(X1, active X2),
             active sel(X1, X2) -> sel(active X1, X2),
    active sel(0(), cons(X, Y)) -> mark X,
    active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
            active indx(X1, X2) -> indx(active X1, X2),
          active indx(nil(), X) -> mark nil(),
     active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                  active from X -> mark cons(X, from s X),
                  active dbl1 X -> dbl1 active X,
                active dbl1 0() -> mark 01(),
                active dbl1 s X -> mark s1 s1 dbl1 X,
                    active s1 X -> s1 active X,
            active sel1(X1, X2) -> sel1(X1, active X2),
            active sel1(X1, X2) -> sel1(active X1, X2),
   active sel1(0(), cons(X, Y)) -> mark X,
   active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                 active quote X -> quote active X,
               active quote 0() -> mark 01(),
             active quote dbl X -> mark dbl1 X,
               active quote s X -> mark s1 quote X,
         active quote sel(X, Y) -> mark sel1(X, Y),
                     dbl mark X -> mark dbl X,
                       dbl ok X -> ok dbl X,
                         s ok X -> ok s X,
                    dbls mark X -> mark dbls X,
                      dbls ok X -> ok dbls X,
             cons(ok X1, ok X2) -> ok cons(X1, X2),
               sel(X1, mark X2) -> mark sel(X1, X2),
               sel(mark X1, X2) -> mark sel(X1, X2),
              sel(ok X1, ok X2) -> ok sel(X1, X2),
              indx(mark X1, X2) -> mark indx(X1, X2),
             indx(ok X1, ok X2) -> ok indx(X1, X2),
                      from ok X -> ok from X,
                    dbl1 mark X -> mark dbl1 X,
                      dbl1 ok X -> ok dbl1 X,
                      s1 mark X -> mark s1 X,
                        s1 ok X -> ok s1 X,
              sel1(X1, mark X2) -> mark sel1(X1, X2),
              sel1(mark X1, X2) -> mark sel1(X1, X2),
             sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                   quote mark X -> mark quote X,
                     quote ok X -> ok quote X,
                     proper 0() -> ok 0(),
                   proper dbl X -> dbl proper X,
                     proper s X -> s proper X,
                   proper nil() -> ok nil(),
                  proper dbls X -> dbls proper X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
             proper sel(X1, X2) -> sel(proper X1, proper X2),
            proper indx(X1, X2) -> indx(proper X1, proper X2),
                  proper from X -> from proper X,
                    proper 01() -> ok 01(),
                  proper dbl1 X -> dbl1 proper X,
                    proper s1 X -> s1 proper X,
            proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                 proper quote X -> quote proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
  UR:
   {                active dbl X -> dbl active X,
                  active dbl 0() -> mark 0(),
                  active dbl s X -> mark s s dbl X,
                   active dbls X -> dbls active X,
               active dbls nil() -> mark nil(),
          active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
              active sel(X1, X2) -> sel(X1, active X2),
              active sel(X1, X2) -> sel(active X1, X2),
     active sel(0(), cons(X, Y)) -> mark X,
     active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
             active indx(X1, X2) -> indx(active X1, X2),
           active indx(nil(), X) -> mark nil(),
      active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                   active from X -> mark cons(X, from s X),
                   active dbl1 X -> dbl1 active X,
                 active dbl1 0() -> mark 01(),
                 active dbl1 s X -> mark s1 s1 dbl1 X,
                     active s1 X -> s1 active X,
             active sel1(X1, X2) -> sel1(X1, active X2),
             active sel1(X1, X2) -> sel1(active X1, X2),
    active sel1(0(), cons(X, Y)) -> mark X,
    active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                  active quote X -> quote active X,
                active quote 0() -> mark 01(),
              active quote dbl X -> mark dbl1 X,
                active quote s X -> mark s1 quote X,
          active quote sel(X, Y) -> mark sel1(X, Y),
                      dbl mark X -> mark dbl X,
                        dbl ok X -> ok dbl X,
                          s ok X -> ok s X,
                     dbls mark X -> mark dbls X,
                       dbls ok X -> ok dbls X,
              cons(ok X1, ok X2) -> ok cons(X1, X2),
                sel(X1, mark X2) -> mark sel(X1, X2),
                sel(mark X1, X2) -> mark sel(X1, X2),
               sel(ok X1, ok X2) -> ok sel(X1, X2),
               indx(mark X1, X2) -> mark indx(X1, X2),
              indx(ok X1, ok X2) -> ok indx(X1, X2),
                       from ok X -> ok from X,
                     dbl1 mark X -> mark dbl1 X,
                       dbl1 ok X -> ok dbl1 X,
                       s1 mark X -> mark s1 X,
                         s1 ok X -> ok s1 X,
               sel1(X1, mark X2) -> mark sel1(X1, X2),
               sel1(mark X1, X2) -> mark sel1(X1, X2),
              sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                    quote mark X -> mark quote X,
                      quote ok X -> ok quote X,
                      proper 0() -> ok 0(),
                    proper dbl X -> dbl proper X,
                      proper s X -> s proper X,
                    proper nil() -> ok nil(),
                   proper dbls X -> dbls proper X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
              proper sel(X1, X2) -> sel(proper X1, proper X2),
             proper indx(X1, X2) -> indx(proper X1, proper X2),
                   proper from X -> from proper X,
                     proper 01() -> ok 01(),
                   proper dbl1 X -> dbl1 proper X,
                     proper s1 X -> s1 proper X,
             proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                  proper quote X -> quote proper X,
                         a(x, y) -> x,
                         a(x, y) -> y}
   EDG:
    {
     (active# dbl s X -> s# dbl X, s# ok X -> s# X)
     (active# from X -> from# s X, from# ok X -> from# X)
     (active# dbl1 s X -> s1# dbl1 X, s1# ok X -> s1# X)
     (active# dbl1 s X -> s1# dbl1 X, s1# mark X -> s1# X)
     (active# quote X -> quote# active X, quote# ok X -> quote# X)
     (active# quote X -> quote# active X, quote# mark X -> quote# X)
     (proper# dbl X -> dbl# proper X, dbl# ok X -> dbl# X)
     (proper# dbl X -> dbl# proper X, dbl# mark X -> dbl# X)
     (proper# dbls X -> dbls# proper X, dbls# ok X -> dbls# X)
     (proper# dbls X -> dbls# proper X, dbls# mark X -> dbls# X)
     (proper# dbl1 X -> dbl1# proper X, dbl1# ok X -> dbl1# X)
     (proper# dbl1 X -> dbl1# proper X, dbl1# mark X -> dbl1# X)
     (proper# quote X -> quote# proper X, quote# ok X -> quote# X)
     (proper# quote X -> quote# proper X, quote# mark X -> quote# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (sel#(X1, mark X2) -> sel#(X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
     (sel#(X1, mark X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
     (sel#(X1, mark X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
     (sel#(ok X1, ok X2) -> sel#(X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
     (sel#(ok X1, ok X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
     (sel#(ok X1, ok X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
     (indx#(ok X1, ok X2) -> indx#(X1, X2), indx#(ok X1, ok X2) -> indx#(X1, X2))
     (indx#(ok X1, ok X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2))
     (sel1#(mark X1, X2) -> sel1#(X1, X2), sel1#(ok X1, ok X2) -> sel1#(X1, X2))
     (sel1#(mark X1, X2) -> sel1#(X1, X2), sel1#(mark X1, X2) -> sel1#(X1, X2))
     (sel1#(mark X1, X2) -> sel1#(X1, X2), sel1#(X1, mark X2) -> sel1#(X1, X2))
     (active# sel(X1, X2) -> active# X2, active# quote sel(X, Y) -> sel1#(X, Y))
     (active# sel(X1, X2) -> active# X2, active# quote s X -> quote# X)
     (active# sel(X1, X2) -> active# X2, active# quote s X -> s1# quote X)
     (active# sel(X1, X2) -> active# X2, active# quote dbl X -> dbl1# X)
     (active# sel(X1, X2) -> active# X2, active# quote X -> quote# active X)
     (active# sel(X1, X2) -> active# X2, active# quote X -> active# X)
     (active# sel(X1, X2) -> active# X2, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (active# sel(X1, X2) -> active# X2, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (active# sel(X1, X2) -> active# X2, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (active# sel(X1, X2) -> active# X2, active# sel1(X1, X2) -> active# X2)
     (active# sel(X1, X2) -> active# X2, active# sel1(X1, X2) -> active# X1)
     (active# sel(X1, X2) -> active# X2, active# s1 X -> s1# active X)
     (active# sel(X1, X2) -> active# X2, active# s1 X -> active# X)
     (active# sel(X1, X2) -> active# X2, active# dbl1 s X -> s1# s1 dbl1 X)
     (active# sel(X1, X2) -> active# X2, active# dbl1 s X -> s1# dbl1 X)
     (active# sel(X1, X2) -> active# X2, active# dbl1 s X -> dbl1# X)
     (active# sel(X1, X2) -> active# X2, active# dbl1 X -> dbl1# active X)
     (active# sel(X1, X2) -> active# X2, active# dbl1 X -> active# X)
     (active# sel(X1, X2) -> active# X2, active# from X -> from# s X)
     (active# sel(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
     (active# sel(X1, X2) -> active# X2, active# from X -> s# X)
     (active# sel(X1, X2) -> active# X2, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# sel(X1, X2) -> active# X2, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (active# sel(X1, X2) -> active# X2, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# sel(X1, X2) -> active# X2, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# sel(X1, X2) -> active# X2, active# indx(X1, X2) -> active# X1)
     (active# sel(X1, X2) -> active# X2, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X2)
     (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X1)
     (active# sel(X1, X2) -> active# X2, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# sel(X1, X2) -> active# X2, active# dbls cons(X, Y) -> dbls# Y)
     (active# sel(X1, X2) -> active# X2, active# dbls cons(X, Y) -> dbl# X)
     (active# sel(X1, X2) -> active# X2, active# dbls X -> dbls# active X)
     (active# sel(X1, X2) -> active# X2, active# dbls X -> active# X)
     (active# sel(X1, X2) -> active# X2, active# dbl s X -> s# s dbl X)
     (active# sel(X1, X2) -> active# X2, active# dbl s X -> s# dbl X)
     (active# sel(X1, X2) -> active# X2, active# dbl s X -> dbl# X)
     (active# sel(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
     (active# sel(X1, X2) -> active# X2, active# dbl X -> active# X)
     (proper# cons(X1, X2) -> proper# X2, proper# quote X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# quote X -> quote# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# s1 X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# s1 X -> s1# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# dbl1 X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# dbl1 X -> dbl1# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# indx(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# indx(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# dbls X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# dbls X -> dbls# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
     (proper# indx(X1, X2) -> proper# X2, proper# quote X -> proper# X)
     (proper# indx(X1, X2) -> proper# X2, proper# quote X -> quote# proper X)
     (proper# indx(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> proper# X2)
     (proper# indx(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> proper# X1)
     (proper# indx(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# indx(X1, X2) -> proper# X2, proper# s1 X -> proper# X)
     (proper# indx(X1, X2) -> proper# X2, proper# s1 X -> s1# proper X)
     (proper# indx(X1, X2) -> proper# X2, proper# dbl1 X -> proper# X)
     (proper# indx(X1, X2) -> proper# X2, proper# dbl1 X -> dbl1# proper X)
     (proper# indx(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# indx(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# indx(X1, X2) -> proper# X2, proper# indx(X1, X2) -> proper# X2)
     (proper# indx(X1, X2) -> proper# X2, proper# indx(X1, X2) -> proper# X1)
     (proper# indx(X1, X2) -> proper# X2, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# indx(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
     (proper# indx(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
     (proper# indx(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# indx(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# indx(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# indx(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# indx(X1, X2) -> proper# X2, proper# dbls X -> proper# X)
     (proper# indx(X1, X2) -> proper# X2, proper# dbls X -> dbls# proper X)
     (proper# indx(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# indx(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# indx(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
     (proper# indx(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
     (active# dbls cons(X, Y) -> dbls# Y, dbls# ok X -> dbls# X)
     (active# dbls cons(X, Y) -> dbls# Y, dbls# mark X -> dbls# X)
     (active# indx(X1, X2) -> active# X1, active# quote sel(X, Y) -> sel1#(X, Y))
     (active# indx(X1, X2) -> active# X1, active# quote s X -> quote# X)
     (active# indx(X1, X2) -> active# X1, active# quote s X -> s1# quote X)
     (active# indx(X1, X2) -> active# X1, active# quote dbl X -> dbl1# X)
     (active# indx(X1, X2) -> active# X1, active# quote X -> quote# active X)
     (active# indx(X1, X2) -> active# X1, active# quote X -> active# X)
     (active# indx(X1, X2) -> active# X1, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (active# indx(X1, X2) -> active# X1, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (active# indx(X1, X2) -> active# X1, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (active# indx(X1, X2) -> active# X1, active# sel1(X1, X2) -> active# X2)
     (active# indx(X1, X2) -> active# X1, active# sel1(X1, X2) -> active# X1)
     (active# indx(X1, X2) -> active# X1, active# s1 X -> s1# active X)
     (active# indx(X1, X2) -> active# X1, active# s1 X -> active# X)
     (active# indx(X1, X2) -> active# X1, active# dbl1 s X -> s1# s1 dbl1 X)
     (active# indx(X1, X2) -> active# X1, active# dbl1 s X -> s1# dbl1 X)
     (active# indx(X1, X2) -> active# X1, active# dbl1 s X -> dbl1# X)
     (active# indx(X1, X2) -> active# X1, active# dbl1 X -> dbl1# active X)
     (active# indx(X1, X2) -> active# X1, active# dbl1 X -> active# X)
     (active# indx(X1, X2) -> active# X1, active# from X -> from# s X)
     (active# indx(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# indx(X1, X2) -> active# X1, active# from X -> s# X)
     (active# indx(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# indx(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (active# indx(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# indx(X1, X2) -> active# X1, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# indx(X1, X2) -> active# X1, active# indx(X1, X2) -> active# X1)
     (active# indx(X1, X2) -> active# X1, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# indx(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# indx(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# indx(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X2)
     (active# indx(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
     (active# indx(X1, X2) -> active# X1, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# indx(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbls# Y)
     (active# indx(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbl# X)
     (active# indx(X1, X2) -> active# X1, active# dbls X -> dbls# active X)
     (active# indx(X1, X2) -> active# X1, active# dbls X -> active# X)
     (active# indx(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
     (active# indx(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
     (active# indx(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
     (active# indx(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
     (active# indx(X1, X2) -> active# X1, active# dbl X -> active# X)
     (proper# cons(X1, X2) -> proper# X1, proper# quote X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# quote X -> quote# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# s1 X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# s1 X -> s1# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# dbl1 X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# dbl1 X -> dbl1# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# indx(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# indx(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# dbls X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# dbls X -> dbls# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
     (proper# indx(X1, X2) -> proper# X1, proper# quote X -> proper# X)
     (proper# indx(X1, X2) -> proper# X1, proper# quote X -> quote# proper X)
     (proper# indx(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> proper# X2)
     (proper# indx(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> proper# X1)
     (proper# indx(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# indx(X1, X2) -> proper# X1, proper# s1 X -> proper# X)
     (proper# indx(X1, X2) -> proper# X1, proper# s1 X -> s1# proper X)
     (proper# indx(X1, X2) -> proper# X1, proper# dbl1 X -> proper# X)
     (proper# indx(X1, X2) -> proper# X1, proper# dbl1 X -> dbl1# proper X)
     (proper# indx(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# indx(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# indx(X1, X2) -> proper# X1, proper# indx(X1, X2) -> proper# X2)
     (proper# indx(X1, X2) -> proper# X1, proper# indx(X1, X2) -> proper# X1)
     (proper# indx(X1, X2) -> proper# X1, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# indx(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X2)
     (proper# indx(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X1)
     (proper# indx(X1, X2) -> proper# X1, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# indx(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# indx(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# indx(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# indx(X1, X2) -> proper# X1, proper# dbls X -> proper# X)
     (proper# indx(X1, X2) -> proper# X1, proper# dbls X -> dbls# proper X)
     (proper# indx(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# indx(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# indx(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
     (proper# indx(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
     (active# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# sel1(X1, X2) -> sel1#(X1, active X2), sel1#(ok X1, ok X2) -> sel1#(X1, X2))
     (active# sel1(X1, X2) -> sel1#(X1, active X2), sel1#(mark X1, X2) -> sel1#(X1, X2))
     (active# sel1(X1, X2) -> sel1#(X1, active X2), sel1#(X1, mark X2) -> sel1#(X1, X2))
     (proper# sel(X1, X2) -> sel#(proper X1, proper X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
     (proper# sel(X1, X2) -> sel#(proper X1, proper X2), sel#(mark X1, X2) -> sel#(X1, X2))
     (proper# sel(X1, X2) -> sel#(proper X1, proper X2), sel#(X1, mark X2) -> sel#(X1, X2))
     (proper# sel1(X1, X2) -> sel1#(proper X1, proper X2), sel1#(ok X1, ok X2) -> sel1#(X1, X2))
     (proper# sel1(X1, X2) -> sel1#(proper X1, proper X2), sel1#(mark X1, X2) -> sel1#(X1, X2))
     (proper# sel1(X1, X2) -> sel1#(proper X1, proper X2), sel1#(X1, mark X2) -> sel1#(X1, X2))
     (active# dbl X -> active# X, active# quote sel(X, Y) -> sel1#(X, Y))
     (active# dbl X -> active# X, active# quote s X -> quote# X)
     (active# dbl X -> active# X, active# quote s X -> s1# quote X)
     (active# dbl X -> active# X, active# quote dbl X -> dbl1# X)
     (active# dbl X -> active# X, active# quote X -> quote# active X)
     (active# dbl X -> active# X, active# quote X -> active# X)
     (active# dbl X -> active# X, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (active# dbl X -> active# X, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (active# dbl X -> active# X, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (active# dbl X -> active# X, active# sel1(X1, X2) -> active# X2)
     (active# dbl X -> active# X, active# sel1(X1, X2) -> active# X1)
     (active# dbl X -> active# X, active# s1 X -> s1# active X)
     (active# dbl X -> active# X, active# s1 X -> active# X)
     (active# dbl X -> active# X, active# dbl1 s X -> s1# s1 dbl1 X)
     (active# dbl X -> active# X, active# dbl1 s X -> s1# dbl1 X)
     (active# dbl X -> active# X, active# dbl1 s X -> dbl1# X)
     (active# dbl X -> active# X, active# dbl1 X -> dbl1# active X)
     (active# dbl X -> active# X, active# dbl1 X -> active# X)
     (active# dbl X -> active# X, active# from X -> from# s X)
     (active# dbl X -> active# X, active# from X -> cons#(X, from s X))
     (active# dbl X -> active# X, active# from X -> s# X)
     (active# dbl X -> active# X, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# dbl X -> active# X, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (active# dbl X -> active# X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# dbl X -> active# X, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# dbl X -> active# X, active# indx(X1, X2) -> active# X1)
     (active# dbl X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# dbl X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# dbl X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# dbl X -> active# X, active# sel(X1, X2) -> active# X2)
     (active# dbl X -> active# X, active# sel(X1, X2) -> active# X1)
     (active# dbl X -> active# X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# dbl X -> active# X, active# dbls cons(X, Y) -> dbls# Y)
     (active# dbl X -> active# X, active# dbls cons(X, Y) -> dbl# X)
     (active# dbl X -> active# X, active# dbls X -> dbls# active X)
     (active# dbl X -> active# X, active# dbls X -> active# X)
     (active# dbl X -> active# X, active# dbl s X -> s# s dbl X)
     (active# dbl X -> active# X, active# dbl s X -> s# dbl X)
     (active# dbl X -> active# X, active# dbl s X -> dbl# X)
     (active# dbl X -> active# X, active# dbl X -> dbl# active X)
     (active# dbl X -> active# X, active# dbl X -> active# X)
     (active# dbls X -> active# X, active# quote sel(X, Y) -> sel1#(X, Y))
     (active# dbls X -> active# X, active# quote s X -> quote# X)
     (active# dbls X -> active# X, active# quote s X -> s1# quote X)
     (active# dbls X -> active# X, active# quote dbl X -> dbl1# X)
     (active# dbls X -> active# X, active# quote X -> quote# active X)
     (active# dbls X -> active# X, active# quote X -> active# X)
     (active# dbls X -> active# X, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (active# dbls X -> active# X, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (active# dbls X -> active# X, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (active# dbls X -> active# X, active# sel1(X1, X2) -> active# X2)
     (active# dbls X -> active# X, active# sel1(X1, X2) -> active# X1)
     (active# dbls X -> active# X, active# s1 X -> s1# active X)
     (active# dbls X -> active# X, active# s1 X -> active# X)
     (active# dbls X -> active# X, active# dbl1 s X -> s1# s1 dbl1 X)
     (active# dbls X -> active# X, active# dbl1 s X -> s1# dbl1 X)
     (active# dbls X -> active# X, active# dbl1 s X -> dbl1# X)
     (active# dbls X -> active# X, active# dbl1 X -> dbl1# active X)
     (active# dbls X -> active# X, active# dbl1 X -> active# X)
     (active# dbls X -> active# X, active# from X -> from# s X)
     (active# dbls X -> active# X, active# from X -> cons#(X, from s X))
     (active# dbls X -> active# X, active# from X -> s# X)
     (active# dbls X -> active# X, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# dbls X -> active# X, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (active# dbls X -> active# X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# dbls X -> active# X, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# dbls X -> active# X, active# indx(X1, X2) -> active# X1)
     (active# dbls X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# dbls X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# dbls X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# dbls X -> active# X, active# sel(X1, X2) -> active# X2)
     (active# dbls X -> active# X, active# sel(X1, X2) -> active# X1)
     (active# dbls X -> active# X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# dbls X -> active# X, active# dbls cons(X, Y) -> dbls# Y)
     (active# dbls X -> active# X, active# dbls cons(X, Y) -> dbl# X)
     (active# dbls X -> active# X, active# dbls X -> dbls# active X)
     (active# dbls X -> active# X, active# dbls X -> active# X)
     (active# dbls X -> active# X, active# dbl s X -> s# s dbl X)
     (active# dbls X -> active# X, active# dbl s X -> s# dbl X)
     (active# dbls X -> active# X, active# dbl s X -> dbl# X)
     (active# dbls X -> active# X, active# dbl X -> dbl# active X)
     (active# dbls X -> active# X, active# dbl X -> active# X)
     (active# from X -> s# X, s# ok X -> s# X)
     (active# dbl1 s X -> dbl1# X, dbl1# ok X -> dbl1# X)
     (active# dbl1 s X -> dbl1# X, dbl1# mark X -> dbl1# X)
     (active# quote X -> active# X, active# quote sel(X, Y) -> sel1#(X, Y))
     (active# quote X -> active# X, active# quote s X -> quote# X)
     (active# quote X -> active# X, active# quote s X -> s1# quote X)
     (active# quote X -> active# X, active# quote dbl X -> dbl1# X)
     (active# quote X -> active# X, active# quote X -> quote# active X)
     (active# quote X -> active# X, active# quote X -> active# X)
     (active# quote X -> active# X, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (active# quote X -> active# X, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (active# quote X -> active# X, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (active# quote X -> active# X, active# sel1(X1, X2) -> active# X2)
     (active# quote X -> active# X, active# sel1(X1, X2) -> active# X1)
     (active# quote X -> active# X, active# s1 X -> s1# active X)
     (active# quote X -> active# X, active# s1 X -> active# X)
     (active# quote X -> active# X, active# dbl1 s X -> s1# s1 dbl1 X)
     (active# quote X -> active# X, active# dbl1 s X -> s1# dbl1 X)
     (active# quote X -> active# X, active# dbl1 s X -> dbl1# X)
     (active# quote X -> active# X, active# dbl1 X -> dbl1# active X)
     (active# quote X -> active# X, active# dbl1 X -> active# X)
     (active# quote X -> active# X, active# from X -> from# s X)
     (active# quote X -> active# X, active# from X -> cons#(X, from s X))
     (active# quote X -> active# X, active# from X -> s# X)
     (active# quote X -> active# X, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# quote X -> active# X, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (active# quote X -> active# X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# quote X -> active# X, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# quote X -> active# X, active# indx(X1, X2) -> active# X1)
     (active# quote X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# quote X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# quote X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# quote X -> active# X, active# sel(X1, X2) -> active# X2)
     (active# quote X -> active# X, active# sel(X1, X2) -> active# X1)
     (active# quote X -> active# X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# quote X -> active# X, active# dbls cons(X, Y) -> dbls# Y)
     (active# quote X -> active# X, active# dbls cons(X, Y) -> dbl# X)
     (active# quote X -> active# X, active# dbls X -> dbls# active X)
     (active# quote X -> active# X, active# dbls X -> active# X)
     (active# quote X -> active# X, active# dbl s X -> s# s dbl X)
     (active# quote X -> active# X, active# dbl s X -> s# dbl X)
     (active# quote X -> active# X, active# dbl s X -> dbl# X)
     (active# quote X -> active# X, active# dbl X -> dbl# active X)
     (active# quote X -> active# X, active# dbl X -> active# X)
     (active# quote s X -> quote# X, quote# ok X -> quote# X)
     (active# quote s X -> quote# X, quote# mark X -> quote# X)
     (dbl# ok X -> dbl# X, dbl# ok X -> dbl# X)
     (dbl# ok X -> dbl# X, dbl# mark X -> dbl# X)
     (dbls# mark X -> dbls# X, dbls# ok X -> dbls# X)
     (dbls# mark X -> dbls# X, dbls# mark X -> dbls# X)
     (from# ok X -> from# X, from# ok X -> from# X)
     (dbl1# ok X -> dbl1# X, dbl1# ok X -> dbl1# X)
     (dbl1# ok X -> dbl1# X, dbl1# mark X -> dbl1# X)
     (s1# ok X -> s1# X, s1# ok X -> s1# X)
     (s1# ok X -> s1# X, s1# mark X -> s1# X)
     (quote# ok X -> quote# X, quote# ok X -> quote# X)
     (quote# ok X -> quote# X, quote# mark X -> quote# X)
     (proper# s X -> proper# X, proper# quote X -> proper# X)
     (proper# s X -> proper# X, proper# quote X -> quote# proper X)
     (proper# s X -> proper# X, proper# sel1(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# sel1(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# s1 X -> proper# X)
     (proper# s X -> proper# X, proper# s1 X -> s1# proper X)
     (proper# s X -> proper# X, proper# dbl1 X -> proper# X)
     (proper# s X -> proper# X, proper# dbl1 X -> dbl1# proper X)
     (proper# s X -> proper# X, proper# from X -> proper# X)
     (proper# s X -> proper# X, proper# from X -> from# proper X)
     (proper# s X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# dbls X -> proper# X)
     (proper# s X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# dbl X -> proper# X)
     (proper# s X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# from X -> proper# X, proper# quote X -> proper# X)
     (proper# from X -> proper# X, proper# quote X -> quote# proper X)
     (proper# from X -> proper# X, proper# sel1(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# sel1(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# s1 X -> proper# X)
     (proper# from X -> proper# X, proper# s1 X -> s1# proper X)
     (proper# from X -> proper# X, proper# dbl1 X -> proper# X)
     (proper# from X -> proper# X, proper# dbl1 X -> dbl1# proper X)
     (proper# from X -> proper# X, proper# from X -> proper# X)
     (proper# from X -> proper# X, proper# from X -> from# proper X)
     (proper# from X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# dbls X -> proper# X)
     (proper# from X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# from X -> proper# X, proper# s X -> proper# X)
     (proper# from X -> proper# X, proper# s X -> s# proper X)
     (proper# from X -> proper# X, proper# dbl X -> proper# X)
     (proper# from X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# s1 X -> proper# X, proper# quote X -> proper# X)
     (proper# s1 X -> proper# X, proper# quote X -> quote# proper X)
     (proper# s1 X -> proper# X, proper# sel1(X1, X2) -> proper# X2)
     (proper# s1 X -> proper# X, proper# sel1(X1, X2) -> proper# X1)
     (proper# s1 X -> proper# X, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# s1 X -> proper# X, proper# s1 X -> proper# X)
     (proper# s1 X -> proper# X, proper# s1 X -> s1# proper X)
     (proper# s1 X -> proper# X, proper# dbl1 X -> proper# X)
     (proper# s1 X -> proper# X, proper# dbl1 X -> dbl1# proper X)
     (proper# s1 X -> proper# X, proper# from X -> proper# X)
     (proper# s1 X -> proper# X, proper# from X -> from# proper X)
     (proper# s1 X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# s1 X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# s1 X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# s1 X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# s1 X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# s1 X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# s1 X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# s1 X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# s1 X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# s1 X -> proper# X, proper# dbls X -> proper# X)
     (proper# s1 X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# s1 X -> proper# X, proper# s X -> proper# X)
     (proper# s1 X -> proper# X, proper# s X -> s# proper X)
     (proper# s1 X -> proper# X, proper# dbl X -> proper# X)
     (proper# s1 X -> proper# X, proper# dbl X -> dbl# proper X)
     (top# mark X -> proper# X, proper# quote X -> proper# X)
     (top# mark X -> proper# X, proper# quote X -> quote# proper X)
     (top# mark X -> proper# X, proper# sel1(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# sel1(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# s1 X -> proper# X)
     (top# mark X -> proper# X, proper# s1 X -> s1# proper X)
     (top# mark X -> proper# X, proper# dbl1 X -> proper# X)
     (top# mark X -> proper# X, proper# dbl1 X -> dbl1# proper X)
     (top# mark X -> proper# X, proper# from X -> proper# X)
     (top# mark X -> proper# X, proper# from X -> from# proper X)
     (top# mark X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# dbls X -> proper# X)
     (top# mark X -> proper# X, proper# dbls X -> dbls# proper X)
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# dbl X -> proper# X)
     (top# mark X -> proper# X, proper# dbl X -> dbl# proper X)
     (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# dbl1 s X -> s1# s1 dbl1 X, s1# ok X -> s1# X)
     (active# dbl1 s X -> s1# s1 dbl1 X, s1# mark X -> s1# X)
     (active# sel(X1, X2) -> sel#(active X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
     (active# sel(X1, X2) -> sel#(active X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
     (active# sel(X1, X2) -> sel#(active X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
     (active# sel1(X1, X2) -> sel1#(active X1, X2), sel1#(ok X1, ok X2) -> sel1#(X1, X2))
     (active# sel1(X1, X2) -> sel1#(active X1, X2), sel1#(mark X1, X2) -> sel1#(X1, X2))
     (active# sel1(X1, X2) -> sel1#(active X1, X2), sel1#(X1, mark X2) -> sel1#(X1, X2))
     (active# indx(cons(X, Y), Z) -> sel#(X, Z), sel#(ok X1, ok X2) -> sel#(X1, X2))
     (active# indx(cons(X, Y), Z) -> sel#(X, Z), sel#(mark X1, X2) -> sel#(X1, X2))
     (active# indx(cons(X, Y), Z) -> sel#(X, Z), sel#(X1, mark X2) -> sel#(X1, X2))
     (active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z), sel1#(ok X1, ok X2) -> sel1#(X1, X2))
     (active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z), sel1#(mark X1, X2) -> sel1#(X1, X2))
     (active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z), sel1#(X1, mark X2) -> sel1#(X1, X2))
     (active# indx(cons(X, Y), Z) -> indx#(Y, Z), indx#(mark X1, X2) -> indx#(X1, X2))
     (active# indx(cons(X, Y), Z) -> indx#(Y, Z), indx#(ok X1, ok X2) -> indx#(X1, X2))
     (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(X1, mark X2) -> sel#(X1, X2))
     (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(mark X1, X2) -> sel#(X1, X2))
     (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(ok X1, ok X2) -> sel#(X1, X2))
     (active# indx(X1, X2) -> indx#(active X1, X2), indx#(mark X1, X2) -> indx#(X1, X2))
     (active# indx(X1, X2) -> indx#(active X1, X2), indx#(ok X1, ok X2) -> indx#(X1, X2))
     (active# quote sel(X, Y) -> sel1#(X, Y), sel1#(X1, mark X2) -> sel1#(X1, X2))
     (active# quote sel(X, Y) -> sel1#(X, Y), sel1#(mark X1, X2) -> sel1#(X1, X2))
     (active# quote sel(X, Y) -> sel1#(X, Y), sel1#(ok X1, ok X2) -> sel1#(X1, X2))
     (active# dbl s X -> s# s dbl X, s# ok X -> s# X)
     (top# ok X -> active# X, active# dbl X -> active# X)
     (top# ok X -> active# X, active# dbl X -> dbl# active X)
     (top# ok X -> active# X, active# dbl s X -> dbl# X)
     (top# ok X -> active# X, active# dbl s X -> s# dbl X)
     (top# ok X -> active# X, active# dbl s X -> s# s dbl X)
     (top# ok X -> active# X, active# dbls X -> active# X)
     (top# ok X -> active# X, active# dbls X -> dbls# active X)
     (top# ok X -> active# X, active# dbls cons(X, Y) -> dbl# X)
     (top# ok X -> active# X, active# dbls cons(X, Y) -> dbls# Y)
     (top# ok X -> active# X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (top# ok X -> active# X, active# sel(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# sel(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
     (top# ok X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
     (top# ok X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (top# ok X -> active# X, active# indx(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# indx(X1, X2) -> indx#(active X1, X2))
     (top# ok X -> active# X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (top# ok X -> active# X, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (top# ok X -> active# X, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (top# ok X -> active# X, active# from X -> s# X)
     (top# ok X -> active# X, active# from X -> cons#(X, from s X))
     (top# ok X -> active# X, active# from X -> from# s X)
     (top# ok X -> active# X, active# dbl1 X -> active# X)
     (top# ok X -> active# X, active# dbl1 X -> dbl1# active X)
     (top# ok X -> active# X, active# dbl1 s X -> dbl1# X)
     (top# ok X -> active# X, active# dbl1 s X -> s1# dbl1 X)
     (top# ok X -> active# X, active# dbl1 s X -> s1# s1 dbl1 X)
     (top# ok X -> active# X, active# s1 X -> active# X)
     (top# ok X -> active# X, active# s1 X -> s1# active X)
     (top# ok X -> active# X, active# sel1(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# sel1(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (top# ok X -> active# X, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (top# ok X -> active# X, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (top# ok X -> active# X, active# quote X -> active# X)
     (top# ok X -> active# X, active# quote X -> quote# active X)
     (top# ok X -> active# X, active# quote dbl X -> dbl1# X)
     (top# ok X -> active# X, active# quote s X -> s1# quote X)
     (top# ok X -> active# X, active# quote s X -> quote# X)
     (top# ok X -> active# X, active# quote sel(X, Y) -> sel1#(X, Y))
     (proper# quote X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# quote X -> proper# X, proper# dbl X -> proper# X)
     (proper# quote X -> proper# X, proper# s X -> s# proper X)
     (proper# quote X -> proper# X, proper# s X -> proper# X)
     (proper# quote X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# quote X -> proper# X, proper# dbls X -> proper# X)
     (proper# quote X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# quote X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# quote X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# quote X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# quote X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# quote X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# quote X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# quote X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# quote X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# quote X -> proper# X, proper# from X -> from# proper X)
     (proper# quote X -> proper# X, proper# from X -> proper# X)
     (proper# quote X -> proper# X, proper# dbl1 X -> dbl1# proper X)
     (proper# quote X -> proper# X, proper# dbl1 X -> proper# X)
     (proper# quote X -> proper# X, proper# s1 X -> s1# proper X)
     (proper# quote X -> proper# X, proper# s1 X -> proper# X)
     (proper# quote X -> proper# X, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# quote X -> proper# X, proper# sel1(X1, X2) -> proper# X1)
     (proper# quote X -> proper# X, proper# sel1(X1, X2) -> proper# X2)
     (proper# quote X -> proper# X, proper# quote X -> quote# proper X)
     (proper# quote X -> proper# X, proper# quote X -> proper# X)
     (proper# dbl1 X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# dbl1 X -> proper# X, proper# dbl X -> proper# X)
     (proper# dbl1 X -> proper# X, proper# s X -> s# proper X)
     (proper# dbl1 X -> proper# X, proper# s X -> proper# X)
     (proper# dbl1 X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# dbl1 X -> proper# X, proper# dbls X -> proper# X)
     (proper# dbl1 X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# dbl1 X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# dbl1 X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# dbl1 X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# dbl1 X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# dbl1 X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# dbl1 X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# dbl1 X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# dbl1 X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# dbl1 X -> proper# X, proper# from X -> from# proper X)
     (proper# dbl1 X -> proper# X, proper# from X -> proper# X)
     (proper# dbl1 X -> proper# X, proper# dbl1 X -> dbl1# proper X)
     (proper# dbl1 X -> proper# X, proper# dbl1 X -> proper# X)
     (proper# dbl1 X -> proper# X, proper# s1 X -> s1# proper X)
     (proper# dbl1 X -> proper# X, proper# s1 X -> proper# X)
     (proper# dbl1 X -> proper# X, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# dbl1 X -> proper# X, proper# sel1(X1, X2) -> proper# X1)
     (proper# dbl1 X -> proper# X, proper# sel1(X1, X2) -> proper# X2)
     (proper# dbl1 X -> proper# X, proper# quote X -> quote# proper X)
     (proper# dbl1 X -> proper# X, proper# quote X -> proper# X)
     (proper# dbls X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# dbls X -> proper# X, proper# dbl X -> proper# X)
     (proper# dbls X -> proper# X, proper# s X -> s# proper X)
     (proper# dbls X -> proper# X, proper# s X -> proper# X)
     (proper# dbls X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# dbls X -> proper# X, proper# dbls X -> proper# X)
     (proper# dbls X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# dbls X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# dbls X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# dbls X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# dbls X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# dbls X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# dbls X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# dbls X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# dbls X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# dbls X -> proper# X, proper# from X -> from# proper X)
     (proper# dbls X -> proper# X, proper# from X -> proper# X)
     (proper# dbls X -> proper# X, proper# dbl1 X -> dbl1# proper X)
     (proper# dbls X -> proper# X, proper# dbl1 X -> proper# X)
     (proper# dbls X -> proper# X, proper# s1 X -> s1# proper X)
     (proper# dbls X -> proper# X, proper# s1 X -> proper# X)
     (proper# dbls X -> proper# X, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# dbls X -> proper# X, proper# sel1(X1, X2) -> proper# X1)
     (proper# dbls X -> proper# X, proper# sel1(X1, X2) -> proper# X2)
     (proper# dbls X -> proper# X, proper# quote X -> quote# proper X)
     (proper# dbls X -> proper# X, proper# quote X -> proper# X)
     (proper# dbl X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# dbl X -> proper# X, proper# dbl X -> proper# X)
     (proper# dbl X -> proper# X, proper# s X -> s# proper X)
     (proper# dbl X -> proper# X, proper# s X -> proper# X)
     (proper# dbl X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# dbl X -> proper# X, proper# dbls X -> proper# X)
     (proper# dbl X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# dbl X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# dbl X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# dbl X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# dbl X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# dbl X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# dbl X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# dbl X -> proper# X, proper# from X -> from# proper X)
     (proper# dbl X -> proper# X, proper# from X -> proper# X)
     (proper# dbl X -> proper# X, proper# dbl1 X -> dbl1# proper X)
     (proper# dbl X -> proper# X, proper# dbl1 X -> proper# X)
     (proper# dbl X -> proper# X, proper# s1 X -> s1# proper X)
     (proper# dbl X -> proper# X, proper# s1 X -> proper# X)
     (proper# dbl X -> proper# X, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# dbl X -> proper# X, proper# sel1(X1, X2) -> proper# X1)
     (proper# dbl X -> proper# X, proper# sel1(X1, X2) -> proper# X2)
     (proper# dbl X -> proper# X, proper# quote X -> quote# proper X)
     (proper# dbl X -> proper# X, proper# quote X -> proper# X)
     (quote# mark X -> quote# X, quote# mark X -> quote# X)
     (quote# mark X -> quote# X, quote# ok X -> quote# X)
     (s1# mark X -> s1# X, s1# mark X -> s1# X)
     (s1# mark X -> s1# X, s1# ok X -> s1# X)
     (dbl1# mark X -> dbl1# X, dbl1# mark X -> dbl1# X)
     (dbl1# mark X -> dbl1# X, dbl1# ok X -> dbl1# X)
     (dbls# ok X -> dbls# X, dbls# mark X -> dbls# X)
     (dbls# ok X -> dbls# X, dbls# ok X -> dbls# X)
     (s# ok X -> s# X, s# ok X -> s# X)
     (dbl# mark X -> dbl# X, dbl# mark X -> dbl# X)
     (dbl# mark X -> dbl# X, dbl# ok X -> dbl# X)
     (active# quote dbl X -> dbl1# X, dbl1# mark X -> dbl1# X)
     (active# quote dbl X -> dbl1# X, dbl1# ok X -> dbl1# X)
     (active# s1 X -> active# X, active# dbl X -> active# X)
     (active# s1 X -> active# X, active# dbl X -> dbl# active X)
     (active# s1 X -> active# X, active# dbl s X -> dbl# X)
     (active# s1 X -> active# X, active# dbl s X -> s# dbl X)
     (active# s1 X -> active# X, active# dbl s X -> s# s dbl X)
     (active# s1 X -> active# X, active# dbls X -> active# X)
     (active# s1 X -> active# X, active# dbls X -> dbls# active X)
     (active# s1 X -> active# X, active# dbls cons(X, Y) -> dbl# X)
     (active# s1 X -> active# X, active# dbls cons(X, Y) -> dbls# Y)
     (active# s1 X -> active# X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# s1 X -> active# X, active# sel(X1, X2) -> active# X1)
     (active# s1 X -> active# X, active# sel(X1, X2) -> active# X2)
     (active# s1 X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# s1 X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# s1 X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# s1 X -> active# X, active# indx(X1, X2) -> active# X1)
     (active# s1 X -> active# X, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# s1 X -> active# X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# s1 X -> active# X, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (active# s1 X -> active# X, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# s1 X -> active# X, active# from X -> s# X)
     (active# s1 X -> active# X, active# from X -> cons#(X, from s X))
     (active# s1 X -> active# X, active# from X -> from# s X)
     (active# s1 X -> active# X, active# dbl1 X -> active# X)
     (active# s1 X -> active# X, active# dbl1 X -> dbl1# active X)
     (active# s1 X -> active# X, active# dbl1 s X -> dbl1# X)
     (active# s1 X -> active# X, active# dbl1 s X -> s1# dbl1 X)
     (active# s1 X -> active# X, active# dbl1 s X -> s1# s1 dbl1 X)
     (active# s1 X -> active# X, active# s1 X -> active# X)
     (active# s1 X -> active# X, active# s1 X -> s1# active X)
     (active# s1 X -> active# X, active# sel1(X1, X2) -> active# X1)
     (active# s1 X -> active# X, active# sel1(X1, X2) -> active# X2)
     (active# s1 X -> active# X, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (active# s1 X -> active# X, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (active# s1 X -> active# X, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (active# s1 X -> active# X, active# quote X -> active# X)
     (active# s1 X -> active# X, active# quote X -> quote# active X)
     (active# s1 X -> active# X, active# quote dbl X -> dbl1# X)
     (active# s1 X -> active# X, active# quote s X -> s1# quote X)
     (active# s1 X -> active# X, active# quote s X -> quote# X)
     (active# s1 X -> active# X, active# quote sel(X, Y) -> sel1#(X, Y))
     (active# dbl1 X -> active# X, active# dbl X -> active# X)
     (active# dbl1 X -> active# X, active# dbl X -> dbl# active X)
     (active# dbl1 X -> active# X, active# dbl s X -> dbl# X)
     (active# dbl1 X -> active# X, active# dbl s X -> s# dbl X)
     (active# dbl1 X -> active# X, active# dbl s X -> s# s dbl X)
     (active# dbl1 X -> active# X, active# dbls X -> active# X)
     (active# dbl1 X -> active# X, active# dbls X -> dbls# active X)
     (active# dbl1 X -> active# X, active# dbls cons(X, Y) -> dbl# X)
     (active# dbl1 X -> active# X, active# dbls cons(X, Y) -> dbls# Y)
     (active# dbl1 X -> active# X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# dbl1 X -> active# X, active# sel(X1, X2) -> active# X1)
     (active# dbl1 X -> active# X, active# sel(X1, X2) -> active# X2)
     (active# dbl1 X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# dbl1 X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# dbl1 X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# dbl1 X -> active# X, active# indx(X1, X2) -> active# X1)
     (active# dbl1 X -> active# X, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# dbl1 X -> active# X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# dbl1 X -> active# X, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (active# dbl1 X -> active# X, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# dbl1 X -> active# X, active# from X -> s# X)
     (active# dbl1 X -> active# X, active# from X -> cons#(X, from s X))
     (active# dbl1 X -> active# X, active# from X -> from# s X)
     (active# dbl1 X -> active# X, active# dbl1 X -> active# X)
     (active# dbl1 X -> active# X, active# dbl1 X -> dbl1# active X)
     (active# dbl1 X -> active# X, active# dbl1 s X -> dbl1# X)
     (active# dbl1 X -> active# X, active# dbl1 s X -> s1# dbl1 X)
     (active# dbl1 X -> active# X, active# dbl1 s X -> s1# s1 dbl1 X)
     (active# dbl1 X -> active# X, active# s1 X -> active# X)
     (active# dbl1 X -> active# X, active# s1 X -> s1# active X)
     (active# dbl1 X -> active# X, active# sel1(X1, X2) -> active# X1)
     (active# dbl1 X -> active# X, active# sel1(X1, X2) -> active# X2)
     (active# dbl1 X -> active# X, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (active# dbl1 X -> active# X, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (active# dbl1 X -> active# X, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (active# dbl1 X -> active# X, active# quote X -> active# X)
     (active# dbl1 X -> active# X, active# quote X -> quote# active X)
     (active# dbl1 X -> active# X, active# quote dbl X -> dbl1# X)
     (active# dbl1 X -> active# X, active# quote s X -> s1# quote X)
     (active# dbl1 X -> active# X, active# quote s X -> quote# X)
     (active# dbl1 X -> active# X, active# quote sel(X, Y) -> sel1#(X, Y))
     (active# dbls cons(X, Y) -> dbl# X, dbl# mark X -> dbl# X)
     (active# dbls cons(X, Y) -> dbl# X, dbl# ok X -> dbl# X)
     (active# dbl s X -> dbl# X, dbl# mark X -> dbl# X)
     (active# dbl s X -> dbl# X, dbl# ok X -> dbl# X)
     (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (proper# indx(X1, X2) -> indx#(proper X1, proper X2), indx#(mark X1, X2) -> indx#(X1, X2))
     (proper# indx(X1, X2) -> indx#(proper X1, proper X2), indx#(ok X1, ok X2) -> indx#(X1, X2))
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# sel(X1, X2) -> sel#(X1, active X2), sel#(X1, mark X2) -> sel#(X1, X2))
     (active# sel(X1, X2) -> sel#(X1, active X2), sel#(mark X1, X2) -> sel#(X1, X2))
     (active# sel(X1, X2) -> sel#(X1, active X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
     (proper# sel1(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
     (proper# sel1(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# sel1(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X1, proper# dbls X -> dbls# proper X)
     (proper# sel1(X1, X2) -> proper# X1, proper# dbls X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# sel1(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# sel1(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# sel1(X1, X2) -> proper# X1, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# sel1(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X1)
     (proper# sel1(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X2)
     (proper# sel1(X1, X2) -> proper# X1, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# sel1(X1, X2) -> proper# X1, proper# indx(X1, X2) -> proper# X1)
     (proper# sel1(X1, X2) -> proper# X1, proper# indx(X1, X2) -> proper# X2)
     (proper# sel1(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# sel1(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X1, proper# dbl1 X -> dbl1# proper X)
     (proper# sel1(X1, X2) -> proper# X1, proper# dbl1 X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X1, proper# s1 X -> s1# proper X)
     (proper# sel1(X1, X2) -> proper# X1, proper# s1 X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# sel1(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> proper# X1)
     (proper# sel1(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> proper# X2)
     (proper# sel1(X1, X2) -> proper# X1, proper# quote X -> quote# proper X)
     (proper# sel1(X1, X2) -> proper# X1, proper# quote X -> proper# X)
     (proper# sel(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
     (proper# sel(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
     (proper# sel(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# sel(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# sel(X1, X2) -> proper# X1, proper# dbls X -> dbls# proper X)
     (proper# sel(X1, X2) -> proper# X1, proper# dbls X -> proper# X)
     (proper# sel(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# sel(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# sel(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# sel(X1, X2) -> proper# X1, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# sel(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X1)
     (proper# sel(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X2)
     (proper# sel(X1, X2) -> proper# X1, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# sel(X1, X2) -> proper# X1, proper# indx(X1, X2) -> proper# X1)
     (proper# sel(X1, X2) -> proper# X1, proper# indx(X1, X2) -> proper# X2)
     (proper# sel(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# sel(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# sel(X1, X2) -> proper# X1, proper# dbl1 X -> dbl1# proper X)
     (proper# sel(X1, X2) -> proper# X1, proper# dbl1 X -> proper# X)
     (proper# sel(X1, X2) -> proper# X1, proper# s1 X -> s1# proper X)
     (proper# sel(X1, X2) -> proper# X1, proper# s1 X -> proper# X)
     (proper# sel(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# sel(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> proper# X1)
     (proper# sel(X1, X2) -> proper# X1, proper# sel1(X1, X2) -> proper# X2)
     (proper# sel(X1, X2) -> proper# X1, proper# quote X -> quote# proper X)
     (proper# sel(X1, X2) -> proper# X1, proper# quote X -> proper# X)
     (active# sel1(X1, X2) -> active# X1, active# dbl X -> active# X)
     (active# sel1(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
     (active# sel1(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
     (active# sel1(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
     (active# sel1(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
     (active# sel1(X1, X2) -> active# X1, active# dbls X -> active# X)
     (active# sel1(X1, X2) -> active# X1, active# dbls X -> dbls# active X)
     (active# sel1(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbl# X)
     (active# sel1(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbls# Y)
     (active# sel1(X1, X2) -> active# X1, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# sel1(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
     (active# sel1(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X2)
     (active# sel1(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# sel1(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# sel1(X1, X2) -> active# X1, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# sel1(X1, X2) -> active# X1, active# indx(X1, X2) -> active# X1)
     (active# sel1(X1, X2) -> active# X1, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# sel1(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# sel1(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (active# sel1(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# sel1(X1, X2) -> active# X1, active# from X -> s# X)
     (active# sel1(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# sel1(X1, X2) -> active# X1, active# from X -> from# s X)
     (active# sel1(X1, X2) -> active# X1, active# dbl1 X -> active# X)
     (active# sel1(X1, X2) -> active# X1, active# dbl1 X -> dbl1# active X)
     (active# sel1(X1, X2) -> active# X1, active# dbl1 s X -> dbl1# X)
     (active# sel1(X1, X2) -> active# X1, active# dbl1 s X -> s1# dbl1 X)
     (active# sel1(X1, X2) -> active# X1, active# dbl1 s X -> s1# s1 dbl1 X)
     (active# sel1(X1, X2) -> active# X1, active# s1 X -> active# X)
     (active# sel1(X1, X2) -> active# X1, active# s1 X -> s1# active X)
     (active# sel1(X1, X2) -> active# X1, active# sel1(X1, X2) -> active# X1)
     (active# sel1(X1, X2) -> active# X1, active# sel1(X1, X2) -> active# X2)
     (active# sel1(X1, X2) -> active# X1, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (active# sel1(X1, X2) -> active# X1, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (active# sel1(X1, X2) -> active# X1, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (active# sel1(X1, X2) -> active# X1, active# quote X -> active# X)
     (active# sel1(X1, X2) -> active# X1, active# quote X -> quote# active X)
     (active# sel1(X1, X2) -> active# X1, active# quote dbl X -> dbl1# X)
     (active# sel1(X1, X2) -> active# X1, active# quote s X -> s1# quote X)
     (active# sel1(X1, X2) -> active# X1, active# quote s X -> quote# X)
     (active# sel1(X1, X2) -> active# X1, active# quote sel(X, Y) -> sel1#(X, Y))
     (active# sel(X1, X2) -> active# X1, active# dbl X -> active# X)
     (active# sel(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
     (active# sel(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
     (active# sel(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
     (active# sel(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
     (active# sel(X1, X2) -> active# X1, active# dbls X -> active# X)
     (active# sel(X1, X2) -> active# X1, active# dbls X -> dbls# active X)
     (active# sel(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbl# X)
     (active# sel(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbls# Y)
     (active# sel(X1, X2) -> active# X1, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
     (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X2)
     (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# sel(X1, X2) -> active# X1, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# sel(X1, X2) -> active# X1, active# indx(X1, X2) -> active# X1)
     (active# sel(X1, X2) -> active# X1, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# sel(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# sel(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (active# sel(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# sel(X1, X2) -> active# X1, active# from X -> s# X)
     (active# sel(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# sel(X1, X2) -> active# X1, active# from X -> from# s X)
     (active# sel(X1, X2) -> active# X1, active# dbl1 X -> active# X)
     (active# sel(X1, X2) -> active# X1, active# dbl1 X -> dbl1# active X)
     (active# sel(X1, X2) -> active# X1, active# dbl1 s X -> dbl1# X)
     (active# sel(X1, X2) -> active# X1, active# dbl1 s X -> s1# dbl1 X)
     (active# sel(X1, X2) -> active# X1, active# dbl1 s X -> s1# s1 dbl1 X)
     (active# sel(X1, X2) -> active# X1, active# s1 X -> active# X)
     (active# sel(X1, X2) -> active# X1, active# s1 X -> s1# active X)
     (active# sel(X1, X2) -> active# X1, active# sel1(X1, X2) -> active# X1)
     (active# sel(X1, X2) -> active# X1, active# sel1(X1, X2) -> active# X2)
     (active# sel(X1, X2) -> active# X1, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (active# sel(X1, X2) -> active# X1, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (active# sel(X1, X2) -> active# X1, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (active# sel(X1, X2) -> active# X1, active# quote X -> active# X)
     (active# sel(X1, X2) -> active# X1, active# quote X -> quote# active X)
     (active# sel(X1, X2) -> active# X1, active# quote dbl X -> dbl1# X)
     (active# sel(X1, X2) -> active# X1, active# quote s X -> s1# quote X)
     (active# sel(X1, X2) -> active# X1, active# quote s X -> quote# X)
     (active# sel(X1, X2) -> active# X1, active# quote sel(X, Y) -> sel1#(X, Y))
     (proper# sel1(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
     (proper# sel1(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# sel1(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X2, proper# dbls X -> dbls# proper X)
     (proper# sel1(X1, X2) -> proper# X2, proper# dbls X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# sel1(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# sel1(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# sel1(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# sel1(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
     (proper# sel1(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
     (proper# sel1(X1, X2) -> proper# X2, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# sel1(X1, X2) -> proper# X2, proper# indx(X1, X2) -> proper# X1)
     (proper# sel1(X1, X2) -> proper# X2, proper# indx(X1, X2) -> proper# X2)
     (proper# sel1(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# sel1(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X2, proper# dbl1 X -> dbl1# proper X)
     (proper# sel1(X1, X2) -> proper# X2, proper# dbl1 X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X2, proper# s1 X -> s1# proper X)
     (proper# sel1(X1, X2) -> proper# X2, proper# s1 X -> proper# X)
     (proper# sel1(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# sel1(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> proper# X1)
     (proper# sel1(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> proper# X2)
     (proper# sel1(X1, X2) -> proper# X2, proper# quote X -> quote# proper X)
     (proper# sel1(X1, X2) -> proper# X2, proper# quote X -> proper# X)
     (proper# sel(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
     (proper# sel(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
     (proper# sel(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# sel(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# sel(X1, X2) -> proper# X2, proper# dbls X -> dbls# proper X)
     (proper# sel(X1, X2) -> proper# X2, proper# dbls X -> proper# X)
     (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
     (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
     (proper# sel(X1, X2) -> proper# X2, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# sel(X1, X2) -> proper# X2, proper# indx(X1, X2) -> proper# X1)
     (proper# sel(X1, X2) -> proper# X2, proper# indx(X1, X2) -> proper# X2)
     (proper# sel(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# sel(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# sel(X1, X2) -> proper# X2, proper# dbl1 X -> dbl1# proper X)
     (proper# sel(X1, X2) -> proper# X2, proper# dbl1 X -> proper# X)
     (proper# sel(X1, X2) -> proper# X2, proper# s1 X -> s1# proper X)
     (proper# sel(X1, X2) -> proper# X2, proper# s1 X -> proper# X)
     (proper# sel(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> sel1#(proper X1, proper X2))
     (proper# sel(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> proper# X1)
     (proper# sel(X1, X2) -> proper# X2, proper# sel1(X1, X2) -> proper# X2)
     (proper# sel(X1, X2) -> proper# X2, proper# quote X -> quote# proper X)
     (proper# sel(X1, X2) -> proper# X2, proper# quote X -> proper# X)
     (active# sel1(X1, X2) -> active# X2, active# dbl X -> active# X)
     (active# sel1(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
     (active# sel1(X1, X2) -> active# X2, active# dbl s X -> dbl# X)
     (active# sel1(X1, X2) -> active# X2, active# dbl s X -> s# dbl X)
     (active# sel1(X1, X2) -> active# X2, active# dbl s X -> s# s dbl X)
     (active# sel1(X1, X2) -> active# X2, active# dbls X -> active# X)
     (active# sel1(X1, X2) -> active# X2, active# dbls X -> dbls# active X)
     (active# sel1(X1, X2) -> active# X2, active# dbls cons(X, Y) -> dbl# X)
     (active# sel1(X1, X2) -> active# X2, active# dbls cons(X, Y) -> dbls# Y)
     (active# sel1(X1, X2) -> active# X2, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# sel1(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X1)
     (active# sel1(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X2)
     (active# sel1(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# sel1(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# sel1(X1, X2) -> active# X2, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# sel1(X1, X2) -> active# X2, active# indx(X1, X2) -> active# X1)
     (active# sel1(X1, X2) -> active# X2, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# sel1(X1, X2) -> active# X2, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# sel1(X1, X2) -> active# X2, active# indx(cons(X, Y), Z) -> sel#(X, Z))
     (active# sel1(X1, X2) -> active# X2, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# sel1(X1, X2) -> active# X2, active# from X -> s# X)
     (active# sel1(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
     (active# sel1(X1, X2) -> active# X2, active# from X -> from# s X)
     (active# sel1(X1, X2) -> active# X2, active# dbl1 X -> active# X)
     (active# sel1(X1, X2) -> active# X2, active# dbl1 X -> dbl1# active X)
     (active# sel1(X1, X2) -> active# X2, active# dbl1 s X -> dbl1# X)
     (active# sel1(X1, X2) -> active# X2, active# dbl1 s X -> s1# dbl1 X)
     (active# sel1(X1, X2) -> active# X2, active# dbl1 s X -> s1# s1 dbl1 X)
     (active# sel1(X1, X2) -> active# X2, active# s1 X -> active# X)
     (active# sel1(X1, X2) -> active# X2, active# s1 X -> s1# active X)
     (active# sel1(X1, X2) -> active# X2, active# sel1(X1, X2) -> active# X1)
     (active# sel1(X1, X2) -> active# X2, active# sel1(X1, X2) -> active# X2)
     (active# sel1(X1, X2) -> active# X2, active# sel1(X1, X2) -> sel1#(X1, active X2))
     (active# sel1(X1, X2) -> active# X2, active# sel1(X1, X2) -> sel1#(active X1, X2))
     (active# sel1(X1, X2) -> active# X2, active# sel1(s X, cons(Y, Z)) -> sel1#(X, Z))
     (active# sel1(X1, X2) -> active# X2, active# quote X -> active# X)
     (active# sel1(X1, X2) -> active# X2, active# quote X -> quote# active X)
     (active# sel1(X1, X2) -> active# X2, active# quote dbl X -> dbl1# X)
     (active# sel1(X1, X2) -> active# X2, active# quote s X -> s1# quote X)
     (active# sel1(X1, X2) -> active# X2, active# quote s X -> quote# X)
     (active# sel1(X1, X2) -> active# X2, active# quote sel(X, Y) -> sel1#(X, Y))
     (sel1#(ok X1, ok X2) -> sel1#(X1, X2), sel1#(X1, mark X2) -> sel1#(X1, X2))
     (sel1#(ok X1, ok X2) -> sel1#(X1, X2), sel1#(mark X1, X2) -> sel1#(X1, X2))
     (sel1#(ok X1, ok X2) -> sel1#(X1, X2), sel1#(ok X1, ok X2) -> sel1#(X1, X2))
     (sel1#(X1, mark X2) -> sel1#(X1, X2), sel1#(X1, mark X2) -> sel1#(X1, X2))
     (sel1#(X1, mark X2) -> sel1#(X1, X2), sel1#(mark X1, X2) -> sel1#(X1, X2))
     (sel1#(X1, mark X2) -> sel1#(X1, X2), sel1#(ok X1, ok X2) -> sel1#(X1, X2))
     (indx#(mark X1, X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2))
     (indx#(mark X1, X2) -> indx#(X1, X2), indx#(ok X1, ok X2) -> indx#(X1, X2))
     (sel#(mark X1, X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
     (sel#(mark X1, X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
     (sel#(mark X1, X2) -> sel#(X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
     (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (proper# s1 X -> s1# proper X, s1# mark X -> s1# X)
     (proper# s1 X -> s1# proper X, s1# ok X -> s1# X)
     (proper# from X -> from# proper X, from# ok X -> from# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (active# quote s X -> s1# quote X, s1# mark X -> s1# X)
     (active# quote s X -> s1# quote X, s1# ok X -> s1# X)
     (active# s1 X -> s1# active X, s1# mark X -> s1# X)
     (active# s1 X -> s1# active X, s1# ok X -> s1# X)
     (active# dbl1 X -> dbl1# active X, dbl1# mark X -> dbl1# X)
     (active# dbl1 X -> dbl1# active X, dbl1# ok X -> dbl1# X)
     (active# dbls X -> dbls# active X, dbls# mark X -> dbls# X)
     (active# dbls X -> dbls# active X, dbls# ok X -> dbls# X)
     (active# dbl X -> dbl# active X, dbl# mark X -> dbl# X)
     (active# dbl X -> dbl# active X, dbl# ok X -> dbl# X)
    }
    STATUS:
     arrows: 0.881380
     SCCS (14):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {       active# dbl X -> active# X,
              active# dbls X -> active# X,
         active# sel(X1, X2) -> active# X1,
         active# sel(X1, X2) -> active# X2,
        active# indx(X1, X2) -> active# X1,
              active# dbl1 X -> active# X,
                active# s1 X -> active# X,
        active# sel1(X1, X2) -> active# X1,
        active# sel1(X1, X2) -> active# X2,
             active# quote X -> active# X}
      Scc:
       {       proper# dbl X -> proper# X,
                 proper# s X -> proper# X,
              proper# dbls X -> proper# X,
        proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
         proper# sel(X1, X2) -> proper# X1,
         proper# sel(X1, X2) -> proper# X2,
        proper# indx(X1, X2) -> proper# X1,
        proper# indx(X1, X2) -> proper# X2,
              proper# from X -> proper# X,
              proper# dbl1 X -> proper# X,
                proper# s1 X -> proper# X,
        proper# sel1(X1, X2) -> proper# X1,
        proper# sel1(X1, X2) -> proper# X2,
             proper# quote X -> proper# X}
      Scc:
       { sel1#(X1, mark X2) -> sel1#(X1, X2),
         sel1#(mark X1, X2) -> sel1#(X1, X2),
        sel1#(ok X1, ok X2) -> sel1#(X1, X2)}
      Scc:
       { indx#(mark X1, X2) -> indx#(X1, X2),
        indx#(ok X1, ok X2) -> indx#(X1, X2)}
      Scc:
       { sel#(X1, mark X2) -> sel#(X1, X2),
         sel#(mark X1, X2) -> sel#(X1, X2),
        sel#(ok X1, ok X2) -> sel#(X1, X2)}
      Scc:
       {cons#(ok X1, ok X2) -> cons#(X1, X2)}
      Scc:
       {quote# mark X -> quote# X,
          quote# ok X -> quote# X}
      Scc:
       {s1# mark X -> s1# X,
          s1# ok X -> s1# X}
      Scc:
       {dbl1# mark X -> dbl1# X,
          dbl1# ok X -> dbl1# X}
      Scc:
       {from# ok X -> from# X}
      Scc:
       {dbls# mark X -> dbls# X,
          dbls# ok X -> dbls# X}
      Scc:
       {s# ok X -> s# X}
      Scc:
       {dbl# mark X -> dbl# X,
          dbl# ok X -> dbl# X}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      SCC (10):
       Strict:
        {       active# dbl X -> active# X,
               active# dbls X -> active# X,
          active# sel(X1, X2) -> active# X1,
          active# sel(X1, X2) -> active# X2,
         active# indx(X1, X2) -> active# X1,
               active# dbl1 X -> active# X,
                 active# s1 X -> active# X,
         active# sel1(X1, X2) -> active# X1,
         active# sel1(X1, X2) -> active# X2,
              active# quote X -> active# X}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      SCC (15):
       Strict:
        {       proper# dbl X -> proper# X,
                  proper# s X -> proper# X,
               proper# dbls X -> proper# X,
         proper# cons(X1, X2) -> proper# X1,
         proper# cons(X1, X2) -> proper# X2,
          proper# sel(X1, X2) -> proper# X1,
          proper# sel(X1, X2) -> proper# X2,
         proper# indx(X1, X2) -> proper# X1,
         proper# indx(X1, X2) -> proper# X2,
               proper# from X -> proper# X,
               proper# dbl1 X -> proper# X,
                 proper# s1 X -> proper# X,
         proper# sel1(X1, X2) -> proper# X1,
         proper# sel1(X1, X2) -> proper# X2,
              proper# quote X -> proper# X}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        { sel1#(X1, mark X2) -> sel1#(X1, X2),
          sel1#(mark X1, X2) -> sel1#(X1, X2),
         sel1#(ok X1, ok X2) -> sel1#(X1, X2)}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        { indx#(mark X1, X2) -> indx#(X1, X2),
         indx#(ok X1, ok X2) -> indx#(X1, X2)}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        { sel#(X1, mark X2) -> sel#(X1, X2),
          sel#(mark X1, X2) -> sel#(X1, X2),
         sel#(ok X1, ok X2) -> sel#(X1, X2)}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {cons#(ok X1, ok X2) -> cons#(X1, X2)}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      
      
      
      
      
      
      
      
      SCC (2):
       Strict:
        {quote# mark X -> quote# X,
           quote# ok X -> quote# X}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      
      SCC (2):
       Strict:
        {s1# mark X -> s1# X,
           s1# ok X -> s1# X}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {dbl1# mark X -> dbl1# X,
           dbl1# ok X -> dbl1# X}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {from# ok X -> from# X}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {dbls# mark X -> dbls# X,
           dbls# ok X -> dbls# X}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {s# ok X -> s# X}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {dbl# mark X -> dbl# X,
           dbl# ok X -> dbl# X}
       Weak:
       {                active dbl X -> dbl active X,
                      active dbl 0() -> mark 0(),
                      active dbl s X -> mark s s dbl X,
                       active dbls X -> dbls active X,
                   active dbls nil() -> mark nil(),
              active dbls cons(X, Y) -> mark cons(dbl X, dbls Y),
                  active sel(X1, X2) -> sel(X1, active X2),
                  active sel(X1, X2) -> sel(active X1, X2),
         active sel(0(), cons(X, Y)) -> mark X,
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
                 active indx(X1, X2) -> indx(active X1, X2),
               active indx(nil(), X) -> mark nil(),
          active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)),
                       active from X -> mark cons(X, from s X),
                       active dbl1 X -> dbl1 active X,
                     active dbl1 0() -> mark 01(),
                     active dbl1 s X -> mark s1 s1 dbl1 X,
                         active s1 X -> s1 active X,
                 active sel1(X1, X2) -> sel1(X1, active X2),
                 active sel1(X1, X2) -> sel1(active X1, X2),
        active sel1(0(), cons(X, Y)) -> mark X,
        active sel1(s X, cons(Y, Z)) -> mark sel1(X, Z),
                      active quote X -> quote active X,
                    active quote 0() -> mark 01(),
                  active quote dbl X -> mark dbl1 X,
                    active quote s X -> mark s1 quote X,
              active quote sel(X, Y) -> mark sel1(X, Y),
                          dbl mark X -> mark dbl X,
                            dbl ok X -> ok dbl X,
                              s ok X -> ok s X,
                         dbls mark X -> mark dbls X,
                           dbls ok X -> ok dbls X,
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                    sel(X1, mark X2) -> mark sel(X1, X2),
                    sel(mark X1, X2) -> mark sel(X1, X2),
                   sel(ok X1, ok X2) -> ok sel(X1, X2),
                   indx(mark X1, X2) -> mark indx(X1, X2),
                  indx(ok X1, ok X2) -> ok indx(X1, X2),
                           from ok X -> ok from X,
                         dbl1 mark X -> mark dbl1 X,
                           dbl1 ok X -> ok dbl1 X,
                           s1 mark X -> mark s1 X,
                             s1 ok X -> ok s1 X,
                   sel1(X1, mark X2) -> mark sel1(X1, X2),
                   sel1(mark X1, X2) -> mark sel1(X1, X2),
                  sel1(ok X1, ok X2) -> ok sel1(X1, X2),
                        quote mark X -> mark quote X,
                          quote ok X -> ok quote X,
                          proper 0() -> ok 0(),
                        proper dbl X -> dbl proper X,
                          proper s X -> s proper X,
                        proper nil() -> ok nil(),
                       proper dbls X -> dbls proper X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper sel(X1, X2) -> sel(proper X1, proper X2),
                 proper indx(X1, X2) -> indx(proper X1, proper X2),
                       proper from X -> from proper X,
                         proper 01() -> ok 01(),
                       proper dbl1 X -> dbl1 proper X,
                         proper s1 X -> s1 proper X,
                 proper sel1(X1, X2) -> sel1(proper X1, proper X2),
                      proper quote X -> quote proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
       Open