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#(active(X1),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))) -> cons#(X,adx(L)) -> cons#(X1,mark(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#(X1,mark(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))) -> 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: 350/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