MAYBE

Problem:
 active(incr(nil())) -> mark(nil())
 active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
 active(adx(nil())) -> mark(nil())
 active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
 active(nats()) -> mark(adx(zeros()))
 active(zeros()) -> mark(cons(0(),zeros()))
 active(head(cons(X,L))) -> mark(X)
 active(tail(cons(X,L))) -> mark(L)
 mark(incr(X)) -> active(incr(mark(X)))
 mark(nil()) -> active(nil())
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(s(X)) -> active(s(mark(X)))
 mark(adx(X)) -> active(adx(mark(X)))
 mark(nats()) -> active(nats())
 mark(zeros()) -> active(zeros())
 mark(0()) -> active(0())
 mark(head(X)) -> active(head(mark(X)))
 mark(tail(X)) -> active(tail(mark(X)))
 incr(mark(X)) -> incr(X)
 incr(active(X)) -> incr(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)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 adx(mark(X)) -> adx(X)
 adx(active(X)) -> adx(X)
 head(mark(X)) -> head(X)
 head(active(X)) -> head(X)
 tail(mark(X)) -> tail(X)
 tail(active(X)) -> tail(X)

Proof:
 DP Processor:
  DPs:
   active#(incr(nil())) -> mark#(nil())
   active#(incr(cons(X,L))) -> incr#(L)
   active#(incr(cons(X,L))) -> s#(X)
   active#(incr(cons(X,L))) -> cons#(s(X),incr(L))
   active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L)))
   active#(adx(nil())) -> mark#(nil())
   active#(adx(cons(X,L))) -> adx#(L)
   active#(adx(cons(X,L))) -> cons#(X,adx(L))
   active#(adx(cons(X,L))) -> incr#(cons(X,adx(L)))
   active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L))))
   active#(nats()) -> adx#(zeros())
   active#(nats()) -> mark#(adx(zeros()))
   active#(zeros()) -> cons#(0(),zeros())
   active#(zeros()) -> mark#(cons(0(),zeros()))
   active#(head(cons(X,L))) -> mark#(X)
   active#(tail(cons(X,L))) -> mark#(L)
   mark#(incr(X)) -> mark#(X)
   mark#(incr(X)) -> incr#(mark(X))
   mark#(incr(X)) -> active#(incr(mark(X)))
   mark#(nil()) -> active#(nil())
   mark#(cons(X1,X2)) -> mark#(X1)
   mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
   mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
   mark#(s(X)) -> mark#(X)
   mark#(s(X)) -> s#(mark(X))
   mark#(s(X)) -> active#(s(mark(X)))
   mark#(adx(X)) -> mark#(X)
   mark#(adx(X)) -> adx#(mark(X))
   mark#(adx(X)) -> active#(adx(mark(X)))
   mark#(nats()) -> active#(nats())
   mark#(zeros()) -> active#(zeros())
   mark#(0()) -> active#(0())
   mark#(head(X)) -> mark#(X)
   mark#(head(X)) -> head#(mark(X))
   mark#(head(X)) -> active#(head(mark(X)))
   mark#(tail(X)) -> mark#(X)
   mark#(tail(X)) -> tail#(mark(X))
   mark#(tail(X)) -> active#(tail(mark(X)))
   incr#(mark(X)) -> incr#(X)
   incr#(active(X)) -> incr#(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)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   adx#(mark(X)) -> adx#(X)
   adx#(active(X)) -> adx#(X)
   head#(mark(X)) -> head#(X)
   head#(active(X)) -> head#(X)
   tail#(mark(X)) -> tail#(X)
   tail#(active(X)) -> tail#(X)
  TRS:
   active(incr(nil())) -> mark(nil())
   active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
   active(adx(nil())) -> mark(nil())
   active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
   active(nats()) -> mark(adx(zeros()))
   active(zeros()) -> mark(cons(0(),zeros()))
   active(head(cons(X,L))) -> mark(X)
   active(tail(cons(X,L))) -> mark(L)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(nil()) -> active(nil())
   mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
   mark(s(X)) -> active(s(mark(X)))
   mark(adx(X)) -> active(adx(mark(X)))
   mark(nats()) -> active(nats())
   mark(zeros()) -> active(zeros())
   mark(0()) -> active(0())
   mark(head(X)) -> active(head(mark(X)))
   mark(tail(X)) -> active(tail(mark(X)))
   incr(mark(X)) -> incr(X)
   incr(active(X)) -> incr(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)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(X)
   head(mark(X)) -> head(X)
   head(active(X)) -> head(X)
   tail(mark(X)) -> tail(X)
   tail(active(X)) -> tail(X)
  EDG Processor:
   DPs:
    active#(incr(nil())) -> mark#(nil())
    active#(incr(cons(X,L))) -> incr#(L)
    active#(incr(cons(X,L))) -> s#(X)
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L)))
    active#(adx(nil())) -> mark#(nil())
    active#(adx(cons(X,L))) -> adx#(L)
    active#(adx(cons(X,L))) -> cons#(X,adx(L))
    active#(adx(cons(X,L))) -> incr#(cons(X,adx(L)))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L))))
    active#(nats()) -> adx#(zeros())
    active#(nats()) -> mark#(adx(zeros()))
    active#(zeros()) -> cons#(0(),zeros())
    active#(zeros()) -> mark#(cons(0(),zeros()))
    active#(head(cons(X,L))) -> mark#(X)
    active#(tail(cons(X,L))) -> mark#(L)
    mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> incr#(mark(X))
    mark#(incr(X)) -> active#(incr(mark(X)))
    mark#(nil()) -> active#(nil())
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(adx(X)) -> mark#(X)
    mark#(adx(X)) -> adx#(mark(X))
    mark#(adx(X)) -> active#(adx(mark(X)))
    mark#(nats()) -> active#(nats())
    mark#(zeros()) -> active#(zeros())
    mark#(0()) -> active#(0())
    mark#(head(X)) -> mark#(X)
    mark#(head(X)) -> head#(mark(X))
    mark#(head(X)) -> active#(head(mark(X)))
    mark#(tail(X)) -> mark#(X)
    mark#(tail(X)) -> tail#(mark(X))
    mark#(tail(X)) -> active#(tail(mark(X)))
    incr#(mark(X)) -> incr#(X)
    incr#(active(X)) -> incr#(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)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    adx#(mark(X)) -> adx#(X)
    adx#(active(X)) -> adx#(X)
    head#(mark(X)) -> head#(X)
    head#(active(X)) -> head#(X)
    tail#(mark(X)) -> tail#(X)
    tail#(active(X)) -> tail#(X)
   TRS:
    active(incr(nil())) -> mark(nil())
    active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
    active(adx(nil())) -> mark(nil())
    active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
    active(nats()) -> mark(adx(zeros()))
    active(zeros()) -> mark(cons(0(),zeros()))
    active(head(cons(X,L))) -> mark(X)
    active(tail(cons(X,L))) -> mark(L)
    mark(incr(X)) -> active(incr(mark(X)))
    mark(nil()) -> active(nil())
    mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    mark(s(X)) -> active(s(mark(X)))
    mark(adx(X)) -> active(adx(mark(X)))
    mark(nats()) -> active(nats())
    mark(zeros()) -> active(zeros())
    mark(0()) -> active(0())
    mark(head(X)) -> active(head(mark(X)))
    mark(tail(X)) -> active(tail(mark(X)))
    incr(mark(X)) -> incr(X)
    incr(active(X)) -> incr(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)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    adx(mark(X)) -> adx(X)
    adx(active(X)) -> adx(X)
    head(mark(X)) -> head(X)
    head(active(X)) -> head(X)
    tail(mark(X)) -> tail(X)
    tail(active(X)) -> tail(X)
   graph:
    tail#(mark(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
    tail#(mark(X)) -> tail#(X) -> tail#(active(X)) -> tail#(X)
    tail#(active(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
    tail#(active(X)) -> tail#(X) -> tail#(active(X)) -> tail#(X)
    head#(mark(X)) -> head#(X) -> head#(mark(X)) -> head#(X)
    head#(mark(X)) -> head#(X) -> head#(active(X)) -> head#(X)
    head#(active(X)) -> head#(X) -> head#(mark(X)) -> head#(X)
    head#(active(X)) -> head#(X) -> head#(active(X)) -> head#(X)
    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)
    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)
    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)
    mark#(tail(X)) -> tail#(mark(X)) -> tail#(mark(X)) -> tail#(X)
    mark#(tail(X)) -> tail#(mark(X)) -> tail#(active(X)) -> tail#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
    mark#(tail(X)) -> mark#(X) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    mark#(tail(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(tail(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(tail(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(tail(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(adx(X)) -> adx#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(adx(X)) -> active#(adx(mark(X)))
    mark#(tail(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
    mark#(tail(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(tail(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(tail(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(head(X)) -> head#(mark(X))
    mark#(tail(X)) -> mark#(X) ->
    mark#(head(X)) -> active#(head(mark(X)))
    mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
    mark#(tail(X)) -> mark#(X) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(incr(nil())) -> mark#(nil())
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(incr(cons(X,L))) -> incr#(L)
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(incr(cons(X,L))) -> s#(X)
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L))
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L)))
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(adx(nil())) -> mark#(nil())
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(adx(cons(X,L))) -> adx#(L)
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(adx(cons(X,L))) -> cons#(X,adx(L))
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(adx(cons(X,L))) -> incr#(cons(X,adx(L)))
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L))))
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(head(cons(X,L))) -> mark#(X)
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(tail(cons(X,L))) -> mark#(L)
    mark#(head(X)) -> head#(mark(X)) -> head#(mark(X)) -> head#(X)
    mark#(head(X)) -> head#(mark(X)) -> head#(active(X)) -> head#(X)
    mark#(head(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
    mark#(head(X)) -> mark#(X) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    mark#(head(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(head(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(head(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(head(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(head(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(adx(X)) -> adx#(mark(X))
    mark#(head(X)) -> mark#(X) -> mark#(adx(X)) -> active#(adx(mark(X)))
    mark#(head(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
    mark#(head(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(head(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(head(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(head(X)) -> head#(mark(X))
    mark#(head(X)) -> mark#(X) ->
    mark#(head(X)) -> active#(head(mark(X)))
    mark#(head(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
    mark#(head(X)) -> mark#(X) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(incr(nil())) -> mark#(nil())
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(incr(cons(X,L))) -> incr#(L)
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(incr(cons(X,L))) -> s#(X)
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L))
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L)))
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(adx(nil())) -> mark#(nil())
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(adx(cons(X,L))) -> adx#(L)
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(adx(cons(X,L))) -> cons#(X,adx(L))
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(adx(cons(X,L))) -> incr#(cons(X,adx(L)))
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L))))
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(head(cons(X,L))) -> mark#(X)
    mark#(head(X)) -> active#(head(mark(X))) ->
    active#(tail(cons(X,L))) -> mark#(L)
    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()))
    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)) -> 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#(nil()) -> active#(nil())
    mark#(adx(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(adx(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(adx(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(adx(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    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#(nats()) -> active#(nats())
    mark#(adx(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(adx(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(adx(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(head(X)) -> head#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(head(X)) -> active#(head(mark(X)))
    mark#(adx(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
    mark#(adx(X)) -> mark#(X) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(incr(nil())) -> mark#(nil())
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(incr(cons(X,L))) -> incr#(L)
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(incr(cons(X,L))) -> s#(X)
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L)))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(adx(nil())) -> mark#(nil())
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(adx(cons(X,L))) -> adx#(L)
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(adx(cons(X,L))) -> cons#(X,adx(L))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(adx(cons(X,L))) -> incr#(cons(X,adx(L)))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L))))
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(head(cons(X,L))) -> mark#(X)
    mark#(adx(X)) -> active#(adx(mark(X))) ->
    active#(tail(cons(X,L))) -> mark#(L)
    mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
    mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> active#(incr(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(adx(X)) -> adx#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(adx(X)) -> active#(adx(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
    mark#(s(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> head#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> active#(head(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
    mark#(s(X)) -> mark#(X) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(incr(nil())) -> mark#(nil())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(incr(cons(X,L))) -> incr#(L)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(incr(cons(X,L))) -> s#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(adx(nil())) -> mark#(nil())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(adx(cons(X,L))) -> adx#(L)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(adx(cons(X,L))) -> cons#(X,adx(L))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(adx(cons(X,L))) -> incr#(cons(X,adx(L)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L))))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(head(cons(X,L))) -> mark#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(tail(cons(X,L))) -> mark#(L)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(incr(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(incr(X)) -> incr#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(nil()) -> active#(nil())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(adx(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(adx(X)) -> adx#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(adx(X)) -> active#(adx(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(nats()) -> active#(nats())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(zeros()) -> active#(zeros())
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(head(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(head(X)) -> head#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(head(X)) -> active#(head(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(tail(X)) -> tail#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(incr(nil())) -> mark#(nil())
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(incr(cons(X,L))) -> incr#(L)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(incr(cons(X,L))) -> s#(X)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(adx(nil())) -> mark#(nil())
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(adx(cons(X,L))) -> adx#(L)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(adx(cons(X,L))) -> cons#(X,adx(L))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(adx(cons(X,L))) -> incr#(cons(X,adx(L)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L))))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(head(cons(X,L))) -> mark#(X)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(tail(cons(X,L))) -> mark#(L)
    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#(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#(nil()) -> active#(nil())
    mark#(incr(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(incr(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(incr(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    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#(nats()) -> active#(nats())
    mark#(incr(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(incr(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(incr(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(head(X)) -> head#(mark(X))
    mark#(incr(X)) -> mark#(X) ->
    mark#(head(X)) -> active#(head(mark(X)))
    mark#(incr(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
    mark#(incr(X)) -> mark#(X) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(incr(nil())) -> mark#(nil())
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(incr(cons(X,L))) -> incr#(L)
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(incr(cons(X,L))) -> s#(X)
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L)))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(adx(nil())) -> mark#(nil())
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(adx(cons(X,L))) -> adx#(L)
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(adx(cons(X,L))) -> cons#(X,adx(L))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(adx(cons(X,L))) -> incr#(cons(X,adx(L)))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L))))
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(head(cons(X,L))) -> mark#(X)
    mark#(incr(X)) -> active#(incr(mark(X))) ->
    active#(tail(cons(X,L))) -> mark#(L)
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(incr(X)) -> mark#(X)
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(incr(X)) -> incr#(mark(X))
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(nil()) -> active#(nil())
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(s(X)) -> mark#(X)
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(s(X)) -> s#(mark(X))
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(adx(X)) -> mark#(X)
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(adx(X)) -> adx#(mark(X))
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(adx(X)) -> active#(adx(mark(X)))
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(nats()) -> active#(nats())
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(zeros()) -> active#(zeros())
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(0()) -> active#(0())
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(head(X)) -> mark#(X)
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(head(X)) -> head#(mark(X))
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(head(X)) -> active#(head(mark(X)))
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(tail(X)) -> mark#(X)
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(tail(X)) -> tail#(mark(X))
    active#(tail(cons(X,L))) -> mark#(L) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(incr(X)) -> mark#(X)
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(incr(X)) -> incr#(mark(X))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(nil()) -> active#(nil())
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(s(X)) -> mark#(X)
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(s(X)) -> s#(mark(X))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(adx(X)) -> mark#(X)
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(adx(X)) -> adx#(mark(X))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(adx(X)) -> active#(adx(mark(X)))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(nats()) -> active#(nats())
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(zeros()) -> active#(zeros())
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(0()) -> active#(0())
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(head(X)) -> mark#(X)
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(head(X)) -> head#(mark(X))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(head(X)) -> active#(head(mark(X)))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(tail(X)) -> mark#(X)
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(tail(X)) -> tail#(mark(X))
    active#(head(cons(X,L))) -> mark#(X) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(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)))
    active#(adx(cons(X,L))) -> adx#(L) ->
    adx#(mark(X)) -> adx#(X)
    active#(adx(cons(X,L))) -> adx#(L) ->
    adx#(active(X)) -> adx#(X)
    active#(adx(cons(X,L))) -> cons#(X,adx(L)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(adx(cons(X,L))) -> cons#(X,adx(L)) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(adx(cons(X,L))) -> cons#(X,adx(L)) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(adx(cons(X,L))) -> cons#(X,adx(L)) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(adx(cons(X,L))) -> incr#(cons(X,adx(L))) ->
    incr#(mark(X)) -> incr#(X)
    active#(adx(cons(X,L))) -> incr#(cons(X,adx(L))) ->
    incr#(active(X)) -> incr#(X)
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(incr(X)) -> mark#(X)
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(incr(X)) -> incr#(mark(X))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(s(X)) -> mark#(X)
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(adx(X)) -> mark#(X)
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(adx(X)) -> adx#(mark(X))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(adx(X)) -> active#(adx(mark(X)))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(head(X)) -> mark#(X)
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(head(X)) -> head#(mark(X))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(head(X)) -> active#(head(mark(X)))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(tail(X)) -> mark#(X)
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(tail(X)) -> tail#(mark(X))
    active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L)))) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    active#(adx(nil())) -> mark#(nil()) ->
    mark#(nil()) -> active#(nil())
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L)) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L)) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(incr(cons(X,L))) -> cons#(s(X),incr(L)) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(incr(cons(X,L))) -> s#(X) -> s#(mark(X)) -> s#(X)
    active#(incr(cons(X,L))) -> s#(X) -> s#(active(X)) -> s#(X)
    active#(incr(cons(X,L))) -> incr#(L) ->
    incr#(mark(X)) -> incr#(X)
    active#(incr(cons(X,L))) -> incr#(L) ->
    incr#(active(X)) -> incr#(X)
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(incr(X)) -> mark#(X)
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(incr(X)) -> incr#(mark(X))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(incr(X)) -> active#(incr(mark(X)))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(s(X)) -> mark#(X)
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(adx(X)) -> mark#(X)
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(adx(X)) -> adx#(mark(X))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(adx(X)) -> active#(adx(mark(X)))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(head(X)) -> mark#(X)
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(head(X)) -> head#(mark(X))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(head(X)) -> active#(head(mark(X)))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(tail(X)) -> mark#(X)
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(tail(X)) -> tail#(mark(X))
    active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L))) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    active#(incr(nil())) -> mark#(nil()) -> mark#(nil()) -> active#(nil())
   SCC Processor:
    #sccs: 7
    #rules: 34
    #arcs: 362/2704
    DPs:
     mark#(tail(X)) -> mark#(X)
     mark#(tail(X)) -> active#(tail(mark(X)))
     active#(tail(cons(X,L))) -> mark#(L)
     mark#(head(X)) -> active#(head(mark(X)))
     active#(head(cons(X,L))) -> mark#(X)
     mark#(head(X)) -> mark#(X)
     mark#(zeros()) -> active#(zeros())
     active#(zeros()) -> mark#(cons(0(),zeros()))
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     active#(adx(cons(X,L))) -> mark#(incr(cons(X,adx(L))))
     mark#(adx(X)) -> active#(adx(mark(X)))
     active#(incr(cons(X,L))) -> mark#(cons(s(X),incr(L)))
     mark#(adx(X)) -> mark#(X)
     mark#(nats()) -> active#(nats())
     active#(nats()) -> mark#(adx(zeros()))
     mark#(s(X)) -> active#(s(mark(X)))
     mark#(s(X)) -> mark#(X)
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(incr(X)) -> active#(incr(mark(X)))
     mark#(incr(X)) -> mark#(X)
    TRS:
     active(incr(nil())) -> mark(nil())
     active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
     active(adx(nil())) -> mark(nil())
     active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(head(cons(X,L))) -> mark(X)
     active(tail(cons(X,L))) -> mark(L)
     mark(incr(X)) -> active(incr(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(s(X)) -> active(s(mark(X)))
     mark(adx(X)) -> active(adx(mark(X)))
     mark(nats()) -> active(nats())
     mark(zeros()) -> active(zeros())
     mark(0()) -> active(0())
     mark(head(X)) -> active(head(mark(X)))
     mark(tail(X)) -> active(tail(mark(X)))
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(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)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(X)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
    Open
    
    DPs:
     incr#(mark(X)) -> incr#(X)
     incr#(active(X)) -> incr#(X)
    TRS:
     active(incr(nil())) -> mark(nil())
     active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
     active(adx(nil())) -> mark(nil())
     active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(head(cons(X,L))) -> mark(X)
     active(tail(cons(X,L))) -> mark(L)
     mark(incr(X)) -> active(incr(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(s(X)) -> active(s(mark(X)))
     mark(adx(X)) -> active(adx(mark(X)))
     mark(nats()) -> active(nats())
     mark(zeros()) -> active(zeros())
     mark(0()) -> active(0())
     mark(head(X)) -> active(head(mark(X)))
     mark(tail(X)) -> active(tail(mark(X)))
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(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)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(X)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
    Open
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(incr(nil())) -> mark(nil())
     active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
     active(adx(nil())) -> mark(nil())
     active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(head(cons(X,L))) -> mark(X)
     active(tail(cons(X,L))) -> mark(L)
     mark(incr(X)) -> active(incr(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(s(X)) -> active(s(mark(X)))
     mark(adx(X)) -> active(adx(mark(X)))
     mark(nats()) -> active(nats())
     mark(zeros()) -> active(zeros())
     mark(0()) -> active(0())
     mark(head(X)) -> active(head(mark(X)))
     mark(tail(X)) -> active(tail(mark(X)))
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(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)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(X)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(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(incr(nil())) -> mark(nil())
     active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
     active(adx(nil())) -> mark(nil())
     active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(head(cons(X,L))) -> mark(X)
     active(tail(cons(X,L))) -> mark(L)
     mark(incr(X)) -> active(incr(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(s(X)) -> active(s(mark(X)))
     mark(adx(X)) -> active(adx(mark(X)))
     mark(nats()) -> active(nats())
     mark(zeros()) -> active(zeros())
     mark(0()) -> active(0())
     mark(head(X)) -> active(head(mark(X)))
     mark(tail(X)) -> active(tail(mark(X)))
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(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)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(X)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
    Open
    
    DPs:
     adx#(mark(X)) -> adx#(X)
     adx#(active(X)) -> adx#(X)
    TRS:
     active(incr(nil())) -> mark(nil())
     active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
     active(adx(nil())) -> mark(nil())
     active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(head(cons(X,L))) -> mark(X)
     active(tail(cons(X,L))) -> mark(L)
     mark(incr(X)) -> active(incr(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(s(X)) -> active(s(mark(X)))
     mark(adx(X)) -> active(adx(mark(X)))
     mark(nats()) -> active(nats())
     mark(zeros()) -> active(zeros())
     mark(0()) -> active(0())
     mark(head(X)) -> active(head(mark(X)))
     mark(tail(X)) -> active(tail(mark(X)))
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(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)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(X)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
    Open
    
    DPs:
     head#(mark(X)) -> head#(X)
     head#(active(X)) -> head#(X)
    TRS:
     active(incr(nil())) -> mark(nil())
     active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
     active(adx(nil())) -> mark(nil())
     active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(head(cons(X,L))) -> mark(X)
     active(tail(cons(X,L))) -> mark(L)
     mark(incr(X)) -> active(incr(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(s(X)) -> active(s(mark(X)))
     mark(adx(X)) -> active(adx(mark(X)))
     mark(nats()) -> active(nats())
     mark(zeros()) -> active(zeros())
     mark(0()) -> active(0())
     mark(head(X)) -> active(head(mark(X)))
     mark(tail(X)) -> active(tail(mark(X)))
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(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)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(X)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
    Open
    
    DPs:
     tail#(mark(X)) -> tail#(X)
     tail#(active(X)) -> tail#(X)
    TRS:
     active(incr(nil())) -> mark(nil())
     active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
     active(adx(nil())) -> mark(nil())
     active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
     active(nats()) -> mark(adx(zeros()))
     active(zeros()) -> mark(cons(0(),zeros()))
     active(head(cons(X,L))) -> mark(X)
     active(tail(cons(X,L))) -> mark(L)
     mark(incr(X)) -> active(incr(mark(X)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(s(X)) -> active(s(mark(X)))
     mark(adx(X)) -> active(adx(mark(X)))
     mark(nats()) -> active(nats())
     mark(zeros()) -> active(zeros())
     mark(0()) -> active(0())
     mark(head(X)) -> active(head(mark(X)))
     mark(tail(X)) -> active(tail(mark(X)))
     incr(mark(X)) -> incr(X)
     incr(active(X)) -> incr(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)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     adx(mark(X)) -> adx(X)
     adx(active(X)) -> adx(X)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
    Open