MAYBE TRS: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} DP: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(from(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X)), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)), mark#(s(X)) -> active#(s(mark(X))), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(head(X)) -> head#(mark(X)), mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X))), mark#(2nd(X)) -> 2nd#(mark(X)), mark#(nil()) -> active#(nil()), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2)), mark#(0()) -> active#(0()), mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2), from#(mark(X)) -> from#(X), from#(active(X)) -> from#(X), s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(from(X)) -> cons#(X, from(s(X))), active#(from(X)) -> from#(s(X)), active#(from(X)) -> s#(X), active#(head(cons(X, XS))) -> mark#(X), active#(2nd(cons(X, XS))) -> mark#(head(XS)), active#(2nd(cons(X, XS))) -> head#(XS), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)), active#(take(s(N), cons(X, XS))) -> take#(N, XS), active#(take(0(), XS)) -> mark#(nil()), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), active#(sel(0(), cons(X, XS))) -> mark#(X), head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X), 2nd#(mark(X)) -> 2nd#(X), 2nd#(active(X)) -> 2nd#(X), take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2), take#(active(X1), X2) -> take#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} EDG: { (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(take(0(), XS)) -> mark#(nil())) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(take(s(N), cons(X, XS))) -> take#(N, XS)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(2nd(cons(X, XS))) -> head#(XS)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(from(X)) -> s#(X)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(from(X)) -> from#(s(X))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (active#(take(0(), XS)) -> mark#(nil()), mark#(nil()) -> active#(nil())) (mark#(s(X)) -> active#(s(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(s(X)) -> active#(s(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(s(X)) -> active#(s(mark(X))), active#(take(0(), XS)) -> mark#(nil())) (mark#(s(X)) -> active#(s(mark(X))), active#(take(s(N), cons(X, XS))) -> take#(N, XS)) (mark#(s(X)) -> active#(s(mark(X))), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS))) (mark#(s(X)) -> active#(s(mark(X))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(s(X)) -> active#(s(mark(X))), active#(2nd(cons(X, XS))) -> head#(XS)) (mark#(s(X)) -> active#(s(mark(X))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(s(X)) -> active#(s(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> s#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> from#(s(X))) (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(take(0(), XS)) -> mark#(nil())) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(take(s(N), cons(X, XS))) -> take#(N, XS)) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(2nd(cons(X, XS))) -> head#(XS)) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(from(X)) -> s#(X)) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(from(X)) -> from#(s(X))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(sel(X1, X2)) -> mark#(X2)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(sel(X1, X2)) -> mark#(X1)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(take(X1, X2)) -> mark#(X2)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(take(X1, X2)) -> mark#(X1)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(2nd(X)) -> 2nd#(mark(X))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(2nd(X)) -> mark#(X)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(head(X)) -> head#(mark(X))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(head(X)) -> active#(head(mark(X)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(head(X)) -> mark#(X)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(s(X)) -> active#(s(mark(X)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(s(X)) -> s#(mark(X))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(s(X)) -> mark#(X)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(from(X)) -> active#(from(mark(X)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(from(X)) -> from#(mark(X))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(from(X)) -> mark#(X)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(cons(X1, X2)) -> mark#(X1)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(active(X1), 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, active(X2)) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), 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, active(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (take#(X1, active(X2)) -> take#(X1, X2), take#(active(X1), X2) -> take#(X1, X2)) (take#(X1, active(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)) (take#(X1, active(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)) (take#(X1, active(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (take#(active(X1), X2) -> take#(X1, X2), take#(active(X1), X2) -> take#(X1, X2)) (take#(active(X1), X2) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)) (take#(active(X1), X2) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)) (take#(active(X1), X2) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(active(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)) (sel#(active(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(active(X1), X2) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(active(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(active(X1), X2) -> sel#(X1, X2)) (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(mark(X1), X2) -> sel#(X1, X2)) (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(X1, active(X2)) -> sel#(X1, X2)) (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(X1, mark(X2)) -> sel#(X1, X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nil()) -> active#(nil())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> 2nd#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(2nd(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#(head(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(sel(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(nil()) -> active#(nil())) (mark#(sel(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> 2nd#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(head(X)) -> head#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (active#(take(s(N), cons(X, XS))) -> take#(N, XS), take#(active(X1), X2) -> take#(X1, X2)) (active#(take(s(N), cons(X, XS))) -> take#(N, XS), take#(mark(X1), X2) -> take#(X1, X2)) (active#(take(s(N), cons(X, XS))) -> take#(N, XS), take#(X1, active(X2)) -> take#(X1, X2)) (active#(take(s(N), cons(X, XS))) -> take#(N, XS), take#(X1, mark(X2)) -> take#(X1, X2)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(take(0(), XS)) -> mark#(nil())) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(take(s(N), cons(X, XS))) -> take#(N, XS)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(2nd(cons(X, XS))) -> head#(XS)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(head(cons(X, XS))) -> mark#(X)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> s#(X)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> from#(s(X))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> mark#(cons(X, from(s(X))))) (active#(from(X)) -> cons#(X, from(s(X))), cons#(active(X1), X2) -> cons#(X1, X2)) (active#(from(X)) -> cons#(X, from(s(X))), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(from(X)) -> cons#(X, from(s(X))), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(from(X)) -> cons#(X, from(s(X))), cons#(X1, mark(X2)) -> cons#(X1, X2)) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(nil()) -> active#(nil())) (mark#(s(X)) -> mark#(X), mark#(2nd(X)) -> 2nd#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(2nd(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#(head(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(2nd(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(2nd(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(2nd(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(2nd(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(2nd(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(2nd(X)) -> mark#(X), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(2nd(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(2nd(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(2nd(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(2nd(X)) -> mark#(X), mark#(nil()) -> active#(nil())) (mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> 2nd#(mark(X))) (mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (mark#(2nd(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(2nd(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(2nd(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(2nd(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(2nd(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(2nd(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(2nd(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(2nd(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (mark#(2nd(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(2nd(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(2nd(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(2nd(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (from#(active(X)) -> from#(X), from#(active(X)) -> from#(X)) (from#(active(X)) -> from#(X), from#(mark(X)) -> from#(X)) (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X)) (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(head(cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (active#(head(cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (active#(head(cons(X, XS))) -> mark#(X), mark#(0()) -> active#(0())) (active#(head(cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (active#(head(cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (active#(head(cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (active#(head(cons(X, XS))) -> mark#(X), mark#(nil()) -> active#(nil())) (active#(head(cons(X, XS))) -> mark#(X), mark#(2nd(X)) -> 2nd#(mark(X))) (active#(head(cons(X, XS))) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (active#(head(cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (active#(head(cons(X, XS))) -> mark#(X), mark#(from(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(head(cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(head(cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X)) (head#(mark(X)) -> head#(X), head#(mark(X)) -> head#(X)) (2nd#(mark(X)) -> 2nd#(X), 2nd#(active(X)) -> 2nd#(X)) (2nd#(mark(X)) -> 2nd#(X), 2nd#(mark(X)) -> 2nd#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(take(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(nil()) -> active#(nil())) (mark#(take(X1, X2)) -> mark#(X2), mark#(2nd(X)) -> 2nd#(mark(X))) (mark#(take(X1, X2)) -> mark#(X2), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(2nd(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(head(X)) -> head#(mark(X))) (mark#(take(X1, X2)) -> mark#(X2), mark#(head(X)) -> active#(head(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(head(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X))) (mark#(take(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(from(X)) -> from#(mark(X))) (mark#(take(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(take(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(sel(X1, X2)) -> mark#(X2)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(sel(X1, X2)) -> mark#(X1)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(take(X1, X2)) -> mark#(X2)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(take(X1, X2)) -> mark#(X1)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(2nd(X)) -> 2nd#(mark(X))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(2nd(X)) -> mark#(X)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(head(X)) -> head#(mark(X))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(head(X)) -> active#(head(mark(X)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(head(X)) -> mark#(X)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(s(X)) -> active#(s(mark(X)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(s(X)) -> s#(mark(X))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(s(X)) -> mark#(X)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(from(X)) -> active#(from(mark(X)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(from(X)) -> from#(mark(X))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(from(X)) -> mark#(X)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> s#(mark(X)), s#(active(X)) -> s#(X)) (mark#(s(X)) -> s#(mark(X)), s#(mark(X)) -> s#(X)) (mark#(2nd(X)) -> 2nd#(mark(X)), 2nd#(active(X)) -> 2nd#(X)) (mark#(2nd(X)) -> 2nd#(mark(X)), 2nd#(mark(X)) -> 2nd#(X)) (active#(from(X)) -> from#(s(X)), from#(mark(X)) -> from#(X)) (active#(from(X)) -> from#(s(X)), from#(active(X)) -> from#(X)) (mark#(head(X)) -> head#(mark(X)), head#(mark(X)) -> head#(X)) (mark#(head(X)) -> head#(mark(X)), head#(active(X)) -> head#(X)) (mark#(from(X)) -> from#(mark(X)), from#(mark(X)) -> from#(X)) (mark#(from(X)) -> from#(mark(X)), from#(active(X)) -> from#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(from(X)) -> from#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(head(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(head(X)) -> active#(head(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(head(X)) -> head#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(2nd(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(2nd(X)) -> 2nd#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(nil()) -> active#(nil())) (mark#(sel(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (2nd#(active(X)) -> 2nd#(X), 2nd#(mark(X)) -> 2nd#(X)) (2nd#(active(X)) -> 2nd#(X), 2nd#(active(X)) -> 2nd#(X)) (head#(active(X)) -> head#(X), head#(mark(X)) -> head#(X)) (head#(active(X)) -> head#(X), head#(active(X)) -> head#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(from(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(2nd(X)) -> 2nd#(mark(X))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(nil()) -> active#(nil())) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(0()) -> active#(0())) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(from(X)) -> s#(X), s#(mark(X)) -> s#(X)) (active#(from(X)) -> s#(X), s#(active(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)) (from#(mark(X)) -> from#(X), from#(mark(X)) -> from#(X)) (from#(mark(X)) -> from#(X), from#(active(X)) -> from#(X)) (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#(from(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (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#(head(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(2nd(X)) -> 2nd#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(nil()) -> active#(nil())) (mark#(head(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(head(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(head(X)) -> mark#(X), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(head(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(head(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(head(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(head(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(2nd(X)) -> 2nd#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(nil()) -> active#(nil())) (mark#(from(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(from(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(from(X)) -> mark#(X), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(from(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(from(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(from(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(from(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(from(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(from(X)) -> from#(mark(X))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(from(X)) -> active#(from(mark(X)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> s#(mark(X))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> active#(s(mark(X)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(head(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(head(X)) -> active#(head(mark(X)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(head(X)) -> head#(mark(X))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(2nd(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(2nd(X)) -> 2nd#(mark(X))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(take(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(take(X1, X2)) -> mark#(X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(X1, mark(X2)) -> sel#(X1, X2)) (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(X1, active(X2)) -> sel#(X1, X2)) (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(mark(X1), X2) -> sel#(X1, X2)) (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(active(X1), X2) -> sel#(X1, X2)) (active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)), cons#(X1, mark(X2)) -> cons#(X1, X2)) (active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)), cons#(active(X1), X2) -> cons#(X1, X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(take(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X))) (mark#(take(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(take(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(head(X)) -> head#(mark(X))) (mark#(take(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> 2nd#(mark(X))) (mark#(take(X1, X2)) -> mark#(X1), mark#(nil()) -> active#(nil())) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(take(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(take(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(2nd(cons(X, XS))) -> head#(XS), head#(mark(X)) -> head#(X)) (active#(2nd(cons(X, XS))) -> head#(XS), head#(active(X)) -> head#(X)) (mark#(take(X1, X2)) -> take#(mark(X1), mark(X2)), take#(X1, mark(X2)) -> take#(X1, X2)) (mark#(take(X1, X2)) -> take#(mark(X1), mark(X2)), take#(X1, active(X2)) -> take#(X1, X2)) (mark#(take(X1, X2)) -> take#(mark(X1), mark(X2)), take#(mark(X1), X2) -> take#(X1, X2)) (mark#(take(X1, X2)) -> take#(mark(X1), mark(X2)), take#(active(X1), X2) -> take#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)) (take#(mark(X1), X2) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (take#(mark(X1), X2) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)) (take#(mark(X1), X2) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)) (take#(mark(X1), X2) -> take#(X1, X2), take#(active(X1), X2) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(active(X1), X2) -> take#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(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#(X1, active(X2)) -> cons#(X1, X2)) (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#(head(X)) -> active#(head(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(head(X)) -> active#(head(mark(X))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(head(X)) -> active#(head(mark(X))), active#(from(X)) -> from#(s(X))) (mark#(head(X)) -> active#(head(mark(X))), active#(from(X)) -> s#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(head(X)) -> active#(head(mark(X))), active#(2nd(cons(X, XS))) -> head#(XS)) (mark#(head(X)) -> active#(head(mark(X))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(head(X)) -> active#(head(mark(X))), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS))) (mark#(head(X)) -> active#(head(mark(X))), active#(take(s(N), cons(X, XS))) -> take#(N, XS)) (mark#(head(X)) -> active#(head(mark(X))), active#(take(0(), XS)) -> mark#(nil())) (mark#(head(X)) -> active#(head(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(head(X)) -> active#(head(mark(X))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(head(X)) -> active#(head(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> from#(s(X))) (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> s#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(from(X)) -> active#(from(mark(X))), active#(2nd(cons(X, XS))) -> head#(XS)) (mark#(from(X)) -> active#(from(mark(X))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(from(X)) -> active#(from(mark(X))), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS))) (mark#(from(X)) -> active#(from(mark(X))), active#(take(s(N), cons(X, XS))) -> take#(N, XS)) (mark#(from(X)) -> active#(from(mark(X))), active#(take(0(), XS)) -> mark#(nil())) (mark#(from(X)) -> active#(from(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(from(X)) -> active#(from(mark(X))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(from(X)) -> active#(from(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> from#(mark(X))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> active#(from(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> s#(mark(X))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> active#(s(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(head(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(head(X)) -> active#(head(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(head(X)) -> head#(mark(X))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(2nd(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(2nd(X)) -> 2nd#(mark(X))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(take(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(take(X1, X2)) -> mark#(X2)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sel(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sel(X1, X2)) -> mark#(X2)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(from(X)) -> from#(s(X))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(from(X)) -> s#(X)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(2nd(cons(X, XS))) -> head#(XS)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(s(N), cons(X, XS))) -> take#(N, XS)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(0(), XS)) -> mark#(nil())) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X)) } SCCS: Scc: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)} Scc: { take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2), take#(active(X1), X2) -> take#(X1, X2)} Scc: { 2nd#(mark(X)) -> 2nd#(X), 2nd#(active(X)) -> 2nd#(X)} Scc: { head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X)} Scc: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Scc: { from#(mark(X)) -> from#(X), from#(active(X)) -> from#(X)} Scc: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X))), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(head(cons(X, XS))) -> mark#(X), active#(2nd(cons(X, XS))) -> mark#(head(XS)), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(0(), cons(X, XS))) -> mark#(X)} SCC: Strict: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(sel#) = 0 Strict: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)} EDG: {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))} SCCS: Scc: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)} SCC: Strict: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(sel#) = 0 Strict: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)} EDG: {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))} SCCS: Scc: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)} SCC: Strict: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(sel#) = 1 Strict: {sel#(X1, active(X2)) -> sel#(X1, X2)} EDG: {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))} SCCS: Scc: {sel#(X1, active(X2)) -> sel#(X1, X2)} SCC: Strict: {sel#(X1, active(X2)) -> sel#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(sel#) = 1 Strict: {} Qed SCC: Strict: { take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2), take#(active(X1), X2) -> take#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(take#) = 0 Strict: { take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)} EDG: {(take#(X1, active(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)) (take#(X1, active(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)) (take#(X1, active(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (take#(mark(X1), X2) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (take#(mark(X1), X2) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)) (take#(mark(X1), X2) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2))} SCCS: Scc: { take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)} SCC: Strict: { take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(take#) = 0 Strict: { take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)} EDG: {(take#(X1, active(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)) (take#(X1, active(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2))} SCCS: Scc: { take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)} SCC: Strict: { take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(take#) = 1 Strict: {take#(X1, active(X2)) -> take#(X1, X2)} EDG: {(take#(X1, active(X2)) -> take#(X1, X2), take#(X1, active(X2)) -> take#(X1, X2))} SCCS: Scc: {take#(X1, active(X2)) -> take#(X1, X2)} SCC: Strict: {take#(X1, active(X2)) -> take#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(take#) = 1 Strict: {} Qed SCC: Strict: { 2nd#(mark(X)) -> 2nd#(X), 2nd#(active(X)) -> 2nd#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(2nd#) = 0 Strict: {2nd#(active(X)) -> 2nd#(X)} EDG: {(2nd#(active(X)) -> 2nd#(X), 2nd#(active(X)) -> 2nd#(X))} SCCS: Scc: {2nd#(active(X)) -> 2nd#(X)} SCC: Strict: {2nd#(active(X)) -> 2nd#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(2nd#) = 0 Strict: {} Qed SCC: Strict: { head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(head#) = 0 Strict: {head#(mark(X)) -> head#(X)} EDG: {(head#(mark(X)) -> head#(X), head#(mark(X)) -> head#(X))} SCCS: Scc: {head#(mark(X)) -> head#(X)} SCC: Strict: {head#(mark(X)) -> head#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(head#) = 0 Strict: {} Qed SCC: Strict: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(s#) = 0 Strict: {s#(active(X)) -> s#(X)} EDG: {(s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))} SCCS: Scc: {s#(active(X)) -> s#(X)} SCC: Strict: {s#(active(X)) -> s#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: { from#(mark(X)) -> from#(X), from#(active(X)) -> from#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(from#) = 0 Strict: {from#(active(X)) -> from#(X)} EDG: {(from#(active(X)) -> from#(X), from#(active(X)) -> from#(X))} SCCS: Scc: {from#(active(X)) -> from#(X)} SCC: Strict: {from#(active(X)) -> from#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(from#) = 0 Strict: {} Qed SCC: Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(cons#) = 0 Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)} EDG: {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(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#(X1, active(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#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))} SCCS: Scc: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)} SCC: Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(cons#) = 0 Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)} EDG: {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, active(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#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))} SCCS: Scc: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)} SCC: Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(cons#) = 1 Strict: {cons#(X1, active(X2)) -> cons#(X1, X2)} EDG: {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))} SCCS: Scc: {cons#(X1, active(X2)) -> cons#(X1, X2)} SCC: Strict: {cons#(X1, active(X2)) -> cons#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} SPSC: Simple Projection: pi(cons#) = 1 Strict: {} Qed SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X))), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(head(cons(X, XS))) -> mark#(X), active#(2nd(cons(X, XS))) -> mark#(head(XS)), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(0(), cons(X, XS))) -> mark#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} POLY: Argument Filtering: pi(sel) = [], pi(0) = [], pi(take) = [], pi(nil) = [], pi(2nd) = [], pi(head) = [], pi(active#) = 0, pi(active) = [], pi(s) = [], pi(from) = [], pi(cons) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [sel] = 1, [take] = 1, [cons] = 0, [2nd] = 1, [head] = 1, [s] = 0, [from] = 1 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X))), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(head(cons(X, XS))) -> mark#(X), active#(2nd(cons(X, XS))) -> mark#(head(XS)), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(0(), cons(X, XS))) -> mark#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} EDG: { (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(sel(X1, X2)) -> mark#(X2)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(sel(X1, X2)) -> mark#(X1)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(take(X1, X2)) -> mark#(X2)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(take(X1, X2)) -> mark#(X1)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(2nd(X)) -> mark#(X)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(head(X)) -> active#(head(mark(X)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(head(X)) -> mark#(X)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(s(X)) -> mark#(X)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(from(X)) -> active#(from(mark(X)))) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(from(X)) -> mark#(X)) (active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> active#(from(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(from(X)) -> active#(from(mark(X))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(from(X)) -> active#(from(mark(X))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(from(X)) -> active#(from(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(2nd(X)) -> active#(2nd(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(2nd(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(2nd(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(2nd(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(2nd(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(2nd(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(2nd(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (mark#(2nd(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(2nd(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(2nd(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(2nd(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(2nd(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(2nd(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(from(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(2nd(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(head(X)) -> active#(head(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(head(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sel(X1, X2)) -> mark#(X2)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sel(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(take(X1, X2)) -> mark#(X2)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(take(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(2nd(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(head(X)) -> active#(head(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(head(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> active#(from(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(head(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(head(X)) -> active#(head(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(2nd(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(head(cons(X, XS))) -> mark#(X), mark#(from(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (active#(head(cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (active#(head(cons(X, XS))) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (active#(head(cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (active#(head(cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(head(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(head(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(head(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(2nd(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(from(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(from(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(from(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(head(X)) -> active#(head(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(head(X)) -> active#(head(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(2nd(cons(X, XS))) -> mark#(head(XS))) (mark#(head(X)) -> active#(head(mark(X))), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS)))) (mark#(head(X)) -> active#(head(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(head(X)) -> active#(head(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(from(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(from(X)) -> active#(from(mark(X)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(head(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(head(X)) -> active#(head(mark(X)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(2nd(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(take(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(take(X1, X2)) -> mark#(X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(cons(X1, X2)) -> mark#(X1)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(from(X)) -> mark#(X)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(from(X)) -> active#(from(mark(X)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(s(X)) -> mark#(X)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(head(X)) -> mark#(X)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(head(X)) -> active#(head(mark(X)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(2nd(X)) -> mark#(X)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(2nd(X)) -> active#(2nd(mark(X)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(take(X1, X2)) -> mark#(X1)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(take(X1, X2)) -> mark#(X2)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(sel(X1, X2)) -> mark#(X1)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(sel(X1, X2)) -> mark#(X2)) (active#(2nd(cons(X, XS))) -> mark#(head(XS)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) } SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X))), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(head(cons(X, XS))) -> mark#(X), active#(2nd(cons(X, XS))) -> mark#(head(XS)), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(0(), cons(X, XS))) -> mark#(X)} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(2nd(X)) -> mark#(X), mark#(2nd(X)) -> active#(2nd(mark(X))), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(head(cons(X, XS))) -> mark#(X), active#(2nd(cons(X, XS))) -> mark#(head(XS)), active#(take(s(N), cons(X, XS))) -> mark#(cons(X, take(N, XS))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(0(), cons(X, XS))) -> mark#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(2nd(X)) -> active(2nd(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(from(X)) -> mark(cons(X, from(s(X)))), active(head(cons(X, XS))) -> mark(X), active(2nd(cons(X, XS))) -> mark(head(XS)), active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))), active(take(0(), XS)) -> mark(nil()), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), 2nd(mark(X)) -> 2nd(X), 2nd(active(X)) -> 2nd(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2)} Fail