MAYBE

Problem:
 active(nats()) -> mark(adx(zeros()))
 active(zeros()) -> mark(cons(0(),zeros()))
 active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
 active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
 active(hd(cons(X,Y))) -> mark(X)
 active(tl(cons(X,Y))) -> mark(Y)
 mark(nats()) -> active(nats())
 mark(adx(X)) -> active(adx(mark(X)))
 mark(zeros()) -> active(zeros())
 mark(cons(X1,X2)) -> active(cons(X1,X2))
 mark(0()) -> active(0())
 mark(incr(X)) -> active(incr(mark(X)))
 mark(s(X)) -> active(s(X))
 mark(hd(X)) -> active(hd(mark(X)))
 mark(tl(X)) -> active(tl(mark(X)))
 adx(mark(X)) -> adx(X)
 adx(active(X)) -> adx(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)
 incr(mark(X)) -> incr(X)
 incr(active(X)) -> incr(X)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 hd(mark(X)) -> hd(X)
 hd(active(X)) -> hd(X)
 tl(mark(X)) -> tl(X)
 tl(active(X)) -> tl(X)

Proof:
 DP Processor:
  DPs:
   active#(nats()) -> adx#(zeros())
   active#(nats()) -> mark#(adx(zeros()))
   active#(zeros()) -> cons#(0(),zeros())
   active#(zeros()) -> mark#(cons(0(),zeros()))
   active#(incr(cons(X,Y))) -> incr#(Y)
   active#(incr(cons(X,Y))) -> s#(X)
   active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y))
   active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y)))
   active#(adx(cons(X,Y))) -> adx#(Y)
   active#(adx(cons(X,Y))) -> cons#(X,adx(Y))
   active#(adx(cons(X,Y))) -> incr#(cons(X,adx(Y)))
   active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y))))
   active#(hd(cons(X,Y))) -> mark#(X)
   active#(tl(cons(X,Y))) -> mark#(Y)
   mark#(nats()) -> active#(nats())
   mark#(adx(X)) -> mark#(X)
   mark#(adx(X)) -> adx#(mark(X))
   mark#(adx(X)) -> active#(adx(mark(X)))
   mark#(zeros()) -> active#(zeros())
   mark#(cons(X1,X2)) -> active#(cons(X1,X2))
   mark#(0()) -> active#(0())
   mark#(incr(X)) -> mark#(X)
   mark#(incr(X)) -> incr#(mark(X))
   mark#(incr(X)) -> active#(incr(mark(X)))
   mark#(s(X)) -> active#(s(X))
   mark#(hd(X)) -> mark#(X)
   mark#(hd(X)) -> hd#(mark(X))
   mark#(hd(X)) -> active#(hd(mark(X)))
   mark#(tl(X)) -> mark#(X)
   mark#(tl(X)) -> tl#(mark(X))
   mark#(tl(X)) -> active#(tl(mark(X)))
   adx#(mark(X)) -> adx#(X)
   adx#(active(X)) -> adx#(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)
   incr#(mark(X)) -> incr#(X)
   incr#(active(X)) -> incr#(X)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   hd#(mark(X)) -> hd#(X)
   hd#(active(X)) -> hd#(X)
   tl#(mark(X)) -> tl#(X)
   tl#(active(X)) -> tl#(X)
  TRS:
   active(nats()) -> mark(adx(zeros()))
   active(zeros()) -> mark(cons(0(),zeros()))
   active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
   active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
   active(hd(cons(X,Y))) -> mark(X)
   active(tl(cons(X,Y))) -> mark(Y)
   mark(nats()) -> active(nats())
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros()) -> active(zeros())
   mark(cons(X1,X2)) -> active(cons(X1,X2))
   mark(0()) -> active(0())
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   incr(mark(X)) -> incr(X)
   incr(active(X)) -> incr(X)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)
  EDG Processor:
   DPs:
    active#(nats()) -> adx#(zeros())
    active#(nats()) -> mark#(adx(zeros()))
    active#(zeros()) -> cons#(0(),zeros())
    active#(zeros()) -> mark#(cons(0(),zeros()))
    active#(incr(cons(X,Y))) -> incr#(Y)
    active#(incr(cons(X,Y))) -> s#(X)
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y))
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y)))
    active#(adx(cons(X,Y))) -> adx#(Y)
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y))
    active#(adx(cons(X,Y))) -> incr#(cons(X,adx(Y)))
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y))))
    active#(hd(cons(X,Y))) -> mark#(X)
    active#(tl(cons(X,Y))) -> mark#(Y)
    mark#(nats()) -> active#(nats())
    mark#(adx(X)) -> mark#(X)
    mark#(adx(X)) -> adx#(mark(X))
    mark#(adx(X)) -> active#(adx(mark(X)))
    mark#(zeros()) -> active#(zeros())
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(0()) -> active#(0())
    mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> incr#(mark(X))
    mark#(incr(X)) -> active#(incr(mark(X)))
    mark#(s(X)) -> active#(s(X))
    mark#(hd(X)) -> mark#(X)
    mark#(hd(X)) -> hd#(mark(X))
    mark#(hd(X)) -> active#(hd(mark(X)))
    mark#(tl(X)) -> mark#(X)
    mark#(tl(X)) -> tl#(mark(X))
    mark#(tl(X)) -> active#(tl(mark(X)))
    adx#(mark(X)) -> adx#(X)
    adx#(active(X)) -> adx#(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)
    incr#(mark(X)) -> incr#(X)
    incr#(active(X)) -> incr#(X)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    hd#(mark(X)) -> hd#(X)
    hd#(active(X)) -> hd#(X)
    tl#(mark(X)) -> tl#(X)
    tl#(active(X)) -> tl#(X)
   TRS:
    active(nats()) -> mark(adx(zeros()))
    active(zeros()) -> mark(cons(0(),zeros()))
    active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
    active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
    active(hd(cons(X,Y))) -> mark(X)
    active(tl(cons(X,Y))) -> mark(Y)
    mark(nats()) -> active(nats())
    mark(adx(X)) -> active(adx(mark(X)))
    mark(zeros()) -> active(zeros())
    mark(cons(X1,X2)) -> active(cons(X1,X2))
    mark(0()) -> active(0())
    mark(incr(X)) -> active(incr(mark(X)))
    mark(s(X)) -> active(s(X))
    mark(hd(X)) -> active(hd(mark(X)))
    mark(tl(X)) -> active(tl(mark(X)))
    adx(mark(X)) -> adx(X)
    adx(active(X)) -> adx(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)
    incr(mark(X)) -> incr(X)
    incr(active(X)) -> incr(X)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    hd(mark(X)) -> hd(X)
    hd(active(X)) -> hd(X)
    tl(mark(X)) -> tl(X)
    tl(active(X)) -> tl(X)
   graph:
    tl#(mark(X)) -> tl#(X) -> tl#(mark(X)) -> tl#(X)
    tl#(mark(X)) -> tl#(X) -> tl#(active(X)) -> tl#(X)
    tl#(active(X)) -> tl#(X) -> tl#(mark(X)) -> tl#(X)
    tl#(active(X)) -> tl#(X) -> tl#(active(X)) -> tl#(X)
    hd#(mark(X)) -> hd#(X) -> hd#(mark(X)) -> hd#(X)
    hd#(mark(X)) -> hd#(X) -> hd#(active(X)) -> hd#(X)
    hd#(active(X)) -> hd#(X) -> hd#(mark(X)) -> hd#(X)
    hd#(active(X)) -> hd#(X) -> hd#(active(X)) -> hd#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    incr#(mark(X)) -> incr#(X) -> incr#(mark(X)) -> incr#(X)
    incr#(mark(X)) -> incr#(X) -> incr#(active(X)) -> incr#(X)
    incr#(active(X)) -> incr#(X) -> incr#(mark(X)) -> incr#(X)
    incr#(active(X)) -> incr#(X) -> incr#(active(X)) -> incr#(X)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(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#(active(X1),X2) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(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#(active(X1),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#(mark(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#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(mark(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#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    mark#(tl(X)) -> tl#(mark(X)) -> tl#(mark(X)) -> tl#(X)
    mark#(tl(X)) -> tl#(mark(X)) -> tl#(active(X)) -> tl#(X)
    mark#(tl(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
    mark#(tl(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(tl(X)) -> mark#(X) -> mark#(adx(X)) -> adx#(mark(X))
    mark#(tl(X)) -> mark#(X) -> mark#(adx(X)) -> active#(adx(mark(X)))
    mark#(tl(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(tl(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(tl(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(tl(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(tl(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
    mark#(tl(X)) -> mark#(X) -> mark#(incr(X)) -> active#(incr(mark(X)))
    mark#(tl(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
    mark#(tl(X)) -> mark#(X) -> mark#(hd(X)) -> mark#(X)
    mark#(tl(X)) -> mark#(X) -> mark#(hd(X)) -> hd#(mark(X))
    mark#(tl(X)) -> mark#(X) -> mark#(hd(X)) -> active#(hd(mark(X)))
    mark#(tl(X)) -> mark#(X) -> mark#(tl(X)) -> mark#(X)
    mark#(tl(X)) -> mark#(X) -> mark#(tl(X)) -> tl#(mark(X))
    mark#(tl(X)) -> mark#(X) ->
    mark#(tl(X)) -> active#(tl(mark(X)))
    mark#(tl(X)) -> active#(tl(mark(X))) ->
    active#(incr(cons(X,Y))) -> incr#(Y)
    mark#(tl(X)) -> active#(tl(mark(X))) ->
    active#(incr(cons(X,Y))) -> s#(X)
    mark#(tl(X)) -> active#(tl(mark(X))) ->
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y))
    mark#(tl(X)) -> active#(tl(mark(X))) ->
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y)))
    mark#(tl(X)) -> active#(tl(mark(X))) ->
    active#(adx(cons(X,Y))) -> adx#(Y)
    mark#(tl(X)) -> active#(tl(mark(X))) ->
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y))
    mark#(tl(X)) -> active#(tl(mark(X))) ->
    active#(adx(cons(X,Y))) -> incr#(cons(X,adx(Y)))
    mark#(tl(X)) -> active#(tl(mark(X))) ->
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y))))
    mark#(tl(X)) -> active#(tl(mark(X))) ->
    active#(hd(cons(X,Y))) -> mark#(X)
    mark#(tl(X)) -> active#(tl(mark(X))) ->
    active#(tl(cons(X,Y))) -> mark#(Y)
    mark#(hd(X)) -> hd#(mark(X)) -> hd#(mark(X)) -> hd#(X)
    mark#(hd(X)) -> hd#(mark(X)) -> hd#(active(X)) -> hd#(X)
    mark#(hd(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
    mark#(hd(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(hd(X)) -> mark#(X) -> mark#(adx(X)) -> adx#(mark(X))
    mark#(hd(X)) -> mark#(X) -> mark#(adx(X)) -> active#(adx(mark(X)))
    mark#(hd(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(hd(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(hd(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(hd(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(hd(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
    mark#(hd(X)) -> mark#(X) -> mark#(incr(X)) -> active#(incr(mark(X)))
    mark#(hd(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
    mark#(hd(X)) -> mark#(X) -> mark#(hd(X)) -> mark#(X)
    mark#(hd(X)) -> mark#(X) -> mark#(hd(X)) -> hd#(mark(X))
    mark#(hd(X)) -> mark#(X) -> mark#(hd(X)) -> active#(hd(mark(X)))
    mark#(hd(X)) -> mark#(X) -> mark#(tl(X)) -> mark#(X)
    mark#(hd(X)) -> mark#(X) -> mark#(tl(X)) -> tl#(mark(X))
    mark#(hd(X)) -> mark#(X) ->
    mark#(tl(X)) -> active#(tl(mark(X)))
    mark#(hd(X)) -> active#(hd(mark(X))) ->
    active#(incr(cons(X,Y))) -> incr#(Y)
    mark#(hd(X)) -> active#(hd(mark(X))) ->
    active#(incr(cons(X,Y))) -> s#(X)
    mark#(hd(X)) -> active#(hd(mark(X))) ->
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y))
    mark#(hd(X)) -> active#(hd(mark(X))) ->
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y)))
    mark#(hd(X)) -> active#(hd(mark(X))) ->
    active#(adx(cons(X,Y))) -> adx#(Y)
    mark#(hd(X)) -> active#(hd(mark(X))) ->
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y))
    mark#(hd(X)) -> active#(hd(mark(X))) ->
    active#(adx(cons(X,Y))) -> incr#(cons(X,adx(Y)))
    mark#(hd(X)) -> active#(hd(mark(X))) ->
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y))))
    mark#(hd(X)) -> active#(hd(mark(X))) ->
    active#(hd(cons(X,Y))) -> mark#(X)
    mark#(hd(X)) -> active#(hd(mark(X))) ->
    active#(tl(cons(X,Y))) -> mark#(Y)
    mark#(s(X)) -> active#(s(X)) ->
    active#(incr(cons(X,Y))) -> incr#(Y)
    mark#(s(X)) -> active#(s(X)) -> active#(incr(cons(X,Y))) -> s#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y))
    mark#(s(X)) -> active#(s(X)) ->
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y)))
    mark#(s(X)) -> active#(s(X)) -> active#(adx(cons(X,Y))) -> adx#(Y)
    mark#(s(X)) -> active#(s(X)) ->
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y))
    mark#(s(X)) -> active#(s(X)) ->
    active#(adx(cons(X,Y))) -> incr#(cons(X,adx(Y)))
    mark#(s(X)) -> active#(s(X)) ->
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y))))
    mark#(s(X)) -> active#(s(X)) -> active#(hd(cons(X,Y))) -> mark#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(tl(cons(X,Y))) -> mark#(Y)
    mark#(incr(X)) -> incr#(mark(X)) -> incr#(mark(X)) -> incr#(X)
    mark#(incr(X)) -> incr#(mark(X)) -> incr#(active(X)) -> incr#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
    mark#(incr(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(adx(X)) -> adx#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(adx(X)) -> active#(adx(mark(X)))
    mark#(incr(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(incr(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(incr(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
    mark#(incr(X)) -> mark#(X) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
    mark#(incr(X)) -> mark#(X) -> mark#(hd(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(hd(X)) -> hd#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(hd(X)) -> active#(hd(mark(X)))
    mark#(incr(X)) -> mark#(X) -> mark#(tl(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(tl(X)) -> tl#(mark(X))
    mark#(incr(X)) -> mark#(X) ->
    mark#(tl(X)) -> active#(tl(mark(X)))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(incr(cons(X,Y))) -> incr#(Y)
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(incr(cons(X,Y))) -> s#(X)
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y)))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(adx(cons(X,Y))) -> adx#(Y)
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(adx(cons(X,Y))) -> incr#(cons(X,adx(Y)))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y))))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(hd(cons(X,Y))) -> mark#(X)
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(tl(cons(X,Y))) -> mark#(Y)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(incr(cons(X,Y))) -> incr#(Y)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(incr(cons(X,Y))) -> s#(X)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y)))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(adx(cons(X,Y))) -> adx#(Y)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(adx(cons(X,Y))) -> incr#(cons(X,adx(Y)))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y))))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(hd(cons(X,Y))) -> mark#(X)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(tl(cons(X,Y))) -> mark#(Y)
    mark#(adx(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
    mark#(adx(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(adx(X)) -> adx#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(adx(X)) -> active#(adx(mark(X)))
    mark#(adx(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(adx(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(adx(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(adx(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(incr(X)) -> active#(incr(mark(X)))
    mark#(adx(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
    mark#(adx(X)) -> mark#(X) -> mark#(hd(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(hd(X)) -> hd#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(hd(X)) -> active#(hd(mark(X)))
    mark#(adx(X)) -> mark#(X) -> mark#(tl(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(tl(X)) -> tl#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(tl(X)) -> active#(tl(mark(X)))
    mark#(adx(X)) -> adx#(mark(X)) -> adx#(mark(X)) -> adx#(X)
    mark#(adx(X)) -> adx#(mark(X)) ->
    adx#(active(X)) -> adx#(X)
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(incr(cons(X,Y))) -> incr#(Y)
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(incr(cons(X,Y))) -> s#(X)
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y)))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(adx(cons(X,Y))) -> adx#(Y)
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(adx(cons(X,Y))) -> incr#(cons(X,adx(Y)))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y))))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(hd(cons(X,Y))) -> mark#(X)
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(tl(cons(X,Y))) -> mark#(Y)
    mark#(zeros()) -> active#(zeros()) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(zeros()) -> active#(zeros()) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(nats()) -> active#(nats()) ->
    active#(nats()) -> adx#(zeros())
    mark#(nats()) -> active#(nats()) ->
    active#(nats()) -> mark#(adx(zeros()))
    adx#(mark(X)) -> adx#(X) -> adx#(mark(X)) -> adx#(X)
    adx#(mark(X)) -> adx#(X) -> adx#(active(X)) -> adx#(X)
    adx#(active(X)) -> adx#(X) -> adx#(mark(X)) -> adx#(X)
    adx#(active(X)) -> adx#(X) -> adx#(active(X)) -> adx#(X)
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(nats()) -> active#(nats())
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(adx(X)) -> mark#(X)
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(adx(X)) -> adx#(mark(X))
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(adx(X)) -> active#(adx(mark(X)))
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(zeros()) -> active#(zeros())
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(0()) -> active#(0())
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(incr(X)) -> mark#(X)
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(incr(X)) -> incr#(mark(X))
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(s(X)) -> active#(s(X))
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(hd(X)) -> mark#(X)
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(hd(X)) -> hd#(mark(X))
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(hd(X)) -> active#(hd(mark(X)))
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(tl(X)) -> mark#(X)
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(tl(X)) -> tl#(mark(X))
    active#(tl(cons(X,Y))) -> mark#(Y) ->
    mark#(tl(X)) -> active#(tl(mark(X)))
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(nats()) -> active#(nats())
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(adx(X)) -> mark#(X)
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(adx(X)) -> adx#(mark(X))
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(adx(X)) -> active#(adx(mark(X)))
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(zeros()) -> active#(zeros())
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(0()) -> active#(0())
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(incr(X)) -> mark#(X)
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(incr(X)) -> incr#(mark(X))
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(s(X)) -> active#(s(X))
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(hd(X)) -> mark#(X)
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(hd(X)) -> hd#(mark(X))
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(hd(X)) -> active#(hd(mark(X)))
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(tl(X)) -> mark#(X)
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(tl(X)) -> tl#(mark(X))
    active#(hd(cons(X,Y))) -> mark#(X) ->
    mark#(tl(X)) -> active#(tl(mark(X)))
    active#(incr(cons(X,Y))) -> s#(X) -> s#(mark(X)) -> s#(X)
    active#(incr(cons(X,Y))) -> s#(X) -> s#(active(X)) -> s#(X)
    active#(incr(cons(X,Y))) -> incr#(Y) ->
    incr#(mark(X)) -> incr#(X)
    active#(incr(cons(X,Y))) -> incr#(Y) ->
    incr#(active(X)) -> incr#(X)
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y)) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y)) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(incr(cons(X,Y))) -> cons#(s(X),incr(Y)) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(adx(X)) -> mark#(X)
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(adx(X)) -> adx#(mark(X))
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(adx(X)) -> active#(adx(mark(X)))
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(incr(X)) -> mark#(X)
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(incr(X)) -> incr#(mark(X))
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(s(X)) -> active#(s(X))
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(hd(X)) -> mark#(X)
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(hd(X)) -> hd#(mark(X))
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(hd(X)) -> active#(hd(mark(X)))
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(tl(X)) -> mark#(X)
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(tl(X)) -> tl#(mark(X))
    active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y))) ->
    mark#(tl(X)) -> active#(tl(mark(X)))
    active#(adx(cons(X,Y))) -> incr#(cons(X,adx(Y))) ->
    incr#(mark(X)) -> incr#(X)
    active#(adx(cons(X,Y))) -> incr#(cons(X,adx(Y))) ->
    incr#(active(X)) -> incr#(X)
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y)) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y)) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(adx(cons(X,Y))) -> cons#(X,adx(Y)) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(adx(X)) -> mark#(X)
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(adx(X)) -> adx#(mark(X))
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(adx(X)) -> active#(adx(mark(X)))
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(incr(X)) -> mark#(X)
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(incr(X)) -> incr#(mark(X))
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(s(X)) -> active#(s(X))
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(hd(X)) -> mark#(X)
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(hd(X)) -> hd#(mark(X))
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(hd(X)) -> active#(hd(mark(X)))
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(tl(X)) -> mark#(X)
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(tl(X)) -> tl#(mark(X))
    active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y)))) ->
    mark#(tl(X)) -> active#(tl(mark(X)))
    active#(adx(cons(X,Y))) -> adx#(Y) ->
    adx#(mark(X)) -> adx#(X)
    active#(adx(cons(X,Y))) -> adx#(Y) ->
    adx#(active(X)) -> adx#(X)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(nats()) -> mark#(adx(zeros())) ->
    mark#(adx(X)) -> mark#(X)
    active#(nats()) -> mark#(adx(zeros())) ->
    mark#(adx(X)) -> adx#(mark(X))
    active#(nats()) -> mark#(adx(zeros())) -> mark#(adx(X)) -> active#(adx(mark(X)))
   SCC Processor:
    #sccs: 7
    #rules: 32
    #arcs: 258/2025
    DPs:
     mark#(tl(X)) -> mark#(X)
     mark#(tl(X)) -> active#(tl(mark(X)))
     active#(tl(cons(X,Y))) -> mark#(Y)
     mark#(hd(X)) -> active#(hd(mark(X)))
     active#(hd(cons(X,Y))) -> mark#(X)
     mark#(hd(X)) -> mark#(X)
     mark#(s(X)) -> active#(s(X))
     active#(adx(cons(X,Y))) -> mark#(incr(cons(X,adx(Y))))
     mark#(incr(X)) -> active#(incr(mark(X)))
     active#(incr(cons(X,Y))) -> mark#(cons(s(X),incr(Y)))
     mark#(incr(X)) -> mark#(X)
     mark#(cons(X1,X2)) -> active#(cons(X1,X2))
     mark#(zeros()) -> active#(zeros())
     active#(zeros()) -> mark#(cons(0(),zeros()))
     mark#(adx(X)) -> active#(adx(mark(X)))
     mark#(adx(X)) -> mark#(X)
     mark#(nats()) -> active#(nats())
     active#(nats()) -> mark#(adx(zeros()))
    TRS:
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
     active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
     active(hd(cons(X,Y))) -> mark(X)
     active(tl(cons(X,Y))) -> mark(Y)
     mark(nats()) -> active(nats())
     mark(adx(X)) -> active(adx(mark(X)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(0()) -> active(0())
     mark(incr(X)) -> active(incr(mark(X)))
     mark(s(X)) -> active(s(X))
     mark(hd(X)) -> active(hd(mark(X)))
     mark(tl(X)) -> active(tl(mark(X)))
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(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)
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     hd(mark(X)) -> hd(X)
     hd(active(X)) -> hd(X)
     tl(mark(X)) -> tl(X)
     tl(active(X)) -> tl(X)
    Open
    
    DPs:
     adx#(active(X)) -> adx#(X)
     adx#(mark(X)) -> adx#(X)
    TRS:
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
     active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
     active(hd(cons(X,Y))) -> mark(X)
     active(tl(cons(X,Y))) -> mark(Y)
     mark(nats()) -> active(nats())
     mark(adx(X)) -> active(adx(mark(X)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(0()) -> active(0())
     mark(incr(X)) -> active(incr(mark(X)))
     mark(s(X)) -> active(s(X))
     mark(hd(X)) -> active(hd(mark(X)))
     mark(tl(X)) -> active(tl(mark(X)))
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(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)
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     hd(mark(X)) -> hd(X)
     hd(active(X)) -> hd(X)
     tl(mark(X)) -> tl(X)
     tl(active(X)) -> tl(X)
    Open
    
    DPs:
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(X1,active(X2)) -> cons#(X1,X2)
     cons#(active(X1),X2) -> cons#(X1,X2)
     cons#(X1,mark(X2)) -> cons#(X1,X2)
    TRS:
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
     active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
     active(hd(cons(X,Y))) -> mark(X)
     active(tl(cons(X,Y))) -> mark(Y)
     mark(nats()) -> active(nats())
     mark(adx(X)) -> active(adx(mark(X)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(0()) -> active(0())
     mark(incr(X)) -> active(incr(mark(X)))
     mark(s(X)) -> active(s(X))
     mark(hd(X)) -> active(hd(mark(X)))
     mark(tl(X)) -> active(tl(mark(X)))
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(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)
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     hd(mark(X)) -> hd(X)
     hd(active(X)) -> hd(X)
     tl(mark(X)) -> tl(X)
     tl(active(X)) -> tl(X)
    Open
    
    DPs:
     incr#(mark(X)) -> incr#(X)
     incr#(active(X)) -> incr#(X)
    TRS:
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
     active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
     active(hd(cons(X,Y))) -> mark(X)
     active(tl(cons(X,Y))) -> mark(Y)
     mark(nats()) -> active(nats())
     mark(adx(X)) -> active(adx(mark(X)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(0()) -> active(0())
     mark(incr(X)) -> active(incr(mark(X)))
     mark(s(X)) -> active(s(X))
     mark(hd(X)) -> active(hd(mark(X)))
     mark(tl(X)) -> active(tl(mark(X)))
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(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)
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     hd(mark(X)) -> hd(X)
     hd(active(X)) -> hd(X)
     tl(mark(X)) -> tl(X)
     tl(active(X)) -> tl(X)
    Open
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
     active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
     active(hd(cons(X,Y))) -> mark(X)
     active(tl(cons(X,Y))) -> mark(Y)
     mark(nats()) -> active(nats())
     mark(adx(X)) -> active(adx(mark(X)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(0()) -> active(0())
     mark(incr(X)) -> active(incr(mark(X)))
     mark(s(X)) -> active(s(X))
     mark(hd(X)) -> active(hd(mark(X)))
     mark(tl(X)) -> active(tl(mark(X)))
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(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)
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     hd(mark(X)) -> hd(X)
     hd(active(X)) -> hd(X)
     tl(mark(X)) -> tl(X)
     tl(active(X)) -> tl(X)
    Open
    
    DPs:
     hd#(mark(X)) -> hd#(X)
     hd#(active(X)) -> hd#(X)
    TRS:
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
     active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
     active(hd(cons(X,Y))) -> mark(X)
     active(tl(cons(X,Y))) -> mark(Y)
     mark(nats()) -> active(nats())
     mark(adx(X)) -> active(adx(mark(X)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(0()) -> active(0())
     mark(incr(X)) -> active(incr(mark(X)))
     mark(s(X)) -> active(s(X))
     mark(hd(X)) -> active(hd(mark(X)))
     mark(tl(X)) -> active(tl(mark(X)))
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(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)
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     hd(mark(X)) -> hd(X)
     hd(active(X)) -> hd(X)
     tl(mark(X)) -> tl(X)
     tl(active(X)) -> tl(X)
    Open
    
    DPs:
     tl#(mark(X)) -> tl#(X)
     tl#(active(X)) -> tl#(X)
    TRS:
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
     active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
     active(hd(cons(X,Y))) -> mark(X)
     active(tl(cons(X,Y))) -> mark(Y)
     mark(nats()) -> active(nats())
     mark(adx(X)) -> active(adx(mark(X)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(0()) -> active(0())
     mark(incr(X)) -> active(incr(mark(X)))
     mark(s(X)) -> active(s(X))
     mark(hd(X)) -> active(hd(mark(X)))
     mark(tl(X)) -> active(tl(mark(X)))
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(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)
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     hd(mark(X)) -> hd(X)
     hd(active(X)) -> hd(X)
     tl(mark(X)) -> tl(X)
     tl(active(X)) -> tl(X)
    Open