MAYBE

Problem:
 active(dbl(0())) -> mark(0())
 active(dbl(s(X))) -> mark(s(s(dbl(X))))
 active(dbls(nil())) -> mark(nil())
 active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
 active(sel(0(),cons(X,Y))) -> mark(X)
 active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
 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))))
 mark(dbl(X)) -> active(dbl(mark(X)))
 mark(0()) -> active(0())
 mark(s(X)) -> active(s(X))
 mark(dbls(X)) -> active(dbls(mark(X)))
 mark(nil()) -> active(nil())
 mark(cons(X1,X2)) -> active(cons(X1,X2))
 mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
 mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
 mark(from(X)) -> active(from(X))
 dbl(mark(X)) -> dbl(X)
 dbl(active(X)) -> dbl(X)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 dbls(mark(X)) -> dbls(X)
 dbls(active(X)) -> dbls(X)
 cons(mark(X1),X2) -> cons(X1,X2)
 cons(X1,mark(X2)) -> cons(X1,X2)
 cons(active(X1),X2) -> cons(X1,X2)
 cons(X1,active(X2)) -> cons(X1,X2)
 sel(mark(X1),X2) -> sel(X1,X2)
 sel(X1,mark(X2)) -> sel(X1,X2)
 sel(active(X1),X2) -> sel(X1,X2)
 sel(X1,active(X2)) -> sel(X1,X2)
 indx(mark(X1),X2) -> indx(X1,X2)
 indx(X1,mark(X2)) -> indx(X1,X2)
 indx(active(X1),X2) -> indx(X1,X2)
 indx(X1,active(X2)) -> indx(X1,X2)
 from(mark(X)) -> from(X)
 from(active(X)) -> from(X)

