MAYBE
Time: 1.096572
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),
                   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,
                   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,
                   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,
                     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,
                   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,
                     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),
                    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,
                    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,
                    top mark X -> top proper X,
                      top ok X -> top active X}
  EDG:
   {
    (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (active# dbl s X -> dbl# X, dbl# ok X -> dbl# X)
    (active# dbl s X -> dbl# X, dbl# mark X -> dbl# X)
    (active# dbls cons(X, Y) -> dbl# X, dbl# ok X -> dbl# X)
    (active# dbls cons(X, Y) -> dbl# X, dbl# mark X -> dbl# X)
    (dbl# mark X -> dbl# X, dbl# ok X -> dbl# X)
    (dbl# mark X -> dbl# X, dbl# mark X -> dbl# X)
    (s# ok X -> s# X, s# ok X -> s# X)
    (dbls# ok X -> dbls# X, dbls# ok X -> dbls# X)
    (dbls# ok X -> dbls# X, dbls# mark X -> dbls# X)
    (proper# dbl X -> proper# X, proper# from X -> proper# X)
    (proper# dbl X -> proper# X, proper# from X -> from# proper X)
    (proper# dbl X -> proper# X, proper# indx(X1, X2) -> proper# X2)
    (proper# dbl X -> proper# X, proper# indx(X1, X2) -> proper# X1)
    (proper# dbl X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
    (proper# dbl X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (proper# dbl X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# dbl X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# dbl X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# dbl X -> proper# X, proper# dbls X -> proper# X)
    (proper# dbl X -> proper# X, proper# dbls X -> dbls# proper X)
    (proper# dbl X -> proper# X, proper# s X -> proper# X)
    (proper# dbl X -> proper# X, proper# s X -> s# proper X)
    (proper# dbl X -> proper# X, proper# dbl X -> proper# X)
    (proper# dbl X -> proper# X, proper# dbl X -> dbl# proper X)
    (proper# dbls X -> proper# X, proper# from X -> proper# X)
    (proper# dbls X -> proper# X, proper# from X -> from# proper X)
    (proper# dbls X -> proper# X, proper# indx(X1, X2) -> proper# X2)
    (proper# dbls X -> proper# X, proper# indx(X1, X2) -> proper# X1)
    (proper# dbls X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
    (proper# dbls X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (proper# dbls X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# dbls X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# dbls X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# dbls X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# dbls X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# dbls X -> proper# X, proper# dbls X -> proper# X)
    (proper# dbls X -> proper# X, proper# dbls X -> dbls# proper X)
    (proper# dbls X -> proper# X, proper# s X -> proper# X)
    (proper# dbls X -> proper# X, proper# s X -> s# proper X)
    (proper# dbls X -> proper# X, proper# dbl X -> proper# X)
    (proper# dbls X -> proper# X, proper# dbl X -> dbl# 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# 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# sel(X1, X2) -> active# X1, active# from X -> from# 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 -> s# X)
    (active# sel(X1, X2) -> active# X1, active# indx(cons(X, Y), 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) -> cons#(sel(X, Z), indx(Y, Z)))
    (active# sel(X1, X2) -> active# X1, active# indx(X1, X2) -> indx#(active X1, X2))
    (active# sel(X1, X2) -> active# X1, active# indx(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X1, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, 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) -> active# X2)
    (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X1, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
    (active# sel(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbls# Y)
    (active# sel(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbl# X)
    (active# sel(X1, X2) -> active# X1, active# dbls X -> dbls# active X)
    (active# sel(X1, X2) -> active# X1, active# dbls X -> active# X)
    (active# sel(X1, X2) -> active# X1, active# dbl s X -> s# s 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 -> dbl# X)
    (active# sel(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
    (active# sel(X1, X2) -> active# X1, active# dbl X -> active# 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# 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# dbl s X -> s# dbl X, s# ok X -> s# X)
    (active# from X -> from# s X, from# ok X -> from# X)
    (proper# s X -> s# proper X, s# ok X -> s# X)
    (proper# from X -> from# proper X, from# ok X -> from# 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))
    (active# sel(X1, X2) -> sel#(X1, active X2), sel#(ok X1, ok 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#(X1, mark X2) -> sel#(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))
    (active# dbls cons(X, Y) -> dbls# Y, dbls# ok X -> dbls# X)
    (active# dbls cons(X, Y) -> dbls# Y, dbls# mark X -> dbls# 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# 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# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(ok X1, ok 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#(X1, mark X2) -> sel#(X1, X2))
    (active# indx(cons(X, Y), Z) -> indx#(Y, Z), indx#(ok X1, ok X2) -> indx#(X1, X2))
    (active# indx(cons(X, Y), Z) -> indx#(Y, Z), indx#(mark X1, X2) -> indx#(X1, X2))
    (active# indx(cons(X, Y), Z) -> sel#(X, Z), sel#(X1, mark 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#(ok X1, ok X2) -> sel#(X1, X2))
    (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (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)
    (active# sel(X1, X2) -> active# X2, active# dbl X -> active# X)
    (active# sel(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
    (active# sel(X1, X2) -> active# X2, active# dbl s X -> 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 -> s# s dbl X)
    (active# sel(X1, X2) -> active# X2, active# dbls X -> active# X)
    (active# sel(X1, X2) -> active# X2, active# dbls X -> dbls# active X)
    (active# sel(X1, X2) -> active# X2, active# dbls cons(X, Y) -> dbl# X)
    (active# sel(X1, X2) -> active# X2, active# dbls cons(X, Y) -> dbls# Y)
    (active# sel(X1, X2) -> active# X2, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# 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) -> sel#(active X1, X2))
    (active# sel(X1, X2) -> active# X2, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# sel(X1, X2) -> active# X2, active# indx(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X2, active# indx(X1, X2) -> indx#(active X1, X2))
    (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(cons(X, Y), Z) -> sel#(X, Z))
    (active# sel(X1, X2) -> active# X2, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
    (active# sel(X1, X2) -> active# X2, active# from X -> 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 -> from# s X)
    (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# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(ok X1, ok X2) -> cons#(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# dbls X -> dbls# proper X, dbls# mark X -> dbls# X)
    (proper# dbls X -> dbls# proper X, dbls# ok X -> dbls# X)
    (proper# dbl X -> dbl# proper X, dbl# mark X -> dbl# X)
    (proper# dbl X -> dbl# proper X, dbl# ok X -> dbl# 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)
    (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)
    (active# indx(X1, X2) -> active# X1, active# dbl X -> active# X)
    (active# indx(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
    (active# indx(X1, X2) -> active# X1, active# dbl s X -> 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 -> s# s dbl X)
    (active# indx(X1, X2) -> active# X1, active# dbls X -> active# X)
    (active# indx(X1, X2) -> active# X1, active# dbls X -> dbls# active X)
    (active# indx(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbl# X)
    (active# indx(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbls# Y)
    (active# indx(X1, X2) -> active# X1, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
    (active# indx(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
    (active# indx(X1, X2) -> active# X1, active# sel(X1, X2) -> active# 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) -> sel#(active X1, X2))
    (active# indx(X1, X2) -> active# X1, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# indx(X1, X2) -> active# X1, active# indx(X1, X2) -> active# X1)
    (active# indx(X1, X2) -> active# X1, active# indx(X1, X2) -> indx#(active X1, X2))
    (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(cons(X, Y), Z) -> sel#(X, Z))
    (active# indx(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
    (active# indx(X1, X2) -> active# X1, active# from X -> 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 -> from# s X)
    (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))
    (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)
    (proper# from X -> proper# X, proper# dbl X -> dbl# proper X)
    (proper# from X -> proper# X, proper# dbl X -> proper# X)
    (proper# from X -> proper# X, proper# s X -> s# proper X)
    (proper# from X -> proper# X, proper# s X -> proper# X)
    (proper# from X -> proper# X, proper# dbls X -> dbls# proper X)
    (proper# from X -> proper# X, proper# dbls X -> proper# X)
    (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# from X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# from X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# from X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (proper# from X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
    (proper# from X -> proper# X, proper# indx(X1, X2) -> proper# X1)
    (proper# from X -> proper# X, proper# indx(X1, X2) -> proper# X2)
    (proper# from X -> proper# X, proper# from X -> from# proper X)
    (proper# from X -> proper# X, proper# from X -> proper# X)
    (proper# s X -> proper# X, proper# dbl X -> dbl# proper X)
    (proper# s X -> proper# X, proper# dbl X -> proper# X)
    (proper# s X -> proper# X, proper# s X -> s# proper X)
    (proper# s X -> proper# X, proper# s X -> proper# X)
    (proper# s X -> proper# X, proper# dbls X -> dbls# proper X)
    (proper# s X -> proper# X, proper# dbls X -> proper# X)
    (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# indx(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# indx(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# from X -> from# proper X)
    (proper# s X -> proper# X, proper# from X -> proper# X)
    (from# ok X -> from# X, from# ok X -> from# X)
    (dbls# mark X -> dbls# X, dbls# mark X -> dbls# X)
    (dbls# mark X -> dbls# X, dbls# ok X -> dbls# X)
    (dbl# ok X -> dbl# X, dbl# mark X -> dbl# X)
    (dbl# ok X -> dbl# X, dbl# ok X -> dbl# X)
    (active# from X -> s# X, s# ok X -> s# X)
    (active# dbls X -> active# X, active# dbl X -> active# X)
    (active# dbls X -> active# X, active# dbl X -> dbl# active X)
    (active# dbls X -> active# X, active# dbl s X -> dbl# X)
    (active# dbls X -> active# X, active# dbl s X -> s# dbl X)
    (active# dbls X -> active# X, active# dbl s X -> s# s dbl X)
    (active# dbls X -> active# X, active# dbls X -> active# X)
    (active# dbls X -> active# X, active# dbls X -> dbls# active X)
    (active# dbls X -> active# X, active# dbls cons(X, Y) -> dbl# X)
    (active# dbls X -> active# X, active# dbls cons(X, Y) -> dbls# Y)
    (active# dbls X -> active# X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
    (active# dbls X -> active# X, active# sel(X1, X2) -> active# X1)
    (active# dbls X -> active# X, active# sel(X1, X2) -> active# X2)
    (active# dbls X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# dbls X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# dbls X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# dbls X -> active# X, active# indx(X1, X2) -> active# X1)
    (active# dbls X -> active# X, active# indx(X1, X2) -> indx#(active X1, X2))
    (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(cons(X, Y), Z) -> sel#(X, Z))
    (active# dbls X -> active# X, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
    (active# dbls X -> active# X, active# from X -> s# X)
    (active# dbls X -> active# X, active# from X -> cons#(X, from s X))
    (active# dbls X -> active# X, active# from X -> from# s X)
    (active# dbl X -> active# X, active# dbl X -> active# X)
    (active# dbl X -> active# X, active# dbl X -> dbl# active X)
    (active# dbl X -> active# X, active# dbl s X -> dbl# X)
    (active# dbl X -> active# X, active# dbl s X -> s# dbl X)
    (active# dbl X -> active# X, active# dbl s X -> s# s dbl X)
    (active# dbl X -> active# X, active# dbls X -> active# X)
    (active# dbl X -> active# X, active# dbls X -> dbls# active X)
    (active# dbl X -> active# X, active# dbls cons(X, Y) -> dbl# X)
    (active# dbl X -> active# X, active# dbls cons(X, Y) -> dbls# Y)
    (active# dbl X -> active# X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
    (active# dbl X -> active# X, active# sel(X1, X2) -> active# X1)
    (active# dbl X -> active# X, active# sel(X1, X2) -> active# X2)
    (active# dbl X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# dbl X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# dbl X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# dbl X -> active# X, active# indx(X1, X2) -> active# X1)
    (active# dbl X -> active# X, active# indx(X1, X2) -> indx#(active X1, X2))
    (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(cons(X, Y), Z) -> sel#(X, Z))
    (active# dbl X -> active# X, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
    (active# dbl X -> active# X, active# from X -> s# X)
    (active# dbl X -> active# X, active# from X -> cons#(X, from s X))
    (active# dbl X -> active# X, active# from X -> from# s X)
    (active# dbl s X -> s# s dbl X, s# ok X -> s# X)
   }
   EDG:
    {
     (active# dbl s X -> dbl# X, dbl# mark X -> dbl# X)
     (active# dbls cons(X, Y) -> dbl# X, dbl# ok X -> dbl# X)
     (active# dbls cons(X, Y) -> dbl# X, dbl# mark X -> dbl# X)
     (dbl# mark X -> dbl# X, dbl# ok X -> dbl# X)
     (dbl# mark X -> dbl# X, dbl# mark X -> dbl# X)
     (s# ok X -> s# X, s# ok X -> s# X)
     (dbls# ok X -> dbls# X, dbls# ok X -> dbls# X)
     (dbls# ok X -> dbls# X, dbls# mark X -> dbls# X)
     (proper# dbl X -> proper# X, proper# from X -> proper# X)
     (proper# dbl X -> proper# X, proper# from X -> from# proper X)
     (proper# dbl X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# dbl X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# dbl X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# dbl X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# dbl X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# dbl X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# dbl X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# dbl X -> proper# X, proper# dbls X -> proper# X)
     (proper# dbl X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# dbl X -> proper# X, proper# s X -> proper# X)
     (proper# dbl X -> proper# X, proper# s X -> s# proper X)
     (proper# dbl X -> proper# X, proper# dbl X -> proper# X)
     (proper# dbl X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# dbls X -> proper# X, proper# from X -> proper# X)
     (proper# dbls X -> proper# X, proper# from X -> from# proper X)
     (proper# dbls X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# dbls X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# dbls X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# dbls X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# dbls X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# dbls X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# dbls X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# dbls X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# dbls X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# dbls X -> proper# X, proper# dbls X -> proper# X)
     (proper# dbls X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# dbls X -> proper# X, proper# s X -> proper# X)
     (proper# dbls X -> proper# X, proper# s X -> s# proper X)
     (proper# dbls X -> proper# X, proper# dbl X -> proper# X)
     (proper# dbls X -> proper# X, proper# dbl X -> dbl# 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# 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) -> active# X1, active# from X -> from# 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 -> s# X)
     (active# sel(X1, X2) -> active# X1, active# indx(cons(X, Y), 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) -> cons#(sel(X, Z), indx(Y, Z)))
     (active# sel(X1, X2) -> active# X1, active# indx(X1, X2) -> indx#(active X1, X2))
     (active# sel(X1, X2) -> active# X1, active# indx(X1, X2) -> active# X1)
     (active# sel(X1, X2) -> active# X1, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, 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) -> active# X2)
     (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
     (active# sel(X1, X2) -> active# X1, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# sel(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbls# Y)
     (active# sel(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbl# X)
     (active# sel(X1, X2) -> active# X1, active# dbls X -> dbls# active X)
     (active# sel(X1, X2) -> active# X1, active# dbls X -> active# X)
     (active# sel(X1, X2) -> active# X1, active# dbl s X -> s# s 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 -> dbl# X)
     (active# sel(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
     (active# sel(X1, X2) -> active# X1, active# dbl X -> active# 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# 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# dbl s X -> s# dbl X, s# ok X -> s# X)
     (active# from X -> from# s X, from# ok X -> from# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (proper# from X -> from# proper X, from# ok X -> from# 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))
     (active# sel(X1, X2) -> sel#(X1, active X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
     (active# sel(X1, X2) -> sel#(X1, active X2), sel#(X1, mark X2) -> sel#(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))
     (active# dbls cons(X, Y) -> dbls# Y, dbls# ok X -> dbls# X)
     (active# dbls cons(X, Y) -> dbls# Y, dbls# mark X -> dbls# 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# 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# 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#(X1, mark X2) -> sel#(X1, X2))
     (active# indx(cons(X, Y), Z) -> indx#(Y, Z), indx#(ok X1, ok X2) -> indx#(X1, X2))
     (active# indx(cons(X, Y), Z) -> indx#(Y, Z), indx#(mark X1, X2) -> indx#(X1, X2))
     (active# indx(cons(X, Y), Z) -> sel#(X, Z), sel#(X1, mark 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#(ok X1, ok X2) -> sel#(X1, X2))
     (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (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)
     (active# sel(X1, X2) -> active# X2, active# dbl X -> active# X)
     (active# sel(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
     (active# sel(X1, X2) -> active# X2, active# dbl s X -> 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 -> s# s dbl X)
     (active# sel(X1, X2) -> active# X2, active# dbls X -> active# X)
     (active# sel(X1, X2) -> active# X2, active# dbls X -> dbls# active X)
     (active# sel(X1, X2) -> active# X2, active# dbls cons(X, Y) -> dbl# X)
     (active# sel(X1, X2) -> active# X2, active# dbls cons(X, Y) -> dbls# Y)
     (active# sel(X1, X2) -> active# X2, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X1)
     (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# 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) -> sel#(active X1, X2))
     (active# sel(X1, X2) -> active# X2, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# sel(X1, X2) -> active# X2, active# indx(X1, X2) -> active# X1)
     (active# sel(X1, X2) -> active# X2, active# indx(X1, X2) -> indx#(active X1, X2))
     (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(cons(X, Y), Z) -> sel#(X, Z))
     (active# sel(X1, X2) -> active# X2, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# sel(X1, X2) -> active# X2, active# from X -> 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 -> from# s X)
     (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# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(ok X1, ok X2) -> cons#(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# dbls X -> dbls# proper X, dbls# mark X -> dbls# X)
     (proper# dbls X -> dbls# proper X, dbls# ok X -> dbls# X)
     (proper# dbl X -> dbl# proper X, dbl# mark X -> dbl# X)
     (proper# dbl X -> dbl# proper X, dbl# ok X -> dbl# 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)
     (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)
     (active# indx(X1, X2) -> active# X1, active# dbl X -> active# X)
     (active# indx(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
     (active# indx(X1, X2) -> active# X1, active# dbl s X -> 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 -> s# s dbl X)
     (active# indx(X1, X2) -> active# X1, active# dbls X -> active# X)
     (active# indx(X1, X2) -> active# X1, active# dbls X -> dbls# active X)
     (active# indx(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbl# X)
     (active# indx(X1, X2) -> active# X1, active# dbls cons(X, Y) -> dbls# Y)
     (active# indx(X1, X2) -> active# X1, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# indx(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
     (active# indx(X1, X2) -> active# X1, active# sel(X1, X2) -> active# 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) -> sel#(active X1, X2))
     (active# indx(X1, X2) -> active# X1, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# indx(X1, X2) -> active# X1, active# indx(X1, X2) -> active# X1)
     (active# indx(X1, X2) -> active# X1, active# indx(X1, X2) -> indx#(active X1, X2))
     (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(cons(X, Y), Z) -> sel#(X, Z))
     (active# indx(X1, X2) -> active# X1, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# indx(X1, X2) -> active# X1, active# from X -> 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 -> from# s X)
     (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))
     (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)
     (proper# from X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# from X -> proper# X, proper# dbl X -> proper# X)
     (proper# from X -> proper# X, proper# s X -> s# proper X)
     (proper# from X -> proper# X, proper# s X -> proper# X)
     (proper# from X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# from X -> proper# X, proper# dbls X -> proper# X)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# from X -> from# proper X)
     (proper# from X -> proper# X, proper# from X -> proper# X)
     (proper# s X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# s X -> proper# X, proper# dbl X -> proper# X)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (proper# s X -> proper# X, proper# dbls X -> dbls# proper X)
     (proper# s X -> proper# X, proper# dbls X -> proper# X)
     (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# indx(X1, X2) -> indx#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# indx(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# indx(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# from X -> from# proper X)
     (proper# s X -> proper# X, proper# from X -> proper# X)
     (from# ok X -> from# X, from# ok X -> from# X)
     (dbls# mark X -> dbls# X, dbls# mark X -> dbls# X)
     (dbls# mark X -> dbls# X, dbls# ok X -> dbls# X)
     (dbl# ok X -> dbl# X, dbl# mark X -> dbl# X)
     (dbl# ok X -> dbl# X, dbl# ok X -> dbl# X)
     (active# dbls X -> active# X, active# dbl X -> active# X)
     (active# dbls X -> active# X, active# dbl X -> dbl# active X)
     (active# dbls X -> active# X, active# dbl s X -> dbl# X)
     (active# dbls X -> active# X, active# dbl s X -> s# dbl X)
     (active# dbls X -> active# X, active# dbl s X -> s# s dbl X)
     (active# dbls X -> active# X, active# dbls X -> active# X)
     (active# dbls X -> active# X, active# dbls X -> dbls# active X)
     (active# dbls X -> active# X, active# dbls cons(X, Y) -> dbl# X)
     (active# dbls X -> active# X, active# dbls cons(X, Y) -> dbls# Y)
     (active# dbls X -> active# X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# dbls X -> active# X, active# sel(X1, X2) -> active# X1)
     (active# dbls X -> active# X, active# sel(X1, X2) -> active# X2)
     (active# dbls X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# dbls X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# dbls X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# dbls X -> active# X, active# indx(X1, X2) -> active# X1)
     (active# dbls X -> active# X, active# indx(X1, X2) -> indx#(active X1, X2))
     (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(cons(X, Y), Z) -> sel#(X, Z))
     (active# dbls X -> active# X, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# dbls X -> active# X, active# from X -> s# X)
     (active# dbls X -> active# X, active# from X -> cons#(X, from s X))
     (active# dbls X -> active# X, active# from X -> from# s X)
     (active# dbl X -> active# X, active# dbl X -> active# X)
     (active# dbl X -> active# X, active# dbl X -> dbl# active X)
     (active# dbl X -> active# X, active# dbl s X -> dbl# X)
     (active# dbl X -> active# X, active# dbl s X -> s# dbl X)
     (active# dbl X -> active# X, active# dbl s X -> s# s dbl X)
     (active# dbl X -> active# X, active# dbls X -> active# X)
     (active# dbl X -> active# X, active# dbls X -> dbls# active X)
     (active# dbl X -> active# X, active# dbls cons(X, Y) -> dbl# X)
     (active# dbl X -> active# X, active# dbls cons(X, Y) -> dbls# Y)
     (active# dbl X -> active# X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y))
     (active# dbl X -> active# X, active# sel(X1, X2) -> active# X1)
     (active# dbl X -> active# X, active# sel(X1, X2) -> active# X2)
     (active# dbl X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
     (active# dbl X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
     (active# dbl X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
     (active# dbl X -> active# X, active# indx(X1, X2) -> active# X1)
     (active# dbl X -> active# X, active# indx(X1, X2) -> indx#(active X1, X2))
     (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(cons(X, Y), Z) -> sel#(X, Z))
     (active# dbl X -> active# X, active# indx(cons(X, Y), Z) -> indx#(Y, Z))
     (active# dbl X -> active# X, active# from X -> s# X)
     (active# dbl X -> active# X, active# from X -> cons#(X, from s X))
     (active# dbl X -> active# X, active# from X -> from# s X)
     (active# dbl s X -> s# s dbl X, s# ok X -> s# X)
    }
    STATUS:
     arrows: 0.873724
     SCCS (10):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# 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}
      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}
      Scc:
       {from# ok X -> from# X}
      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:
       {dbls# mark X -> dbls# X,
          dbls# ok X -> dbls# X}
      Scc:
       {dbl# mark X -> dbl# X,
          dbl# ok X -> dbl# X}
      Scc:
       {s# ok X -> s# 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),
                         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,
                         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,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open
      
      
      SCC (10):
       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}
       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),
                         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,
                         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,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open
      
      
      
      
      
      
      
      SCC (5):
       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}
       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),
                         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,
                         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,
                         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),
                         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,
                         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,
                         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),
                         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,
                         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,
                         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),
                         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,
                         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,
                         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),
                         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,
                         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,
                         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),
                         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,
                         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,
                         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),
                         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,
                         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,
                         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),
                         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,
                         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,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open