Proof:
 DP Processor:
  DPs:
   active#(dbl(0())) -> mark#(0())
   active#(dbl(s(X))) -> dbl#(X)
   active#(dbl(s(X))) -> s#(dbl(X))
   active#(dbl(s(X))) -> s#(s(dbl(X)))
   active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
   active#(dbls(nil())) -> mark#(nil())
   active#(dbls(cons(X,Y))) -> dbls#(Y)
   active#(dbls(cons(X,Y))) -> dbl#(X)
   active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
   active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
   active#(sel(0(),cons(X,Y))) -> mark#(X)
   active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
   active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
   active#(indx(nil(),X)) -> mark#(nil())
   active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
   active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
   active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
   active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
   active#(from(X)) -> s#(X)
   active#(from(X)) -> from#(s(X))
   active#(from(X)) -> cons#(X,from(s(X)))
   active#(from(X)) -> mark#(cons(X,from(s(X))))
   mark#(dbl(X)) -> mark#(X)
   mark#(dbl(X)) -> dbl#(mark(X))
   mark#(dbl(X)) -> active#(dbl(mark(X)))
   mark#(0()) -> active#(0())
   mark#(s(X)) -> active#(s(X))
   mark#(dbls(X)) -> mark#(X)
   mark#(dbls(X)) -> dbls#(mark(X))
   mark#(dbls(X)) -> active#(dbls(mark(X)))
   mark#(nil()) -> active#(nil())
   mark#(cons(X1,X2)) -> active#(cons(X1,X2))
   mark#(sel(X1,X2)) -> mark#(X2)
   mark#(sel(X1,X2)) -> mark#(X1)
   mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
   mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
   mark#(indx(X1,X2)) -> mark#(X1)
   mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
   mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
   mark#(from(X)) -> active#(from(X))
   dbl#(mark(X)) -> dbl#(X)
   dbl#(active(X)) -> dbl#(X)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   dbls#(mark(X)) -> dbls#(X)
   dbls#(active(X)) -> dbls#(X)
   cons#(mark(X1),X2) -> cons#(X1,X2)
   cons#(X1,mark(X2)) -> cons#(X1,X2)
   cons#(active(X1),X2) -> cons#(X1,X2)
   cons#(X1,active(X2)) -> cons#(X1,X2)
   sel#(mark(X1),X2) -> sel#(X1,X2)
   sel#(X1,mark(X2)) -> sel#(X1,X2)
   sel#(active(X1),X2) -> sel#(X1,X2)
   sel#(X1,active(X2)) -> sel#(X1,X2)
   indx#(mark(X1),X2) -> indx#(X1,X2)
   indx#(X1,mark(X2)) -> indx#(X1,X2)
   indx#(active(X1),X2) -> indx#(X1,X2)
   indx#(X1,active(X2)) -> indx#(X1,X2)
   from#(mark(X)) -> from#(X)
   from#(active(X)) -> from#(X)
  TRS:
   active(dbl(0())) -> mark(0())
   active(dbl(s(X))) -> mark(s(s(dbl(X))))
   active(dbls(nil())) -> mark(nil())
   active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
   active(sel(0(),cons(X,Y))) -> mark(X)
   active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
   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))))
   mark(dbl(X)) -> active(dbl(mark(X)))
   mark(0()) -> active(0())
   mark(s(X)) -> active(s(X))
   mark(dbls(X)) -> active(dbls(mark(X)))
   mark(nil()) -> active(nil())
   mark(cons(X1,X2)) -> active(cons(X1,X2))
   mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
   mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
   mark(from(X)) -> active(from(X))
   dbl(mark(X)) -> dbl(X)
   dbl(active(X)) -> dbl(X)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   dbls(mark(X)) -> dbls(X)
   dbls(active(X)) -> dbls(X)
   cons(mark(X1),X2) -> cons(X1,X2)
   cons(X1,mark(X2)) -> cons(X1,X2)
   cons(active(X1),X2) -> cons(X1,X2)
   cons(X1,active(X2)) -> cons(X1,X2)
   sel(mark(X1),X2) -> sel(X1,X2)
   sel(X1,mark(X2)) -> sel(X1,X2)
   sel(active(X1),X2) -> sel(X1,X2)
   sel(X1,active(X2)) -> sel(X1,X2)
   indx(mark(X1),X2) -> indx(X1,X2)
   indx(X1,mark(X2)) -> indx(X1,X2)
   indx(active(X1),X2) -> indx(X1,X2)
   indx(X1,active(X2)) -> indx(X1,X2)
   from(mark(X)) -> from(X)
   from(active(X)) -> from(X)
  TDG Processor:
   DPs:
    active#(dbl(0())) -> mark#(0())
    active#(dbl(s(X))) -> dbl#(X)
    active#(dbl(s(X))) -> s#(dbl(X))
    active#(dbl(s(X))) -> s#(s(dbl(X)))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
    active#(dbls(nil())) -> mark#(nil())
    active#(dbls(cons(X,Y))) -> dbls#(Y)
    active#(dbls(cons(X,Y))) -> dbl#(X)
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    active#(indx(nil(),X)) -> mark#(nil())
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
    active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
    active#(from(X)) -> s#(X)
    active#(from(X)) -> from#(s(X))
    active#(from(X)) -> cons#(X,from(s(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(dbl(X)) -> mark#(X)
    mark#(dbl(X)) -> dbl#(mark(X))
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    mark#(0()) -> active#(0())
    mark#(s(X)) -> active#(s(X))
    mark#(dbls(X)) -> mark#(X)
    mark#(dbls(X)) -> dbls#(mark(X))
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    mark#(nil()) -> active#(nil())
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(sel(X1,X2)) -> mark#(X2)
    mark#(sel(X1,X2)) -> mark#(X1)
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(indx(X1,X2)) -> mark#(X1)
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    mark#(from(X)) -> active#(from(X))
    dbl#(mark(X)) -> dbl#(X)
    dbl#(active(X)) -> dbl#(X)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    dbls#(mark(X)) -> dbls#(X)
    dbls#(active(X)) -> dbls#(X)
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2)
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(active(X1),X2) -> sel#(X1,X2)
    sel#(X1,active(X2)) -> sel#(X1,X2)
    indx#(mark(X1),X2) -> indx#(X1,X2)
    indx#(X1,mark(X2)) -> indx#(X1,X2)
    indx#(active(X1),X2) -> indx#(X1,X2)
    indx#(X1,active(X2)) -> indx#(X1,X2)
    from#(mark(X)) -> from#(X)
    from#(active(X)) -> from#(X)
   TRS:
    active(dbl(0())) -> mark(0())
    active(dbl(s(X))) -> mark(s(s(dbl(X))))
    active(dbls(nil())) -> mark(nil())
    active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
    active(sel(0(),cons(X,Y))) -> mark(X)
    active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
    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))))
    mark(dbl(X)) -> active(dbl(mark(X)))
    mark(0()) -> active(0())
    mark(s(X)) -> active(s(X))
    mark(dbls(X)) -> active(dbls(mark(X)))
    mark(nil()) -> active(nil())
    mark(cons(X1,X2)) -> active(cons(X1,X2))
    mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
    mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
    mark(from(X)) -> active(from(X))
    dbl(mark(X)) -> dbl(X)
    dbl(active(X)) -> dbl(X)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    dbls(mark(X)) -> dbls(X)
    dbls(active(X)) -> dbls(X)
    cons(mark(X1),X2) -> cons(X1,X2)
    cons(X1,mark(X2)) -> cons(X1,X2)
    cons(active(X1),X2) -> cons(X1,X2)
    cons(X1,active(X2)) -> cons(X1,X2)
    sel(mark(X1),X2) -> sel(X1,X2)
    sel(X1,mark(X2)) -> sel(X1,X2)
    sel(active(X1),X2) -> sel(X1,X2)
    sel(X1,active(X2)) -> sel(X1,X2)
    indx(mark(X1),X2) -> indx(X1,X2)
    indx(X1,mark(X2)) -> indx(X1,X2)
    indx(active(X1),X2) -> indx(X1,X2)
    indx(X1,active(X2)) -> indx(X1,X2)
    from(mark(X)) -> from(X)
    from(active(X)) -> from(X)
   graph:
    from#(mark(X)) -> from#(X) -> from#(active(X)) -> from#(X)
    from#(mark(X)) -> from#(X) -> from#(mark(X)) -> from#(X)
    from#(active(X)) -> from#(X) -> from#(active(X)) -> from#(X)
    from#(active(X)) -> from#(X) -> from#(mark(X)) -> from#(X)
    indx#(mark(X1),X2) -> indx#(X1,X2) ->
    indx#(X1,active(X2)) -> indx#(X1,X2)
    indx#(mark(X1),X2) -> indx#(X1,X2) ->
    indx#(active(X1),X2) -> indx#(X1,X2)
    indx#(mark(X1),X2) -> indx#(X1,X2) ->
    indx#(X1,mark(X2)) -> indx#(X1,X2)
    indx#(mark(X1),X2) -> indx#(X1,X2) ->
    indx#(mark(X1),X2) -> indx#(X1,X2)
    indx#(active(X1),X2) -> indx#(X1,X2) ->
    indx#(X1,active(X2)) -> indx#(X1,X2)
    indx#(active(X1),X2) -> indx#(X1,X2) ->
    indx#(active(X1),X2) -> indx#(X1,X2)
    indx#(active(X1),X2) -> indx#(X1,X2) ->
    indx#(X1,mark(X2)) -> indx#(X1,X2)
    indx#(active(X1),X2) -> indx#(X1,X2) ->
    indx#(mark(X1),X2) -> indx#(X1,X2)
    indx#(X1,mark(X2)) -> indx#(X1,X2) ->
    indx#(X1,active(X2)) -> indx#(X1,X2)
    indx#(X1,mark(X2)) -> indx#(X1,X2) ->
    indx#(active(X1),X2) -> indx#(X1,X2)
    indx#(X1,mark(X2)) -> indx#(X1,X2) ->
    indx#(X1,mark(X2)) -> indx#(X1,X2)
    indx#(X1,mark(X2)) -> indx#(X1,X2) ->
    indx#(mark(X1),X2) -> indx#(X1,X2)
    indx#(X1,active(X2)) -> indx#(X1,X2) ->
    indx#(X1,active(X2)) -> indx#(X1,X2)
    indx#(X1,active(X2)) -> indx#(X1,X2) ->
    indx#(active(X1),X2) -> indx#(X1,X2)
    indx#(X1,active(X2)) -> indx#(X1,X2) ->
    indx#(X1,mark(X2)) -> indx#(X1,X2)
    indx#(X1,active(X2)) -> indx#(X1,X2) ->
    indx#(mark(X1),X2) -> indx#(X1,X2)
    sel#(mark(X1),X2) -> sel#(X1,X2) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    sel#(mark(X1),X2) -> sel#(X1,X2) ->
    sel#(active(X1),X2) -> sel#(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#(active(X1),X2) -> sel#(X1,X2) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    sel#(active(X1),X2) -> sel#(X1,X2) ->
    sel#(active(X1),X2) -> sel#(X1,X2)
    sel#(active(X1),X2) -> sel#(X1,X2) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(active(X1),X2) -> sel#(X1,X2) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(active(X1),X2) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(X1,active(X2)) -> sel#(X1,X2) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    sel#(X1,active(X2)) -> sel#(X1,X2) ->
    sel#(active(X1),X2) -> sel#(X1,X2)
    sel#(X1,active(X2)) -> sel#(X1,X2) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(X1,active(X2)) -> sel#(X1,X2) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    dbls#(mark(X)) -> dbls#(X) -> dbls#(active(X)) -> dbls#(X)
    dbls#(mark(X)) -> dbls#(X) -> dbls#(mark(X)) -> dbls#(X)
    dbls#(active(X)) -> dbls#(X) -> dbls#(active(X)) -> dbls#(X)
    dbls#(active(X)) -> dbls#(X) -> dbls#(mark(X)) -> dbls#(X)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    dbl#(mark(X)) -> dbl#(X) -> dbl#(active(X)) -> dbl#(X)
    dbl#(mark(X)) -> dbl#(X) -> dbl#(mark(X)) -> dbl#(X)
    dbl#(active(X)) -> dbl#(X) -> dbl#(active(X)) -> dbl#(X)
    dbl#(active(X)) -> dbl#(X) -> dbl#(mark(X)) -> dbl#(X)
    mark#(from(X)) -> active#(from(X)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(from(X)) -> active#(from(X)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(from(X)) -> active#(from(X)) ->
    active#(from(X)) -> from#(s(X))
    mark#(from(X)) -> active#(from(X)) ->
    active#(from(X)) -> s#(X)
    mark#(from(X)) -> active#(from(X)) ->
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
    mark#(from(X)) -> active#(from(X)) ->
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
    mark#(from(X)) -> active#(from(X)) ->
    active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
    mark#(from(X)) -> active#(from(X)) ->
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
    mark#(from(X)) -> active#(from(X)) ->
    active#(indx(nil(),X)) -> mark#(nil())
    mark#(from(X)) -> active#(from(X)) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(from(X)) -> active#(from(X)) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(from(X)) -> active#(from(X)) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(from(X)) -> active#(from(X)) ->
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
    mark#(from(X)) -> active#(from(X)) ->
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
    mark#(from(X)) -> active#(from(X)) ->
    active#(dbls(cons(X,Y))) -> dbl#(X)
    mark#(from(X)) -> active#(from(X)) ->
    active#(dbls(cons(X,Y))) -> dbls#(Y)
    mark#(from(X)) -> active#(from(X)) ->
    active#(dbls(nil())) -> mark#(nil())
    mark#(from(X)) -> active#(from(X)) ->
    active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
    mark#(from(X)) -> active#(from(X)) ->
    active#(dbl(s(X))) -> s#(s(dbl(X)))
    mark#(from(X)) -> active#(from(X)) ->
    active#(dbl(s(X))) -> s#(dbl(X))
    mark#(from(X)) -> active#(from(X)) ->
    active#(dbl(s(X))) -> dbl#(X)
    mark#(from(X)) -> active#(from(X)) ->
    active#(dbl(0())) -> mark#(0())
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2) ->
    indx#(X1,active(X2)) -> indx#(X1,X2)
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2) ->
    indx#(active(X1),X2) -> indx#(X1,X2)
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2) ->
    indx#(X1,mark(X2)) -> indx#(X1,X2)
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2) ->
    indx#(mark(X1),X2) -> indx#(X1,X2)
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> active#(from(X))
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(indx(X1,X2)) -> mark#(X1)
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(nil()) -> active#(nil())
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    mark#(indx(X1,X2)) -> mark#(X1) -> mark#(dbls(X)) -> mark#(X)
    mark#(indx(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
    mark#(indx(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(dbl(X)) -> dbl#(mark(X))
    mark#(indx(X1,X2)) -> mark#(X1) ->
    mark#(dbl(X)) -> mark#(X)
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(from(X)) -> from#(s(X))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(from(X)) -> s#(X)
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(indx(nil(),X)) -> mark#(nil())
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(dbls(cons(X,Y))) -> dbl#(X)
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(dbls(cons(X,Y))) -> dbls#(Y)
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(dbls(nil())) -> mark#(nil())
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(dbl(s(X))) -> s#(s(dbl(X)))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(dbl(s(X))) -> s#(dbl(X))
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(dbl(s(X))) -> dbl#(X)
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
    active#(dbl(0())) -> mark#(0())
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2)) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2)) ->
    sel#(active(X1),X2) -> sel#(X1,X2)
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2)) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2)) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(from(X)) -> active#(from(X))
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(indx(X1,X2)) -> mark#(X1)
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X1)
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X2)
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(nil()) -> active#(nil())
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbls(X)) -> mark#(X)
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(X))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbl(X)) -> dbl#(mark(X))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbl(X)) -> mark#(X)
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> active#(from(X))
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(indx(X1,X2)) -> mark#(X1)
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X1)
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X2)
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil())
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(dbls(X)) -> mark#(X)
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(dbl(X)) -> dbl#(mark(X))
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(dbl(X)) -> mark#(X)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(from(X)) -> from#(s(X))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(from(X)) -> s#(X)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(indx(nil(),X)) -> mark#(nil())
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(dbls(cons(X,Y))) -> dbl#(X)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(dbls(cons(X,Y))) -> dbls#(Y)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(dbls(nil())) -> mark#(nil())
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(dbl(s(X))) -> s#(s(dbl(X)))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(dbl(s(X))) -> s#(dbl(X))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(dbl(s(X))) -> dbl#(X)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(dbl(0())) -> mark#(0())
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(from(X)) -> from#(s(X))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(from(X)) -> s#(X)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(indx(nil(),X)) -> mark#(nil())
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(dbls(cons(X,Y))) -> dbl#(X)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(dbls(cons(X,Y))) -> dbls#(Y)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(dbls(nil())) -> mark#(nil())
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(dbl(s(X))) -> s#(s(dbl(X)))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(dbl(s(X))) -> s#(dbl(X))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(dbl(s(X))) -> dbl#(X)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(dbl(0())) -> mark#(0())
    mark#(dbls(X)) -> dbls#(mark(X)) ->
    dbls#(active(X)) -> dbls#(X)
    mark#(dbls(X)) -> dbls#(mark(X)) -> dbls#(mark(X)) -> dbls#(X)
    mark#(dbls(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(X))
    mark#(dbls(X)) -> mark#(X) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    mark#(dbls(X)) -> mark#(X) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    mark#(dbls(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> mark#(X1)
    mark#(dbls(X)) -> mark#(X) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(dbls(X)) -> mark#(X) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(dbls(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1)
    mark#(dbls(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2)
    mark#(dbls(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(dbls(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(dbls(X)) -> mark#(X) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    mark#(dbls(X)) -> mark#(X) -> mark#(dbls(X)) -> dbls#(mark(X))
    mark#(dbls(X)) -> mark#(X) -> mark#(dbls(X)) -> mark#(X)
    mark#(dbls(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
    mark#(dbls(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(dbls(X)) -> mark#(X) -> mark#(dbl(X)) -> active#(dbl(mark(X)))
    mark#(dbls(X)) -> mark#(X) -> mark#(dbl(X)) -> dbl#(mark(X))
    mark#(dbls(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(from(X)) -> from#(s(X))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(from(X)) -> s#(X)
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(indx(nil(),X)) -> mark#(nil())
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(dbls(cons(X,Y))) -> dbl#(X)
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(dbls(cons(X,Y))) -> dbls#(Y)
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(dbls(nil())) -> mark#(nil())
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(dbl(s(X))) -> s#(s(dbl(X)))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(dbl(s(X))) -> s#(dbl(X))
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(dbl(s(X))) -> dbl#(X)
    mark#(dbls(X)) -> active#(dbls(mark(X))) ->
    active#(dbl(0())) -> mark#(0())
    mark#(nil()) -> active#(nil()) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(nil()) -> active#(nil()) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(nil()) -> active#(nil()) -> active#(from(X)) -> from#(s(X))
    mark#(nil()) -> active#(nil()) -> active#(from(X)) -> s#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
    mark#(nil()) -> active#(nil()) ->
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
    mark#(nil()) -> active#(nil()) ->
    active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
    mark#(nil()) -> active#(nil()) ->
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
    mark#(nil()) -> active#(nil()) ->
    active#(indx(nil(),X)) -> mark#(nil())
    mark#(nil()) -> active#(nil()) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(nil()) -> active#(nil()) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(nil()) -> active#(nil()) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
    mark#(nil()) -> active#(nil()) ->
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
    mark#(nil()) -> active#(nil()) ->
    active#(dbls(cons(X,Y))) -> dbl#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(dbls(cons(X,Y))) -> dbls#(Y)
    mark#(nil()) -> active#(nil()) ->
    active#(dbls(nil())) -> mark#(nil())
    mark#(nil()) -> active#(nil()) ->
    active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
    mark#(nil()) -> active#(nil()) ->
    active#(dbl(s(X))) -> s#(s(dbl(X)))
    mark#(nil()) -> active#(nil()) ->
    active#(dbl(s(X))) -> s#(dbl(X))
    mark#(nil()) -> active#(nil()) -> active#(dbl(s(X))) -> dbl#(X)
    mark#(nil()) -> active#(nil()) -> active#(dbl(0())) -> mark#(0())
    mark#(s(X)) -> active#(s(X)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(s(X)) -> active#(s(X)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(s(X)) -> active#(s(X)) -> active#(from(X)) -> from#(s(X))
    mark#(s(X)) -> active#(s(X)) -> active#(from(X)) -> s#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
    mark#(s(X)) -> active#(s(X)) ->
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
    mark#(s(X)) -> active#(s(X)) ->
    active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
    mark#(s(X)) -> active#(s(X)) ->
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
    mark#(s(X)) -> active#(s(X)) ->
    active#(indx(nil(),X)) -> mark#(nil())
    mark#(s(X)) -> active#(s(X)) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(s(X)) -> active#(s(X)) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(s(X)) -> active#(s(X)) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
    mark#(s(X)) -> active#(s(X)) ->
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
    mark#(s(X)) -> active#(s(X)) -> active#(dbls(cons(X,Y))) -> dbl#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(dbls(cons(X,Y))) -> dbls#(Y)
    mark#(s(X)) -> active#(s(X)) ->
    active#(dbls(nil())) -> mark#(nil())
    mark#(s(X)) -> active#(s(X)) ->
    active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
    mark#(s(X)) -> active#(s(X)) -> active#(dbl(s(X))) -> s#(s(dbl(X)))
    mark#(s(X)) -> active#(s(X)) -> active#(dbl(s(X))) -> s#(dbl(X))
    mark#(s(X)) -> active#(s(X)) -> active#(dbl(s(X))) -> dbl#(X)
    mark#(s(X)) -> active#(s(X)) -> active#(dbl(0())) -> mark#(0())
    mark#(dbl(X)) -> dbl#(mark(X)) -> dbl#(active(X)) -> dbl#(X)
    mark#(dbl(X)) -> dbl#(mark(X)) -> dbl#(mark(X)) -> dbl#(X)
    mark#(dbl(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(X))
    mark#(dbl(X)) -> mark#(X) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    mark#(dbl(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    mark#(dbl(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> mark#(X1)
    mark#(dbl(X)) -> mark#(X) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(dbl(X)) -> mark#(X) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(dbl(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1)
    mark#(dbl(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2)
    mark#(dbl(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(dbl(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(dbl(X)) -> mark#(X) -> mark#(dbls(X)) -> active#(dbls(mark(X)))
    mark#(dbl(X)) -> mark#(X) -> mark#(dbls(X)) -> dbls#(mark(X))
    mark#(dbl(X)) -> mark#(X) -> mark#(dbls(X)) -> mark#(X)
    mark#(dbl(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
    mark#(dbl(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> active#(dbl(mark(X)))
    mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> dbl#(mark(X))
    mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(from(X)) -> from#(s(X))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(from(X)) -> s#(X)
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(indx(nil(),X)) -> mark#(nil())
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(dbls(cons(X,Y))) -> dbl#(X)
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(dbls(cons(X,Y))) -> dbls#(Y)
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(dbls(nil())) -> mark#(nil())
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(dbl(s(X))) -> s#(s(dbl(X)))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(dbl(s(X))) -> s#(dbl(X))
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(dbl(s(X))) -> dbl#(X)
    mark#(dbl(X)) -> active#(dbl(mark(X))) ->
    active#(dbl(0())) -> mark#(0())
    mark#(0()) -> active#(0()) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(0()) -> active#(0()) -> active#(from(X)) -> cons#(X,from(s(X)))
    mark#(0()) -> active#(0()) -> active#(from(X)) -> from#(s(X))
    mark#(0()) -> active#(0()) -> active#(from(X)) -> s#(X)
    mark#(0()) -> active#(0()) ->
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
    mark#(0()) -> active#(0()) ->
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z))
    mark#(0()) -> active#(0()) -> active#(indx(cons(X,Y),Z)) -> sel#(X,Z)
    mark#(0()) -> active#(0()) ->
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z)
    mark#(0()) -> active#(0()) -> active#(indx(nil(),X)) -> mark#(nil())
    mark#(0()) -> active#(0()) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(0()) -> active#(0()) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(0()) -> active#(0()) -> active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(0()) -> active#(0()) ->
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
    mark#(0()) -> active#(0()) ->
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y))
    mark#(0()) -> active#(0()) -> active#(dbls(cons(X,Y))) -> dbl#(X)
    mark#(0()) -> active#(0()) -> active#(dbls(cons(X,Y))) -> dbls#(Y)
    mark#(0()) -> active#(0()) -> active#(dbls(nil())) -> mark#(nil())
    mark#(0()) -> active#(0()) ->
    active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
    mark#(0()) -> active#(0()) -> active#(dbl(s(X))) -> s#(s(dbl(X)))
    mark#(0()) -> active#(0()) -> active#(dbl(s(X))) -> s#(dbl(X))
    mark#(0()) -> active#(0()) -> active#(dbl(s(X))) -> dbl#(X)
    mark#(0()) -> active#(0()) -> active#(dbl(0())) -> mark#(0())
    active#(from(X)) -> from#(s(X)) -> from#(active(X)) -> from#(X)
    active#(from(X)) -> from#(s(X)) ->
    from#(mark(X)) -> from#(X)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(from(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    active#(from(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(from(X)) -> active#(from(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(indx(X1,X2)) -> mark#(X1)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(nil()) -> active#(nil())
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(dbls(X)) -> mark#(X)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(s(X)) -> active#(s(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(0()) -> active#(0())
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(dbl(X)) -> dbl#(mark(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(dbl(X)) -> mark#(X)
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z) ->
    indx#(X1,active(X2)) -> indx#(X1,X2)
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z) ->
    indx#(active(X1),X2) -> indx#(X1,X2)
    active#(indx(cons(X,Y),Z)) -> indx#(Y,Z) ->
    indx#(X1,mark(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,active(X2)) -> sel#(X1,X2)
    active#(indx(cons(X,Y),Z)) -> sel#(X,Z) ->
    sel#(active(X1),X2) -> sel#(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)) -> cons#(sel(X,Z),indx(Y,Z)) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z)) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z)) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(from(X)) -> active#(from(X))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(indx(X1,X2)) -> mark#(X1)
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(nil()) -> active#(nil())
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(dbls(X)) -> mark#(X)
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(s(X)) -> active#(s(X))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(0()) -> active#(0())
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(dbl(X)) -> dbl#(mark(X))
    active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
    mark#(dbl(X)) -> mark#(X)
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(from(X)) -> active#(from(X))
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(indx(X1,X2)) -> mark#(X1)
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(nil()) -> active#(nil())
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(dbls(X)) -> mark#(X)
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(s(X)) -> active#(s(X))
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(0()) -> active#(0())
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(dbl(X)) -> dbl#(mark(X))
    active#(indx(nil(),X)) -> mark#(nil()) ->
    mark#(dbl(X)) -> mark#(X)
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z) ->
    sel#(active(X1),X2) -> sel#(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))) -> mark#(sel(X,Z)) ->
    mark#(from(X)) -> active#(from(X))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(indx(X1,X2)) -> mark#(X1)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(nil()) -> active#(nil())
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(dbls(X)) -> mark#(X)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(s(X)) -> active#(s(X))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(0()) -> active#(0())
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(dbl(X)) -> dbl#(mark(X))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(dbl(X)) -> mark#(X)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(from(X)) -> active#(from(X))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(indx(X1,X2)) -> mark#(X1)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(nil()) -> active#(nil())
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(dbls(X)) -> mark#(X)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(s(X)) -> active#(s(X))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(0()) -> active#(0())
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(dbl(X)) -> dbl#(mark(X))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(dbl(X)) -> mark#(X)
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y)) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y)) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y)) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(dbls(cons(X,Y))) -> dbls#(Y) ->
    dbls#(active(X)) -> dbls#(X)
    active#(dbls(cons(X,Y))) -> dbls#(Y) ->
    dbls#(mark(X)) -> dbls#(X)
    active#(dbls(cons(X,Y))) -> dbl#(X) ->
    dbl#(active(X)) -> dbl#(X)
    active#(dbls(cons(X,Y))) -> dbl#(X) ->
    dbl#(mark(X)) -> dbl#(X)
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(from(X)) -> active#(from(X))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(indx(X1,X2)) -> mark#(X1)
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(nil()) -> active#(nil())
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(dbls(X)) -> mark#(X)
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(s(X)) -> active#(s(X))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(0()) -> active#(0())
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(dbl(X)) -> dbl#(mark(X))
    active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
    mark#(dbl(X)) -> mark#(X)
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(from(X)) -> active#(from(X))
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(indx(X1,X2)) -> mark#(X1)
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(nil()) -> active#(nil())
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(dbls(X)) -> mark#(X)
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(s(X)) -> active#(s(X))
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(0()) -> active#(0())
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(dbl(X)) -> dbl#(mark(X))
    active#(dbls(nil())) -> mark#(nil()) ->
    mark#(dbl(X)) -> mark#(X)
    active#(dbl(s(X))) -> s#(s(dbl(X))) ->
    s#(active(X)) -> s#(X)
    active#(dbl(s(X))) -> s#(s(dbl(X))) -> s#(mark(X)) -> s#(X)
    active#(dbl(s(X))) -> s#(dbl(X)) -> s#(active(X)) -> s#(X)
    active#(dbl(s(X))) -> s#(dbl(X)) -> s#(mark(X)) -> s#(X)
    active#(dbl(s(X))) -> dbl#(X) -> dbl#(active(X)) -> dbl#(X)
    active#(dbl(s(X))) -> dbl#(X) ->
    dbl#(mark(X)) -> dbl#(X)
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(from(X)) -> active#(from(X))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(indx(X1,X2)) -> mark#(X1)
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(nil()) -> active#(nil())
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(dbls(X)) -> mark#(X)
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(s(X)) -> active#(s(X))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(0()) -> active#(0())
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(dbl(X)) -> dbl#(mark(X))
    active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
    mark#(dbl(X)) -> mark#(X)
    active#(dbl(0())) -> mark#(0()) ->
    mark#(from(X)) -> active#(from(X))
    active#(dbl(0())) -> mark#(0()) ->
    mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
    active#(dbl(0())) -> mark#(0()) ->
    mark#(indx(X1,X2)) -> indx#(mark(X1),X2)
    active#(dbl(0())) -> mark#(0()) ->
    mark#(indx(X1,X2)) -> mark#(X1)
    active#(dbl(0())) -> mark#(0()) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(dbl(0())) -> mark#(0()) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(dbl(0())) -> mark#(0()) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(dbl(0())) -> mark#(0()) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(dbl(0())) -> mark#(0()) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(dbl(0())) -> mark#(0()) ->
    mark#(nil()) -> active#(nil())
    active#(dbl(0())) -> mark#(0()) ->
    mark#(dbls(X)) -> active#(dbls(mark(X)))
    active#(dbl(0())) -> mark#(0()) ->
    mark#(dbls(X)) -> dbls#(mark(X))
    active#(dbl(0())) -> mark#(0()) -> mark#(dbls(X)) -> mark#(X)
    active#(dbl(0())) -> mark#(0()) -> mark#(s(X)) -> active#(s(X))
    active#(dbl(0())) -> mark#(0()) -> mark#(0()) -> active#(0())
    active#(dbl(0())) -> mark#(0()) ->
    mark#(dbl(X)) -> active#(dbl(mark(X)))
    active#(dbl(0())) -> mark#(0()) ->
    mark#(dbl(X)) -> dbl#(mark(X))
    active#(dbl(0())) -> mark#(0()) -> mark#(dbl(X)) -> mark#(X)
   SCC Processor:
    #sccs: 8
    #rules: 43
    #arcs: 564/3600
    DPs:
     mark#(from(X)) -> active#(from(X))
     active#(dbl(0())) -> mark#(0())
     mark#(dbl(X)) -> mark#(X)
     mark#(dbl(X)) -> active#(dbl(mark(X)))
     active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
     mark#(0()) -> active#(0())
     active#(dbls(nil())) -> mark#(nil())
     mark#(s(X)) -> active#(s(X))
     active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
     mark#(dbls(X)) -> mark#(X)
     mark#(dbls(X)) -> active#(dbls(mark(X)))
     active#(sel(0(),cons(X,Y))) -> mark#(X)
     mark#(nil()) -> active#(nil())
     active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
     mark#(cons(X1,X2)) -> active#(cons(X1,X2))
     active#(indx(nil(),X)) -> mark#(nil())
     mark#(sel(X1,X2)) -> mark#(X2)
     mark#(sel(X1,X2)) -> mark#(X1)
     mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
     active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
     mark#(indx(X1,X2)) -> mark#(X1)
     mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
     active#(from(X)) -> mark#(cons(X,from(s(X))))
    TRS:
     active(dbl(0())) -> mark(0())
     active(dbl(s(X))) -> mark(s(s(dbl(X))))
     active(dbls(nil())) -> mark(nil())
     active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     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))))
     mark(dbl(X)) -> active(dbl(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(dbls(X)) -> active(dbls(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
     mark(from(X)) -> active(from(X))
     dbl(mark(X)) -> dbl(X)
     dbl(active(X)) -> dbl(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     dbls(mark(X)) -> dbls(X)
     dbls(active(X)) -> dbls(X)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
     indx(mark(X1),X2) -> indx(X1,X2)
     indx(X1,mark(X2)) -> indx(X1,X2)
     indx(active(X1),X2) -> indx(X1,X2)
     indx(X1,active(X2)) -> indx(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    EDG Processor:
     DPs:
      mark#(from(X)) -> active#(from(X))
      active#(dbl(0())) -> mark#(0())
      mark#(dbl(X)) -> mark#(X)
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
      mark#(0()) -> active#(0())
      active#(dbls(nil())) -> mark#(nil())
      mark#(s(X)) -> active#(s(X))
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
      mark#(dbls(X)) -> mark#(X)
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      active#(sel(0(),cons(X,Y))) -> mark#(X)
      mark#(nil()) -> active#(nil())
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(indx(nil(),X)) -> mark#(nil())
      mark#(sel(X1,X2)) -> mark#(X2)
      mark#(sel(X1,X2)) -> mark#(X1)
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
      mark#(indx(X1,X2)) -> mark#(X1)
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      active#(from(X)) -> mark#(cons(X,from(s(X))))
     TRS:
      active(dbl(0())) -> mark(0())
      active(dbl(s(X))) -> mark(s(s(dbl(X))))
      active(dbls(nil())) -> mark(nil())
      active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
      active(sel(0(),cons(X,Y))) -> mark(X)
      active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
      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))))
      mark(dbl(X)) -> active(dbl(mark(X)))
      mark(0()) -> active(0())
      mark(s(X)) -> active(s(X))
      mark(dbls(X)) -> active(dbls(mark(X)))
      mark(nil()) -> active(nil())
      mark(cons(X1,X2)) -> active(cons(X1,X2))
      mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
      mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
      mark(from(X)) -> active(from(X))
      dbl(mark(X)) -> dbl(X)
      dbl(active(X)) -> dbl(X)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      dbls(mark(X)) -> dbls(X)
      dbls(active(X)) -> dbls(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      sel(mark(X1),X2) -> sel(X1,X2)
      sel(X1,mark(X2)) -> sel(X1,X2)
      sel(active(X1),X2) -> sel(X1,X2)
      sel(X1,active(X2)) -> sel(X1,X2)
      indx(mark(X1),X2) -> indx(X1,X2)
      indx(X1,mark(X2)) -> indx(X1,X2)
      indx(active(X1),X2) -> indx(X1,X2)
      indx(X1,active(X2)) -> indx(X1,X2)
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
     graph:
      mark#(from(X)) -> active#(from(X)) ->
      active#(dbl(0())) -> mark#(0())
      mark#(from(X)) -> active#(from(X)) ->
      active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
      mark#(from(X)) -> active#(from(X)) ->
      active#(dbls(nil())) -> mark#(nil())
      mark#(from(X)) -> active#(from(X)) ->
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
      mark#(from(X)) -> active#(from(X)) ->
      active#(sel(0(),cons(X,Y))) -> mark#(X)
      mark#(from(X)) -> active#(from(X)) ->
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
      mark#(from(X)) -> active#(from(X)) ->
      active#(indx(nil(),X)) -> mark#(nil())
      mark#(from(X)) -> active#(from(X)) ->
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
      mark#(from(X)) -> active#(from(X)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(indx(X1,X2)) -> mark#(X1) -> mark#(dbl(X)) -> mark#(X)
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      mark#(indx(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(s(X)) -> active#(s(X))
      mark#(indx(X1,X2)) -> mark#(X1) -> mark#(dbls(X)) -> mark#(X)
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(nil()) -> active#(nil())
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(sel(X1,X2)) -> mark#(X2)
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(sel(X1,X2)) -> mark#(X1)
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(indx(X1,X2)) -> mark#(X1)
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      mark#(indx(X1,X2)) -> mark#(X1) ->
      mark#(from(X)) -> active#(from(X))
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
      active#(dbl(0())) -> mark#(0())
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
      active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
      active#(dbls(nil())) -> mark#(nil())
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
      active#(sel(0(),cons(X,Y))) -> mark#(X)
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
      active#(indx(nil(),X)) -> mark#(nil())
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbl(X)) -> mark#(X)
      mark#(sel(X1,X2)) -> mark#(X2) ->
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      mark#(sel(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
      mark#(sel(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(X))
      mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbls(X)) -> mark#(X)
      mark#(sel(X1,X2)) -> mark#(X2) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      mark#(sel(X1,X2)) -> mark#(X2) ->
      mark#(nil()) -> active#(nil())
      mark#(sel(X1,X2)) -> mark#(X2) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      mark#(sel(X1,X2)) -> mark#(X2) ->
      mark#(sel(X1,X2)) -> mark#(X2)
      mark#(sel(X1,X2)) -> mark#(X2) ->
      mark#(sel(X1,X2)) -> mark#(X1)
      mark#(sel(X1,X2)) -> mark#(X2) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      mark#(sel(X1,X2)) -> mark#(X2) ->
      mark#(indx(X1,X2)) -> mark#(X1)
      mark#(sel(X1,X2)) -> mark#(X2) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      mark#(sel(X1,X2)) -> mark#(X2) ->
      mark#(from(X)) -> active#(from(X))
      mark#(sel(X1,X2)) -> mark#(X1) -> mark#(dbl(X)) -> mark#(X)
      mark#(sel(X1,X2)) -> mark#(X1) ->
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      mark#(sel(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
      mark#(sel(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
      mark#(sel(X1,X2)) -> mark#(X1) -> mark#(dbls(X)) -> mark#(X)
      mark#(sel(X1,X2)) -> mark#(X1) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      mark#(sel(X1,X2)) -> mark#(X1) ->
      mark#(nil()) -> active#(nil())
      mark#(sel(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      mark#(sel(X1,X2)) -> mark#(X1) ->
      mark#(sel(X1,X2)) -> mark#(X2)
      mark#(sel(X1,X2)) -> mark#(X1) ->
      mark#(sel(X1,X2)) -> mark#(X1)
      mark#(sel(X1,X2)) -> mark#(X1) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      mark#(sel(X1,X2)) -> mark#(X1) ->
      mark#(indx(X1,X2)) -> mark#(X1)
      mark#(sel(X1,X2)) -> mark#(X1) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      mark#(sel(X1,X2)) -> mark#(X1) ->
      mark#(from(X)) -> active#(from(X))
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
      active#(dbl(0())) -> mark#(0())
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
      active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
      active#(dbls(nil())) -> mark#(nil())
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
      active#(sel(0(),cons(X,Y))) -> mark#(X)
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
      active#(indx(nil(),X)) -> mark#(nil())
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(dbl(0())) -> mark#(0())
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(dbls(nil())) -> mark#(nil())
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(sel(0(),cons(X,Y))) -> mark#(X)
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(indx(nil(),X)) -> mark#(nil())
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(dbls(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
      mark#(dbls(X)) -> mark#(X) ->
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      mark#(dbls(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(dbls(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
      mark#(dbls(X)) -> mark#(X) -> mark#(dbls(X)) -> mark#(X)
      mark#(dbls(X)) -> mark#(X) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      mark#(dbls(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
      mark#(dbls(X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      mark#(dbls(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2)
      mark#(dbls(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1)
      mark#(dbls(X)) -> mark#(X) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      mark#(dbls(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> mark#(X1)
      mark#(dbls(X)) -> mark#(X) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      mark#(dbls(X)) -> mark#(X) ->
      mark#(from(X)) -> active#(from(X))
      mark#(dbls(X)) -> active#(dbls(mark(X))) ->
      active#(dbl(0())) -> mark#(0())
      mark#(dbls(X)) -> active#(dbls(mark(X))) ->
      active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
      mark#(dbls(X)) -> active#(dbls(mark(X))) ->
      active#(dbls(nil())) -> mark#(nil())
      mark#(dbls(X)) -> active#(dbls(mark(X))) ->
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
      mark#(dbls(X)) -> active#(dbls(mark(X))) ->
      active#(sel(0(),cons(X,Y))) -> mark#(X)
      mark#(dbls(X)) -> active#(dbls(mark(X))) ->
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
      mark#(dbls(X)) -> active#(dbls(mark(X))) ->
      active#(indx(nil(),X)) -> mark#(nil())
      mark#(dbls(X)) -> active#(dbls(mark(X))) ->
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
      mark#(dbls(X)) -> active#(dbls(mark(X))) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(s(X)) -> active#(s(X)) -> active#(dbl(0())) -> mark#(0())
      mark#(s(X)) -> active#(s(X)) ->
      active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
      mark#(s(X)) -> active#(s(X)) ->
      active#(dbls(nil())) -> mark#(nil())
      mark#(s(X)) -> active#(s(X)) ->
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
      mark#(s(X)) -> active#(s(X)) ->
      active#(sel(0(),cons(X,Y))) -> mark#(X)
      mark#(s(X)) -> active#(s(X)) ->
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
      mark#(s(X)) -> active#(s(X)) ->
      active#(indx(nil(),X)) -> mark#(nil())
      mark#(s(X)) -> active#(s(X)) ->
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
      mark#(s(X)) -> active#(s(X)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
      mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> active#(dbl(mark(X)))
      mark#(dbl(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(dbl(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
      mark#(dbl(X)) -> mark#(X) -> mark#(dbls(X)) -> mark#(X)
      mark#(dbl(X)) -> mark#(X) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      mark#(dbl(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
      mark#(dbl(X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      mark#(dbl(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2)
      mark#(dbl(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1)
      mark#(dbl(X)) -> mark#(X) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      mark#(dbl(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> mark#(X1)
      mark#(dbl(X)) -> mark#(X) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      mark#(dbl(X)) -> mark#(X) ->
      mark#(from(X)) -> active#(from(X))
      mark#(dbl(X)) -> active#(dbl(mark(X))) ->
      active#(dbl(0())) -> mark#(0())
      mark#(dbl(X)) -> active#(dbl(mark(X))) ->
      active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
      mark#(dbl(X)) -> active#(dbl(mark(X))) ->
      active#(dbls(nil())) -> mark#(nil())
      mark#(dbl(X)) -> active#(dbl(mark(X))) ->
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
      mark#(dbl(X)) -> active#(dbl(mark(X))) ->
      active#(sel(0(),cons(X,Y))) -> mark#(X)
      mark#(dbl(X)) -> active#(dbl(mark(X))) ->
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
      mark#(dbl(X)) -> active#(dbl(mark(X))) ->
      active#(indx(nil(),X)) -> mark#(nil())
      mark#(dbl(X)) -> active#(dbl(mark(X))) ->
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
      mark#(dbl(X)) -> active#(dbl(mark(X))) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(dbl(X)) -> mark#(X)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(s(X)) -> active#(s(X))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(dbls(X)) -> mark#(X)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(sel(X1,X2)) -> mark#(X2)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(sel(X1,X2)) -> mark#(X1)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(indx(X1,X2)) -> mark#(X1)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(from(X)) -> active#(from(X))
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(dbl(X)) -> mark#(X)
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(s(X)) -> active#(s(X))
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(dbls(X)) -> mark#(X)
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(sel(X1,X2)) -> mark#(X2)
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(sel(X1,X2)) -> mark#(X1)
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(indx(X1,X2)) -> mark#(X1)
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
      mark#(from(X)) -> active#(from(X))
      active#(indx(nil(),X)) -> mark#(nil()) ->
      mark#(nil()) -> active#(nil())
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(dbl(X)) -> mark#(X)
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(s(X)) -> active#(s(X))
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(dbls(X)) -> mark#(X)
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(sel(X1,X2)) -> mark#(X2)
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(sel(X1,X2)) -> mark#(X1)
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(indx(X1,X2)) -> mark#(X1)
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
      mark#(from(X)) -> active#(from(X))
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(dbl(X)) -> mark#(X)
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(0()) -> active#(0())
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(s(X)) -> active#(s(X))
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(dbls(X)) -> mark#(X)
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(nil()) -> active#(nil())
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(sel(X1,X2)) -> mark#(X2)
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(sel(X1,X2)) -> mark#(X1)
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(indx(X1,X2)) -> mark#(X1)
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      active#(sel(0(),cons(X,Y))) -> mark#(X) ->
      mark#(from(X)) -> active#(from(X))
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(dbl(X)) -> mark#(X)
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(s(X)) -> active#(s(X))
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(dbls(X)) -> mark#(X)
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(sel(X1,X2)) -> mark#(X2)
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(sel(X1,X2)) -> mark#(X1)
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(indx(X1,X2)) -> mark#(X1)
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
      mark#(from(X)) -> active#(from(X))
      active#(dbls(nil())) -> mark#(nil()) ->
      mark#(nil()) -> active#(nil())
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(dbl(X)) -> mark#(X)
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(dbl(X)) -> active#(dbl(mark(X)))
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(s(X)) -> active#(s(X))
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(dbls(X)) -> mark#(X)
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(dbls(X)) -> active#(dbls(mark(X)))
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(sel(X1,X2)) -> mark#(X2)
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(sel(X1,X2)) -> mark#(X1)
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(indx(X1,X2)) -> mark#(X1)
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
      active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
      mark#(from(X)) -> active#(from(X))
      active#(dbl(0())) -> mark#(0()) -> mark#(0()) -> active#(0())
     CDG Processor:
      DPs:
       mark#(from(X)) -> active#(from(X))
       active#(dbl(0())) -> mark#(0())
       mark#(dbl(X)) -> mark#(X)
       mark#(dbl(X)) -> active#(dbl(mark(X)))
       active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
       mark#(0()) -> active#(0())
       active#(dbls(nil())) -> mark#(nil())
       mark#(s(X)) -> active#(s(X))
       active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
       mark#(dbls(X)) -> mark#(X)
       mark#(dbls(X)) -> active#(dbls(mark(X)))
       active#(sel(0(),cons(X,Y))) -> mark#(X)
       mark#(nil()) -> active#(nil())
       active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(indx(nil(),X)) -> mark#(nil())
       mark#(sel(X1,X2)) -> mark#(X2)
       mark#(sel(X1,X2)) -> mark#(X1)
       mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
       active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
       mark#(indx(X1,X2)) -> mark#(X1)
       mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
       active#(from(X)) -> mark#(cons(X,from(s(X))))
      TRS:
       active(dbl(0())) -> mark(0())
       active(dbl(s(X))) -> mark(s(s(dbl(X))))
       active(dbls(nil())) -> mark(nil())
       active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
       active(sel(0(),cons(X,Y))) -> mark(X)
       active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
       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))))
       mark(dbl(X)) -> active(dbl(mark(X)))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(dbls(X)) -> active(dbls(mark(X)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
       mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
       mark(from(X)) -> active(from(X))
       dbl(mark(X)) -> dbl(X)
       dbl(active(X)) -> dbl(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       dbls(mark(X)) -> dbls(X)
       dbls(active(X)) -> dbls(X)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       sel(mark(X1),X2) -> sel(X1,X2)
       sel(X1,mark(X2)) -> sel(X1,X2)
       sel(active(X1),X2) -> sel(X1,X2)
       sel(X1,active(X2)) -> sel(X1,X2)
       indx(mark(X1),X2) -> indx(X1,X2)
       indx(X1,mark(X2)) -> indx(X1,X2)
       indx(active(X1),X2) -> indx(X1,X2)
       indx(X1,active(X2)) -> indx(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
      graph:
       mark#(from(X)) -> active#(from(X)) ->
       active#(from(X)) -> mark#(cons(X,from(s(X))))
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(from(X))
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(indx(X1,X2)) -> mark#(X1)
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(sel(X1,X2)) -> mark#(X1)
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(sel(X1,X2)) -> mark#(X2)
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(nil()) -> active#(nil())
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(dbls(X)) -> active#(dbls(mark(X)))
       mark#(indx(X1,X2)) -> mark#(X1) -> mark#(dbls(X)) -> mark#(X)
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(s(X)) -> active#(s(X))
       mark#(indx(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(dbl(X)) -> active#(dbl(mark(X)))
       mark#(indx(X1,X2)) -> mark#(X1) ->
       mark#(dbl(X)) -> mark#(X)
       mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
       active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z)))
       mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2)) ->
       active#(indx(nil(),X)) -> mark#(nil())
       mark#(sel(X1,X2)) -> mark#(X2) ->
       mark#(from(X)) -> active#(from(X))
       mark#(sel(X1,X2)) -> mark#(X2) ->
       mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
       mark#(sel(X1,X2)) -> mark#(X2) ->
       mark#(indx(X1,X2)) -> mark#(X1)
       mark#(sel(X1,X2)) -> mark#(X2) ->
       mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
       mark#(sel(X1,X2)) -> mark#(X2) ->
       mark#(sel(X1,X2)) -> mark#(X1)
       mark#(sel(X1,X2)) -> mark#(X2) ->
       mark#(sel(X1,X2)) -> mark#(X2)
       mark#(sel(X1,X2)) -> mark#(X2) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       mark#(sel(X1,X2)) -> mark#(X2) ->
       mark#(nil()) -> active#(nil())
       mark#(sel(X1,X2)) -> mark#(X2) ->
       mark#(dbls(X)) -> active#(dbls(mark(X)))
       mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbls(X)) -> mark#(X)
       mark#(sel(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(X))
       mark#(sel(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
       mark#(sel(X1,X2)) -> mark#(X2) ->
       mark#(dbl(X)) -> active#(dbl(mark(X)))
       mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbl(X)) -> mark#(X)
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(from(X))
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(indx(X1,X2)) -> mark#(X1)
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(sel(X1,X2)) -> mark#(X1)
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(sel(X1,X2)) -> mark#(X2)
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(nil()) -> active#(nil())
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(dbls(X)) -> active#(dbls(mark(X)))
       mark#(sel(X1,X2)) -> mark#(X1) -> mark#(dbls(X)) -> mark#(X)
       mark#(sel(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
       mark#(sel(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(dbl(X)) -> active#(dbl(mark(X)))
       mark#(sel(X1,X2)) -> mark#(X1) ->
       mark#(dbl(X)) -> mark#(X)
       mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
       active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
       mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
       active#(sel(0(),cons(X,Y))) -> mark#(X)
       mark#(dbls(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(X))
       mark#(dbls(X)) -> mark#(X) ->
       mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
       mark#(dbls(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> mark#(X1)
       mark#(dbls(X)) -> mark#(X) ->
       mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
       mark#(dbls(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1)
       mark#(dbls(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2)
       mark#(dbls(X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       mark#(dbls(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
       mark#(dbls(X)) -> mark#(X) ->
       mark#(dbls(X)) -> active#(dbls(mark(X)))
       mark#(dbls(X)) -> mark#(X) -> mark#(dbls(X)) -> mark#(X)
       mark#(dbls(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
       mark#(dbls(X)) -> mark#(X) -> mark#(0()) -> active#(0())
       mark#(dbls(X)) -> mark#(X) ->
       mark#(dbl(X)) -> active#(dbl(mark(X)))
       mark#(dbls(X)) -> mark#(X) ->
       mark#(dbl(X)) -> mark#(X)
       mark#(dbls(X)) -> active#(dbls(mark(X))) ->
       active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y)))
       mark#(dbls(X)) -> active#(dbls(mark(X))) ->
       active#(dbls(nil())) -> mark#(nil())
       mark#(dbl(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(X))
       mark#(dbl(X)) -> mark#(X) ->
       mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
       mark#(dbl(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> mark#(X1)
       mark#(dbl(X)) -> mark#(X) ->
       mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
       mark#(dbl(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1)
       mark#(dbl(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2)
       mark#(dbl(X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       mark#(dbl(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
       mark#(dbl(X)) -> mark#(X) ->
       mark#(dbls(X)) -> active#(dbls(mark(X)))
       mark#(dbl(X)) -> mark#(X) -> mark#(dbls(X)) -> mark#(X)
       mark#(dbl(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
       mark#(dbl(X)) -> mark#(X) -> mark#(0()) -> active#(0())
       mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> active#(dbl(mark(X)))
       mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
       mark#(dbl(X)) -> active#(dbl(mark(X))) ->
       active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
       mark#(dbl(X)) -> active#(dbl(mark(X))) ->
       active#(dbl(0())) -> mark#(0())
       active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(indx(cons(X,Y),Z)) -> mark#(cons(sel(X,Z),indx(Y,Z))) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(indx(nil(),X)) -> mark#(nil()) ->
       mark#(nil()) -> active#(nil())
       active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
       mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
       active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
       mark#(sel(X1,X2)) -> mark#(X1)
       active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
       mark#(sel(X1,X2)) -> mark#(X2)
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(from(X)) -> active#(from(X))
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(indx(X1,X2)) -> active#(indx(mark(X1),X2))
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(indx(X1,X2)) -> mark#(X1)
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(sel(X1,X2)) -> mark#(X1)
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(sel(X1,X2)) -> mark#(X2)
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(nil()) -> active#(nil())
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(dbls(X)) -> active#(dbls(mark(X)))
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(dbls(X)) -> mark#(X)
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(s(X)) -> active#(s(X))
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(0()) -> active#(0())
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(dbl(X)) -> active#(dbl(mark(X)))
       active#(sel(0(),cons(X,Y))) -> mark#(X) ->
       mark#(dbl(X)) -> mark#(X)
       active#(dbls(cons(X,Y))) -> mark#(cons(dbl(X),dbls(Y))) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(dbls(nil())) -> mark#(nil()) ->
       mark#(nil()) -> active#(nil())
       active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) ->
       mark#(s(X)) -> active#(s(X))
       active#(dbl(0())) -> mark#(0()) -> mark#(0()) -> active#(0())
      SCC Processor:
       #sccs: 1
       #rules: 8
       #arcs: 103/529
       DPs:
        mark#(indx(X1,X2)) -> mark#(X1)
        mark#(dbl(X)) -> mark#(X)
        mark#(dbls(X)) -> mark#(X)
        mark#(sel(X1,X2)) -> mark#(X2)
        mark#(sel(X1,X2)) -> mark#(X1)
        mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
        active#(sel(0(),cons(X,Y))) -> mark#(X)
        active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
       TRS:
        active(dbl(0())) -> mark(0())
        active(dbl(s(X))) -> mark(s(s(dbl(X))))
        active(dbls(nil())) -> mark(nil())
        active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
        active(sel(0(),cons(X,Y))) -> mark(X)
        active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
        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))))
        mark(dbl(X)) -> active(dbl(mark(X)))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(X))
        mark(dbls(X)) -> active(dbls(mark(X)))
        mark(nil()) -> active(nil())
        mark(cons(X1,X2)) -> active(cons(X1,X2))
        mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
        mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
        mark(from(X)) -> active(from(X))
        dbl(mark(X)) -> dbl(X)
        dbl(active(X)) -> dbl(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        dbls(mark(X)) -> dbls(X)
        dbls(active(X)) -> dbls(X)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        sel(mark(X1),X2) -> sel(X1,X2)
        sel(X1,mark(X2)) -> sel(X1,X2)
        sel(active(X1),X2) -> sel(X1,X2)
        sel(X1,active(X2)) -> sel(X1,X2)
        indx(mark(X1),X2) -> indx(X1,X2)
        indx(X1,mark(X2)) -> indx(X1,X2)
        indx(active(X1),X2) -> indx(X1,X2)
        indx(X1,active(X2)) -> indx(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [mark#](x0) = x0 + 0,
         
         [active#](x0) = x0 + 0,
         
         [from](x0) = x0 + 4,
         
         [indx](x0, x1) = 1x0 + 4x1 + 2,
         
         [sel](x0, x1) = x0 + x1 + 0,
         
         [cons](x0, x1) = x0 + x1 + 0,
         
         [dbls](x0) = x0 + 0,
         
         [nil] = 2,
         
         [s](x0) = x0 + 0,
         
         [mark](x0) = x0 + 0,
         
         [active](x0) = x0 + 0,
         
         [dbl](x0) = x0 + 0,
         
         [0] = 0
        orientation:
         mark#(indx(X1,X2)) = 1X1 + 4X2 + 2 >= X1 + 0 = mark#(X1)
         
         mark#(dbl(X)) = X + 0 >= X + 0 = mark#(X)
         
         mark#(dbls(X)) = X + 0 >= X + 0 = mark#(X)
         
         mark#(sel(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = mark#(X2)
         
         mark#(sel(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = mark#(X1)
         
         mark#(sel(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active#(sel(mark(X1),mark(X2)))
         
         active#(sel(0(),cons(X,Y))) = X + Y + 0 >= X + 0 = mark#(X)
         
         active#(sel(s(X),cons(Y,Z))) = X + Y + Z + 0 >= X + Z + 0 = mark#(sel(X,Z))
         
         active(dbl(0())) = 0 >= 0 = mark(0())
         
         active(dbl(s(X))) = X + 0 >= X + 0 = mark(s(s(dbl(X))))
         
         active(dbls(nil())) = 2 >= 2 = mark(nil())
         
         active(dbls(cons(X,Y))) = X + Y + 0 >= X + Y + 0 = mark(cons(dbl(X),dbls(Y)))
         
         active(sel(0(),cons(X,Y))) = X + Y + 0 >= X + 0 = mark(X)
         
         active(sel(s(X),cons(Y,Z))) = X + Y + Z + 0 >= X + Z + 0 = mark(sel(X,Z))
         
         active(indx(nil(),X)) = 4X + 3 >= 2 = mark(nil())
         
         active(indx(cons(X,Y),Z)) = 1X + 1Y + 4Z + 2 >= X + 1Y + 4Z + 2 = mark(cons(sel(X,Z),indx(Y,Z)))
         
         active(from(X)) = X + 4 >= X + 4 = mark(cons(X,from(s(X))))
         
         mark(dbl(X)) = X + 0 >= X + 0 = active(dbl(mark(X)))
         
         mark(0()) = 0 >= 0 = active(0())
         
         mark(s(X)) = X + 0 >= X + 0 = active(s(X))
         
         mark(dbls(X)) = X + 0 >= X + 0 = active(dbls(mark(X)))
         
         mark(nil()) = 2 >= 2 = active(nil())
         
         mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active(cons(X1,X2))
         
         mark(sel(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active(sel(mark(X1),mark(X2)))
         
         mark(indx(X1,X2)) = 1X1 + 4X2 + 2 >= 1X1 + 4X2 + 2 = active(indx(mark(X1),X2))
         
         mark(from(X)) = X + 4 >= X + 4 = active(from(X))
         
         dbl(mark(X)) = X + 0 >= X + 0 = dbl(X)
         
         dbl(active(X)) = X + 0 >= X + 0 = dbl(X)
         
         s(mark(X)) = X + 0 >= X + 0 = s(X)
         
         s(active(X)) = X + 0 >= X + 0 = s(X)
         
         dbls(mark(X)) = X + 0 >= X + 0 = dbls(X)
         
         dbls(active(X)) = X + 0 >= X + 0 = dbls(X)
         
         cons(mark(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
         
         cons(X1,mark(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
         
         cons(active(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
         
         cons(X1,active(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
         
         sel(mark(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = sel(X1,X2)
         
         sel(X1,mark(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = sel(X1,X2)
         
         sel(active(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = sel(X1,X2)
         
         sel(X1,active(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = sel(X1,X2)
         
         indx(mark(X1),X2) = 1X1 + 4X2 + 2 >= 1X1 + 4X2 + 2 = indx(X1,X2)
         
         indx(X1,mark(X2)) = 1X1 + 4X2 + 4 >= 1X1 + 4X2 + 2 = indx(X1,X2)
         
         indx(active(X1),X2) = 1X1 + 4X2 + 2 >= 1X1 + 4X2 + 2 = indx(X1,X2)
         
         indx(X1,active(X2)) = 1X1 + 4X2 + 4 >= 1X1 + 4X2 + 2 = indx(X1,X2)
         
         from(mark(X)) = X + 4 >= X + 4 = from(X)
         
         from(active(X)) = X + 4 >= X + 4 = from(X)
        problem:
         DPs:
          mark#(dbl(X)) -> mark#(X)
          mark#(dbls(X)) -> mark#(X)
          mark#(sel(X1,X2)) -> mark#(X2)
          mark#(sel(X1,X2)) -> mark#(X1)
          mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
          active#(sel(0(),cons(X,Y))) -> mark#(X)
          active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
         TRS:
          active(dbl(0())) -> mark(0())
          active(dbl(s(X))) -> mark(s(s(dbl(X))))
          active(dbls(nil())) -> mark(nil())
          active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
          active(sel(0(),cons(X,Y))) -> mark(X)
          active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
          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))))
          mark(dbl(X)) -> active(dbl(mark(X)))
          mark(0()) -> active(0())
          mark(s(X)) -> active(s(X))
          mark(dbls(X)) -> active(dbls(mark(X)))
          mark(nil()) -> active(nil())
          mark(cons(X1,X2)) -> active(cons(X1,X2))
          mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
          mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
          mark(from(X)) -> active(from(X))
          dbl(mark(X)) -> dbl(X)
          dbl(active(X)) -> dbl(X)
          s(mark(X)) -> s(X)
          s(active(X)) -> s(X)
          dbls(mark(X)) -> dbls(X)
          dbls(active(X)) -> dbls(X)
          cons(mark(X1),X2) -> cons(X1,X2)
          cons(X1,mark(X2)) -> cons(X1,X2)
          cons(active(X1),X2) -> cons(X1,X2)
          cons(X1,active(X2)) -> cons(X1,X2)
          sel(mark(X1),X2) -> sel(X1,X2)
          sel(X1,mark(X2)) -> sel(X1,X2)
          sel(active(X1),X2) -> sel(X1,X2)
          sel(X1,active(X2)) -> sel(X1,X2)
          indx(mark(X1),X2) -> indx(X1,X2)
          indx(X1,mark(X2)) -> indx(X1,X2)
          indx(active(X1),X2) -> indx(X1,X2)
          indx(X1,active(X2)) -> indx(X1,X2)
          from(mark(X)) -> from(X)
          from(active(X)) -> from(X)
        Arctic Interpretation Processor:
         dimension: 1
         interpretation:
          [mark#](x0) = x0,
          
          [active#](x0) = x0 + 0,
          
          [from](x0) = x0 + 0,
          
          [indx](x0, x1) = 7x0 + x1 + 7,
          
          [sel](x0, x1) = 7x0 + x1 + 7,
          
          [cons](x0, x1) = x0 + x1 + 0,
          
          [dbls](x0) = x0 + 0,
          
          [nil] = 0,
          
          [s](x0) = x0 + 0,
          
          [mark](x0) = x0,
          
          [active](x0) = x0 + 0,
          
          [dbl](x0) = x0 + 0,
          
          [0] = 0
         orientation:
          mark#(dbl(X)) = X + 0 >= X = mark#(X)
          
          mark#(dbls(X)) = X + 0 >= X = mark#(X)
          
          mark#(sel(X1,X2)) = 7X1 + X2 + 7 >= X2 = mark#(X2)
          
          mark#(sel(X1,X2)) = 7X1 + X2 + 7 >= X1 = mark#(X1)
          
          mark#(sel(X1,X2)) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = active#(sel(mark(X1),mark(X2)))
          
          active#(sel(0(),cons(X,Y))) = X + Y + 7 >= X = mark#(X)
          
          active#(sel(s(X),cons(Y,Z))) = 7X + Y + Z + 7 >= 7X + Z + 7 = mark#(sel(X,Z))
          
          active(dbl(0())) = 0 >= 0 = mark(0())
          
          active(dbl(s(X))) = X + 0 >= X + 0 = mark(s(s(dbl(X))))
          
          active(dbls(nil())) = 0 >= 0 = mark(nil())
          
          active(dbls(cons(X,Y))) = X + Y + 0 >= X + Y + 0 = mark(cons(dbl(X),dbls(Y)))
          
          active(sel(0(),cons(X,Y))) = X + Y + 7 >= X = mark(X)
          
          active(sel(s(X),cons(Y,Z))) = 7X + Y + Z + 7 >= 7X + Z + 7 = mark(sel(X,Z))
          
          active(indx(nil(),X)) = X + 7 >= 0 = mark(nil())
          
          active(indx(cons(X,Y),Z)) = 7X + 7Y + Z + 7 >= 7X + 7Y + Z + 7 = mark(cons(sel(X,Z),indx(Y,Z)))
          
          active(from(X)) = X + 0 >= X + 0 = mark(cons(X,from(s(X))))
          
          mark(dbl(X)) = X + 0 >= X + 0 = active(dbl(mark(X)))
          
          mark(0()) = 0 >= 0 = active(0())
          
          mark(s(X)) = X + 0 >= X + 0 = active(s(X))
          
          mark(dbls(X)) = X + 0 >= X + 0 = active(dbls(mark(X)))
          
          mark(nil()) = 0 >= 0 = active(nil())
          
          mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active(cons(X1,X2))
          
          mark(sel(X1,X2)) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = active(sel(mark(X1),mark(X2)))
          
          mark(indx(X1,X2)) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = active(indx(mark(X1),X2))
          
          mark(from(X)) = X + 0 >= X + 0 = active(from(X))
          
          dbl(mark(X)) = X + 0 >= X + 0 = dbl(X)
          
          dbl(active(X)) = X + 0 >= X + 0 = dbl(X)
          
          s(mark(X)) = X + 0 >= X + 0 = s(X)
          
          s(active(X)) = X + 0 >= X + 0 = s(X)
          
          dbls(mark(X)) = X + 0 >= X + 0 = dbls(X)
          
          dbls(active(X)) = X + 0 >= X + 0 = dbls(X)
          
          cons(mark(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
          
          cons(X1,mark(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
          
          cons(active(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
          
          cons(X1,active(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
          
          sel(mark(X1),X2) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = sel(X1,X2)
          
          sel(X1,mark(X2)) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = sel(X1,X2)
          
          sel(active(X1),X2) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = sel(X1,X2)
          
          sel(X1,active(X2)) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = sel(X1,X2)
          
          indx(mark(X1),X2) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = indx(X1,X2)
          
          indx(X1,mark(X2)) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = indx(X1,X2)
          
          indx(active(X1),X2) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = indx(X1,X2)
          
          indx(X1,active(X2)) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = indx(X1,X2)
          
          from(mark(X)) = X + 0 >= X + 0 = from(X)
          
          from(active(X)) = X + 0 >= X + 0 = from(X)
         problem:
          DPs:
           mark#(dbl(X)) -> mark#(X)
           mark#(dbls(X)) -> mark#(X)
           mark#(sel(X1,X2)) -> mark#(X2)
           mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
           active#(sel(0(),cons(X,Y))) -> mark#(X)
           active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
          TRS:
           active(dbl(0())) -> mark(0())
           active(dbl(s(X))) -> mark(s(s(dbl(X))))
           active(dbls(nil())) -> mark(nil())
           active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
           active(sel(0(),cons(X,Y))) -> mark(X)
           active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
           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))))
           mark(dbl(X)) -> active(dbl(mark(X)))
           mark(0()) -> active(0())
           mark(s(X)) -> active(s(X))
           mark(dbls(X)) -> active(dbls(mark(X)))
           mark(nil()) -> active(nil())
           mark(cons(X1,X2)) -> active(cons(X1,X2))
           mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
           mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
           mark(from(X)) -> active(from(X))
           dbl(mark(X)) -> dbl(X)
           dbl(active(X)) -> dbl(X)
           s(mark(X)) -> s(X)
           s(active(X)) -> s(X)
           dbls(mark(X)) -> dbls(X)
           dbls(active(X)) -> dbls(X)
           cons(mark(X1),X2) -> cons(X1,X2)
           cons(X1,mark(X2)) -> cons(X1,X2)
           cons(active(X1),X2) -> cons(X1,X2)
           cons(X1,active(X2)) -> cons(X1,X2)
           sel(mark(X1),X2) -> sel(X1,X2)
           sel(X1,mark(X2)) -> sel(X1,X2)
           sel(active(X1),X2) -> sel(X1,X2)
           sel(X1,active(X2)) -> sel(X1,X2)
           indx(mark(X1),X2) -> indx(X1,X2)
           indx(X1,mark(X2)) -> indx(X1,X2)
           indx(active(X1),X2) -> indx(X1,X2)
           indx(X1,active(X2)) -> indx(X1,X2)
           from(mark(X)) -> from(X)
           from(active(X)) -> from(X)
         Arctic Interpretation Processor:
          dimension: 1
          interpretation:
           [mark#](x0) = 4x0,
           
           [active#](x0) = 4x0,
           
           [from](x0) = 5x0 + 3,
           
           [indx](x0, x1) = 3x0 + 6x1 + 1,
           
           [sel](x0, x1) = x0 + 3x1,
           
           [cons](x0, x1) = x0 + x1 + 0,
           
           [dbls](x0) = 3x0 + 2,
           
           [nil] = 0,
           
           [s](x0) = x0,
           
           [mark](x0) = x0,
           
           [active](x0) = x0,
           
           [dbl](x0) = x0 + 0,
           
           [0] = 1
          orientation:
           mark#(dbl(X)) = 4X + 4 >= 4X = mark#(X)
           
           mark#(dbls(X)) = 7X + 6 >= 4X = mark#(X)
           
           mark#(sel(X1,X2)) = 4X1 + 7X2 >= 4X2 = mark#(X2)
           
           mark#(sel(X1,X2)) = 4X1 + 7X2 >= 4X1 + 7X2 = active#(sel(mark(X1),mark(X2)))
           
           active#(sel(0(),cons(X,Y))) = 7X + 7Y + 7 >= 4X = mark#(X)
           
           active#(sel(s(X),cons(Y,Z))) = 4X + 7Y + 7Z + 7 >= 4X + 7Z = mark#(sel(X,Z))
           
           active(dbl(0())) = 1 >= 1 = mark(0())
           
           active(dbl(s(X))) = X + 0 >= X + 0 = mark(s(s(dbl(X))))
           
           active(dbls(nil())) = 3 >= 0 = mark(nil())
           
           active(dbls(cons(X,Y))) = 3X + 3Y + 3 >= X + 3Y + 2 = mark(cons(dbl(X),dbls(Y)))
           
           active(sel(0(),cons(X,Y))) = 3X + 3Y + 3 >= X = mark(X)
           
           active(sel(s(X),cons(Y,Z))) = X + 3Y + 3Z + 3 >= X + 3Z = mark(sel(X,Z))
           
           active(indx(nil(),X)) = 6X + 3 >= 0 = mark(nil())
           
           active(indx(cons(X,Y),Z)) = 3X + 3Y + 6Z + 3 >= X + 3Y + 6Z + 1 = mark(cons(sel(X,Z),indx(Y,Z)))
           
           active(from(X)) = 5X + 3 >= 5X + 3 = mark(cons(X,from(s(X))))
           
           mark(dbl(X)) = X + 0 >= X + 0 = active(dbl(mark(X)))
           
           mark(0()) = 1 >= 1 = active(0())
           
           mark(s(X)) = X >= X = active(s(X))
           
           mark(dbls(X)) = 3X + 2 >= 3X + 2 = active(dbls(mark(X)))
           
           mark(nil()) = 0 >= 0 = active(nil())
           
           mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active(cons(X1,X2))
           
           mark(sel(X1,X2)) = X1 + 3X2 >= X1 + 3X2 = active(sel(mark(X1),mark(X2)))
           
           mark(indx(X1,X2)) = 3X1 + 6X2 + 1 >= 3X1 + 6X2 + 1 = active(indx(mark(X1),X2))
           
           mark(from(X)) = 5X + 3 >= 5X + 3 = active(from(X))
           
           dbl(mark(X)) = X + 0 >= X + 0 = dbl(X)
           
           dbl(active(X)) = X + 0 >= X + 0 = dbl(X)
           
           s(mark(X)) = X >= X = s(X)
           
           s(active(X)) = X >= X = s(X)
           
           dbls(mark(X)) = 3X + 2 >= 3X + 2 = dbls(X)
           
           dbls(active(X)) = 3X + 2 >= 3X + 2 = dbls(X)
           
           cons(mark(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
           
           cons(X1,mark(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
           
           cons(active(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
           
           cons(X1,active(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
           
           sel(mark(X1),X2) = X1 + 3X2 >= X1 + 3X2 = sel(X1,X2)
           
           sel(X1,mark(X2)) = X1 + 3X2 >= X1 + 3X2 = sel(X1,X2)
           
           sel(active(X1),X2) = X1 + 3X2 >= X1 + 3X2 = sel(X1,X2)
           
           sel(X1,active(X2)) = X1 + 3X2 >= X1 + 3X2 = sel(X1,X2)
           
           indx(mark(X1),X2) = 3X1 + 6X2 + 1 >= 3X1 + 6X2 + 1 = indx(X1,X2)
           
           indx(X1,mark(X2)) = 3X1 + 6X2 + 1 >= 3X1 + 6X2 + 1 = indx(X1,X2)
           
           indx(active(X1),X2) = 3X1 + 6X2 + 1 >= 3X1 + 6X2 + 1 = indx(X1,X2)
           
           indx(X1,active(X2)) = 3X1 + 6X2 + 1 >= 3X1 + 6X2 + 1 = indx(X1,X2)
           
           from(mark(X)) = 5X + 3 >= 5X + 3 = from(X)
           
           from(active(X)) = 5X + 3 >= 5X + 3 = from(X)
          problem:
           DPs:
            mark#(dbl(X)) -> mark#(X)
            mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
            active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
           TRS:
            active(dbl(0())) -> mark(0())
            active(dbl(s(X))) -> mark(s(s(dbl(X))))
            active(dbls(nil())) -> mark(nil())
            active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
            active(sel(0(),cons(X,Y))) -> mark(X)
            active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
            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))))
            mark(dbl(X)) -> active(dbl(mark(X)))
            mark(0()) -> active(0())
            mark(s(X)) -> active(s(X))
            mark(dbls(X)) -> active(dbls(mark(X)))
            mark(nil()) -> active(nil())
            mark(cons(X1,X2)) -> active(cons(X1,X2))
            mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
            mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
            mark(from(X)) -> active(from(X))
            dbl(mark(X)) -> dbl(X)
            dbl(active(X)) -> dbl(X)
            s(mark(X)) -> s(X)
            s(active(X)) -> s(X)
            dbls(mark(X)) -> dbls(X)
            dbls(active(X)) -> dbls(X)
            cons(mark(X1),X2) -> cons(X1,X2)
            cons(X1,mark(X2)) -> cons(X1,X2)
            cons(active(X1),X2) -> cons(X1,X2)
            cons(X1,active(X2)) -> cons(X1,X2)
            sel(mark(X1),X2) -> sel(X1,X2)
            sel(X1,mark(X2)) -> sel(X1,X2)
            sel(active(X1),X2) -> sel(X1,X2)
            sel(X1,active(X2)) -> sel(X1,X2)
            indx(mark(X1),X2) -> indx(X1,X2)
            indx(X1,mark(X2)) -> indx(X1,X2)
            indx(active(X1),X2) -> indx(X1,X2)
            indx(X1,active(X2)) -> indx(X1,X2)
            from(mark(X)) -> from(X)
            from(active(X)) -> from(X)
          SCC Processor:
           #sccs: 2
           #rules: 3
           #arcs: 41/9
           DPs:
            mark#(dbl(X)) -> mark#(X)
           TRS:
            active(dbl(0())) -> mark(0())
            active(dbl(s(X))) -> mark(s(s(dbl(X))))
            active(dbls(nil())) -> mark(nil())
            active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
            active(sel(0(),cons(X,Y))) -> mark(X)
            active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
            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))))
            mark(dbl(X)) -> active(dbl(mark(X)))
            mark(0()) -> active(0())
            mark(s(X)) -> active(s(X))
            mark(dbls(X)) -> active(dbls(mark(X)))
            mark(nil()) -> active(nil())
            mark(cons(X1,X2)) -> active(cons(X1,X2))
            mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
            mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
            mark(from(X)) -> active(from(X))
            dbl(mark(X)) -> dbl(X)
            dbl(active(X)) -> dbl(X)
            s(mark(X)) -> s(X)
            s(active(X)) -> s(X)
            dbls(mark(X)) -> dbls(X)
            dbls(active(X)) -> dbls(X)
            cons(mark(X1),X2) -> cons(X1,X2)
            cons(X1,mark(X2)) -> cons(X1,X2)
            cons(active(X1),X2) -> cons(X1,X2)
            cons(X1,active(X2)) -> cons(X1,X2)
            sel(mark(X1),X2) -> sel(X1,X2)
            sel(X1,mark(X2)) -> sel(X1,X2)
            sel(active(X1),X2) -> sel(X1,X2)
            sel(X1,active(X2)) -> sel(X1,X2)
            indx(mark(X1),X2) -> indx(X1,X2)
            indx(X1,mark(X2)) -> indx(X1,X2)
            indx(active(X1),X2) -> indx(X1,X2)
            indx(X1,active(X2)) -> indx(X1,X2)
            from(mark(X)) -> from(X)
            from(active(X)) -> from(X)
           Subterm Criterion Processor:
            simple projection:
             pi(mark#) = 0
            problem:
             DPs:
              
             TRS:
              active(dbl(0())) -> mark(0())
              active(dbl(s(X))) -> mark(s(s(dbl(X))))
              active(dbls(nil())) -> mark(nil())
              active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
              active(sel(0(),cons(X,Y))) -> mark(X)
              active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
              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))))
              mark(dbl(X)) -> active(dbl(mark(X)))
              mark(0()) -> active(0())
              mark(s(X)) -> active(s(X))
              mark(dbls(X)) -> active(dbls(mark(X)))
              mark(nil()) -> active(nil())
              mark(cons(X1,X2)) -> active(cons(X1,X2))
              mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
              mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
              mark(from(X)) -> active(from(X))
              dbl(mark(X)) -> dbl(X)
              dbl(active(X)) -> dbl(X)
              s(mark(X)) -> s(X)
              s(active(X)) -> s(X)
              dbls(mark(X)) -> dbls(X)
              dbls(active(X)) -> dbls(X)
              cons(mark(X1),X2) -> cons(X1,X2)
              cons(X1,mark(X2)) -> cons(X1,X2)
              cons(active(X1),X2) -> cons(X1,X2)
              cons(X1,active(X2)) -> cons(X1,X2)
              sel(mark(X1),X2) -> sel(X1,X2)
              sel(X1,mark(X2)) -> sel(X1,X2)
              sel(active(X1),X2) -> sel(X1,X2)
              sel(X1,active(X2)) -> sel(X1,X2)
              indx(mark(X1),X2) -> indx(X1,X2)
              indx(X1,mark(X2)) -> indx(X1,X2)
              indx(active(X1),X2) -> indx(X1,X2)
              indx(X1,active(X2)) -> indx(X1,X2)
              from(mark(X)) -> from(X)
              from(active(X)) -> from(X)
            Qed
           
           DPs:
            mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
            active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
           TRS:
            active(dbl(0())) -> mark(0())
            active(dbl(s(X))) -> mark(s(s(dbl(X))))
            active(dbls(nil())) -> mark(nil())
            active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
            active(sel(0(),cons(X,Y))) -> mark(X)
            active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
            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))))
            mark(dbl(X)) -> active(dbl(mark(X)))
            mark(0()) -> active(0())
            mark(s(X)) -> active(s(X))
            mark(dbls(X)) -> active(dbls(mark(X)))
            mark(nil()) -> active(nil())
            mark(cons(X1,X2)) -> active(cons(X1,X2))
            mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
            mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
            mark(from(X)) -> active(from(X))
            dbl(mark(X)) -> dbl(X)
            dbl(active(X)) -> dbl(X)
            s(mark(X)) -> s(X)
            s(active(X)) -> s(X)
            dbls(mark(X)) -> dbls(X)
            dbls(active(X)) -> dbls(X)
            cons(mark(X1),X2) -> cons(X1,X2)
            cons(X1,mark(X2)) -> cons(X1,X2)
            cons(active(X1),X2) -> cons(X1,X2)
            cons(X1,active(X2)) -> cons(X1,X2)
            sel(mark(X1),X2) -> sel(X1,X2)
            sel(X1,mark(X2)) -> sel(X1,X2)
            sel(active(X1),X2) -> sel(X1,X2)
            sel(X1,active(X2)) -> sel(X1,X2)
            indx(mark(X1),X2) -> indx(X1,X2)
            indx(X1,mark(X2)) -> indx(X1,X2)
            indx(active(X1),X2) -> indx(X1,X2)
            indx(X1,active(X2)) -> indx(X1,X2)
            from(mark(X)) -> from(X)
            from(active(X)) -> from(X)
           Open
    
    DPs:
     dbl#(mark(X)) -> dbl#(X)
     dbl#(active(X)) -> dbl#(X)
    TRS:
     active(dbl(0())) -> mark(0())
     active(dbl(s(X))) -> mark(s(s(dbl(X))))
     active(dbls(nil())) -> mark(nil())
     active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     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))))
     mark(dbl(X)) -> active(dbl(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(dbls(X)) -> active(dbls(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
     mark(from(X)) -> active(from(X))
     dbl(mark(X)) -> dbl(X)
     dbl(active(X)) -> dbl(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     dbls(mark(X)) -> dbls(X)
     dbls(active(X)) -> dbls(X)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
     indx(mark(X1),X2) -> indx(X1,X2)
     indx(X1,mark(X2)) -> indx(X1,X2)
     indx(active(X1),X2) -> indx(X1,X2)
     indx(X1,active(X2)) -> indx(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(dbl#) = 0
     problem:
      DPs:
       
      TRS:
       active(dbl(0())) -> mark(0())
       active(dbl(s(X))) -> mark(s(s(dbl(X))))
       active(dbls(nil())) -> mark(nil())
       active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
       active(sel(0(),cons(X,Y))) -> mark(X)
       active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
       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))))
       mark(dbl(X)) -> active(dbl(mark(X)))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(dbls(X)) -> active(dbls(mark(X)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
       mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
       mark(from(X)) -> active(from(X))
       dbl(mark(X)) -> dbl(X)
       dbl(active(X)) -> dbl(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       dbls(mark(X)) -> dbls(X)
       dbls(active(X)) -> dbls(X)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       sel(mark(X1),X2) -> sel(X1,X2)
       sel(X1,mark(X2)) -> sel(X1,X2)
       sel(active(X1),X2) -> sel(X1,X2)
       sel(X1,active(X2)) -> sel(X1,X2)
       indx(mark(X1),X2) -> indx(X1,X2)
       indx(X1,mark(X2)) -> indx(X1,X2)
       indx(active(X1),X2) -> indx(X1,X2)
       indx(X1,active(X2)) -> indx(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Qed
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(dbl(0())) -> mark(0())
     active(dbl(s(X))) -> mark(s(s(dbl(X))))
     active(dbls(nil())) -> mark(nil())
     active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     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))))
     mark(dbl(X)) -> active(dbl(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(dbls(X)) -> active(dbls(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
     mark(from(X)) -> active(from(X))
     dbl(mark(X)) -> dbl(X)
     dbl(active(X)) -> dbl(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     dbls(mark(X)) -> dbls(X)
     dbls(active(X)) -> dbls(X)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
     indx(mark(X1),X2) -> indx(X1,X2)
     indx(X1,mark(X2)) -> indx(X1,X2)
     indx(active(X1),X2) -> indx(X1,X2)
     indx(X1,active(X2)) -> indx(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(s#) = 0
     problem:
      DPs:
       
      TRS:
       active(dbl(0())) -> mark(0())
       active(dbl(s(X))) -> mark(s(s(dbl(X))))
       active(dbls(nil())) -> mark(nil())
       active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
       active(sel(0(),cons(X,Y))) -> mark(X)
       active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
       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))))
       mark(dbl(X)) -> active(dbl(mark(X)))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(dbls(X)) -> active(dbls(mark(X)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
       mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
       mark(from(X)) -> active(from(X))
       dbl(mark(X)) -> dbl(X)
       dbl(active(X)) -> dbl(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       dbls(mark(X)) -> dbls(X)
       dbls(active(X)) -> dbls(X)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       sel(mark(X1),X2) -> sel(X1,X2)
       sel(X1,mark(X2)) -> sel(X1,X2)
       sel(active(X1),X2) -> sel(X1,X2)
       sel(X1,active(X2)) -> sel(X1,X2)
       indx(mark(X1),X2) -> indx(X1,X2)
       indx(X1,mark(X2)) -> indx(X1,X2)
       indx(active(X1),X2) -> indx(X1,X2)
       indx(X1,active(X2)) -> indx(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Qed
    
    DPs:
     dbls#(mark(X)) -> dbls#(X)
     dbls#(active(X)) -> dbls#(X)
    TRS:
     active(dbl(0())) -> mark(0())
     active(dbl(s(X))) -> mark(s(s(dbl(X))))
     active(dbls(nil())) -> mark(nil())
     active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     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))))
     mark(dbl(X)) -> active(dbl(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(dbls(X)) -> active(dbls(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
     mark(from(X)) -> active(from(X))
     dbl(mark(X)) -> dbl(X)
     dbl(active(X)) -> dbl(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     dbls(mark(X)) -> dbls(X)
     dbls(active(X)) -> dbls(X)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
     indx(mark(X1),X2) -> indx(X1,X2)
     indx(X1,mark(X2)) -> indx(X1,X2)
     indx(active(X1),X2) -> indx(X1,X2)
     indx(X1,active(X2)) -> indx(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(dbls#) = 0
     problem:
      DPs:
       
      TRS:
       active(dbl(0())) -> mark(0())
       active(dbl(s(X))) -> mark(s(s(dbl(X))))
       active(dbls(nil())) -> mark(nil())
       active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
       active(sel(0(),cons(X,Y))) -> mark(X)
       active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
       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))))
       mark(dbl(X)) -> active(dbl(mark(X)))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(dbls(X)) -> active(dbls(mark(X)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
       mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
       mark(from(X)) -> active(from(X))
       dbl(mark(X)) -> dbl(X)
       dbl(active(X)) -> dbl(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       dbls(mark(X)) -> dbls(X)
       dbls(active(X)) -> dbls(X)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       sel(mark(X1),X2) -> sel(X1,X2)
       sel(X1,mark(X2)) -> sel(X1,X2)
       sel(active(X1),X2) -> sel(X1,X2)
       sel(X1,active(X2)) -> sel(X1,X2)
       indx(mark(X1),X2) -> indx(X1,X2)
       indx(X1,mark(X2)) -> indx(X1,X2)
       indx(active(X1),X2) -> indx(X1,X2)
       indx(X1,active(X2)) -> indx(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Qed
    
    DPs:
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     cons#(active(X1),X2) -> cons#(X1,X2)
     cons#(X1,active(X2)) -> cons#(X1,X2)
    TRS:
     active(dbl(0())) -> mark(0())
     active(dbl(s(X))) -> mark(s(s(dbl(X))))
     active(dbls(nil())) -> mark(nil())
     active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     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))))
     mark(dbl(X)) -> active(dbl(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(dbls(X)) -> active(dbls(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
     mark(from(X)) -> active(from(X))
     dbl(mark(X)) -> dbl(X)
     dbl(active(X)) -> dbl(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     dbls(mark(X)) -> dbls(X)
     dbls(active(X)) -> dbls(X)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
     indx(mark(X1),X2) -> indx(X1,X2)
     indx(X1,mark(X2)) -> indx(X1,X2)
     indx(active(X1),X2) -> indx(X1,X2)
     indx(X1,active(X2)) -> indx(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(cons#) = 1
     problem:
      DPs:
       cons#(mark(X1),X2) -> cons#(X1,X2)
       cons#(active(X1),X2) -> cons#(X1,X2)
      TRS:
       active(dbl(0())) -> mark(0())
       active(dbl(s(X))) -> mark(s(s(dbl(X))))
       active(dbls(nil())) -> mark(nil())
       active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
       active(sel(0(),cons(X,Y))) -> mark(X)
       active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
       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))))
       mark(dbl(X)) -> active(dbl(mark(X)))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(dbls(X)) -> active(dbls(mark(X)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
       mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
       mark(from(X)) -> active(from(X))
       dbl(mark(X)) -> dbl(X)
       dbl(active(X)) -> dbl(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       dbls(mark(X)) -> dbls(X)
       dbls(active(X)) -> dbls(X)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       sel(mark(X1),X2) -> sel(X1,X2)
       sel(X1,mark(X2)) -> sel(X1,X2)
       sel(active(X1),X2) -> sel(X1,X2)
       sel(X1,active(X2)) -> sel(X1,X2)
       indx(mark(X1),X2) -> indx(X1,X2)
       indx(X1,mark(X2)) -> indx(X1,X2)
       indx(active(X1),X2) -> indx(X1,X2)
       indx(X1,active(X2)) -> indx(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Subterm Criterion Processor:
      simple projection:
       pi(cons#) = 0
      problem:
       DPs:
        
       TRS:
        active(dbl(0())) -> mark(0())
        active(dbl(s(X))) -> mark(s(s(dbl(X))))
        active(dbls(nil())) -> mark(nil())
        active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
        active(sel(0(),cons(X,Y))) -> mark(X)
        active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
        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))))
        mark(dbl(X)) -> active(dbl(mark(X)))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(X))
        mark(dbls(X)) -> active(dbls(mark(X)))
        mark(nil()) -> active(nil())
        mark(cons(X1,X2)) -> active(cons(X1,X2))
        mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
        mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
        mark(from(X)) -> active(from(X))
        dbl(mark(X)) -> dbl(X)
        dbl(active(X)) -> dbl(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        dbls(mark(X)) -> dbls(X)
        dbls(active(X)) -> dbls(X)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        sel(mark(X1),X2) -> sel(X1,X2)
        sel(X1,mark(X2)) -> sel(X1,X2)
        sel(active(X1),X2) -> sel(X1,X2)
        sel(X1,active(X2)) -> sel(X1,X2)
        indx(mark(X1),X2) -> indx(X1,X2)
        indx(X1,mark(X2)) -> indx(X1,X2)
        indx(active(X1),X2) -> indx(X1,X2)
        indx(X1,active(X2)) -> indx(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
      Qed
    
    DPs:
     sel#(mark(X1),X2) -> sel#(X1,X2)
     sel#(X1,mark(X2)) -> sel#(X1,X2)
     sel#(active(X1),X2) -> sel#(X1,X2)
     sel#(X1,active(X2)) -> sel#(X1,X2)
    TRS:
     active(dbl(0())) -> mark(0())
     active(dbl(s(X))) -> mark(s(s(dbl(X))))
     active(dbls(nil())) -> mark(nil())
     active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     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))))
     mark(dbl(X)) -> active(dbl(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(dbls(X)) -> active(dbls(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
     mark(from(X)) -> active(from(X))
     dbl(mark(X)) -> dbl(X)
     dbl(active(X)) -> dbl(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     dbls(mark(X)) -> dbls(X)
     dbls(active(X)) -> dbls(X)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
     indx(mark(X1),X2) -> indx(X1,X2)
     indx(X1,mark(X2)) -> indx(X1,X2)
     indx(active(X1),X2) -> indx(X1,X2)
     indx(X1,active(X2)) -> indx(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(sel#) = 1
     problem:
      DPs:
       sel#(mark(X1),X2) -> sel#(X1,X2)
       sel#(active(X1),X2) -> sel#(X1,X2)
      TRS:
       active(dbl(0())) -> mark(0())
       active(dbl(s(X))) -> mark(s(s(dbl(X))))
       active(dbls(nil())) -> mark(nil())
       active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
       active(sel(0(),cons(X,Y))) -> mark(X)
       active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
       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))))
       mark(dbl(X)) -> active(dbl(mark(X)))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(dbls(X)) -> active(dbls(mark(X)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
       mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
       mark(from(X)) -> active(from(X))
       dbl(mark(X)) -> dbl(X)
       dbl(active(X)) -> dbl(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       dbls(mark(X)) -> dbls(X)
       dbls(active(X)) -> dbls(X)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       sel(mark(X1),X2) -> sel(X1,X2)
       sel(X1,mark(X2)) -> sel(X1,X2)
       sel(active(X1),X2) -> sel(X1,X2)
       sel(X1,active(X2)) -> sel(X1,X2)
       indx(mark(X1),X2) -> indx(X1,X2)
       indx(X1,mark(X2)) -> indx(X1,X2)
       indx(active(X1),X2) -> indx(X1,X2)
       indx(X1,active(X2)) -> indx(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Subterm Criterion Processor:
      simple projection:
       pi(sel#) = 0
      problem:
       DPs:
        
       TRS:
        active(dbl(0())) -> mark(0())
        active(dbl(s(X))) -> mark(s(s(dbl(X))))
        active(dbls(nil())) -> mark(nil())
        active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
        active(sel(0(),cons(X,Y))) -> mark(X)
        active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
        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))))
        mark(dbl(X)) -> active(dbl(mark(X)))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(X))
        mark(dbls(X)) -> active(dbls(mark(X)))
        mark(nil()) -> active(nil())
        mark(cons(X1,X2)) -> active(cons(X1,X2))
        mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
        mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
        mark(from(X)) -> active(from(X))
        dbl(mark(X)) -> dbl(X)
        dbl(active(X)) -> dbl(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        dbls(mark(X)) -> dbls(X)
        dbls(active(X)) -> dbls(X)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        sel(mark(X1),X2) -> sel(X1,X2)
        sel(X1,mark(X2)) -> sel(X1,X2)
        sel(active(X1),X2) -> sel(X1,X2)
        sel(X1,active(X2)) -> sel(X1,X2)
        indx(mark(X1),X2) -> indx(X1,X2)
        indx(X1,mark(X2)) -> indx(X1,X2)
        indx(active(X1),X2) -> indx(X1,X2)
        indx(X1,active(X2)) -> indx(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
      Qed
    
    DPs:
     indx#(mark(X1),X2) -> indx#(X1,X2)
     indx#(X1,mark(X2)) -> indx#(X1,X2)
     indx#(active(X1),X2) -> indx#(X1,X2)
     indx#(X1,active(X2)) -> indx#(X1,X2)
    TRS:
     active(dbl(0())) -> mark(0())
     active(dbl(s(X))) -> mark(s(s(dbl(X))))
     active(dbls(nil())) -> mark(nil())
     active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     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))))
     mark(dbl(X)) -> active(dbl(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(dbls(X)) -> active(dbls(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
     mark(from(X)) -> active(from(X))
     dbl(mark(X)) -> dbl(X)
     dbl(active(X)) -> dbl(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     dbls(mark(X)) -> dbls(X)
     dbls(active(X)) -> dbls(X)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
     indx(mark(X1),X2) -> indx(X1,X2)
     indx(X1,mark(X2)) -> indx(X1,X2)
     indx(active(X1),X2) -> indx(X1,X2)
     indx(X1,active(X2)) -> indx(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(indx#) = 1
     problem:
      DPs:
       indx#(mark(X1),X2) -> indx#(X1,X2)
       indx#(active(X1),X2) -> indx#(X1,X2)
      TRS:
       active(dbl(0())) -> mark(0())
       active(dbl(s(X))) -> mark(s(s(dbl(X))))
       active(dbls(nil())) -> mark(nil())
       active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
       active(sel(0(),cons(X,Y))) -> mark(X)
       active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
       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))))
       mark(dbl(X)) -> active(dbl(mark(X)))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(dbls(X)) -> active(dbls(mark(X)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
       mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
       mark(from(X)) -> active(from(X))
       dbl(mark(X)) -> dbl(X)
       dbl(active(X)) -> dbl(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       dbls(mark(X)) -> dbls(X)
       dbls(active(X)) -> dbls(X)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       sel(mark(X1),X2) -> sel(X1,X2)
       sel(X1,mark(X2)) -> sel(X1,X2)
       sel(active(X1),X2) -> sel(X1,X2)
       sel(X1,active(X2)) -> sel(X1,X2)
       indx(mark(X1),X2) -> indx(X1,X2)
       indx(X1,mark(X2)) -> indx(X1,X2)
       indx(active(X1),X2) -> indx(X1,X2)
       indx(X1,active(X2)) -> indx(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Subterm Criterion Processor:
      simple projection:
       pi(indx#) = 0
      problem:
       DPs:
        
       TRS:
        active(dbl(0())) -> mark(0())
        active(dbl(s(X))) -> mark(s(s(dbl(X))))
        active(dbls(nil())) -> mark(nil())
        active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
        active(sel(0(),cons(X,Y))) -> mark(X)
        active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
        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))))
        mark(dbl(X)) -> active(dbl(mark(X)))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(X))
        mark(dbls(X)) -> active(dbls(mark(X)))
        mark(nil()) -> active(nil())
        mark(cons(X1,X2)) -> active(cons(X1,X2))
        mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
        mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
        mark(from(X)) -> active(from(X))
        dbl(mark(X)) -> dbl(X)
        dbl(active(X)) -> dbl(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        dbls(mark(X)) -> dbls(X)
        dbls(active(X)) -> dbls(X)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        sel(mark(X1),X2) -> sel(X1,X2)
        sel(X1,mark(X2)) -> sel(X1,X2)
        sel(active(X1),X2) -> sel(X1,X2)
        sel(X1,active(X2)) -> sel(X1,X2)
        indx(mark(X1),X2) -> indx(X1,X2)
        indx(X1,mark(X2)) -> indx(X1,X2)
        indx(active(X1),X2) -> indx(X1,X2)
        indx(X1,active(X2)) -> indx(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
      Qed
    
    DPs:
     from#(mark(X)) -> from#(X)
     from#(active(X)) -> from#(X)
    TRS:
     active(dbl(0())) -> mark(0())
     active(dbl(s(X))) -> mark(s(s(dbl(X))))
     active(dbls(nil())) -> mark(nil())
     active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     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))))
     mark(dbl(X)) -> active(dbl(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(dbls(X)) -> active(dbls(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
     mark(from(X)) -> active(from(X))
     dbl(mark(X)) -> dbl(X)
     dbl(active(X)) -> dbl(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     dbls(mark(X)) -> dbls(X)
     dbls(active(X)) -> dbls(X)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
     indx(mark(X1),X2) -> indx(X1,X2)
     indx(X1,mark(X2)) -> indx(X1,X2)
     indx(active(X1),X2) -> indx(X1,X2)
     indx(X1,active(X2)) -> indx(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(from#) = 0
     problem:
      DPs:
       
      TRS:
       active(dbl(0())) -> mark(0())
       active(dbl(s(X))) -> mark(s(s(dbl(X))))
       active(dbls(nil())) -> mark(nil())
       active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
       active(sel(0(),cons(X,Y))) -> mark(X)
       active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
       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))))
       mark(dbl(X)) -> active(dbl(mark(X)))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(dbls(X)) -> active(dbls(mark(X)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
       mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
       mark(from(X)) -> active(from(X))
       dbl(mark(X)) -> dbl(X)
       dbl(active(X)) -> dbl(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       dbls(mark(X)) -> dbls(X)
       dbls(active(X)) -> dbls(X)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       sel(mark(X1),X2) -> sel(X1,X2)
       sel(X1,mark(X2)) -> sel(X1,X2)
       sel(active(X1),X2) -> sel(X1,X2)
       sel(X1,active(X2)) -> sel(X1,X2)
       indx(mark(X1),X2) -> indx(X1,X2)
       indx(X1,mark(X2)) -> indx(X1,X2)
       indx(active(X1),X2) -> indx(X1,X2)
       indx(X1,active(X2)) -> indx(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Qed