YES TRS: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} DP: Strict: { mark#(true()) -> active#(true()), mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(0()) -> active#(0()), mark#(s(X)) -> active#(s(X)), mark#(false()) -> active#(false()), mark#(cons(X1, X2)) -> active#(cons(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), mark#(inf(X)) -> inf#(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#(length(X)) -> mark#(X), mark#(length(X)) -> active#(length(mark(X))), mark#(length(X)) -> length#(mark(X)), active#(eq(X, Y)) -> mark#(false()), active#(eq(0(), 0())) -> mark#(true()), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(eq(s(X), s(Y))) -> eq#(X, Y), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(inf(X)) -> s#(X), active#(inf(X)) -> cons#(X, inf(s(X))), active#(inf(X)) -> inf#(s(X)), active#(take(0(), X)) -> mark#(nil()), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L)), active#(take(s(X), cons(Y, L))) -> take#(X, L), active#(length(cons(X, L))) -> mark#(s(length(L))), active#(length(cons(X, L))) -> s#(length(L)), active#(length(cons(X, L))) -> length#(L), active#(length(nil())) -> mark#(0()), eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2), eq#(active(X1), X2) -> eq#(X1, X2), s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X), 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), inf#(mark(X)) -> inf#(X), inf#(active(X)) -> inf#(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), length#(mark(X)) -> length#(X), length#(active(X)) -> length#(X)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} EDG: { (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> length#(mark(X))) (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> active#(length(mark(X)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> take#(mark(X1), 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)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(nil()) -> active#(nil())) (mark#(take(X1, X2)) -> mark#(X1), mark#(inf(X)) -> inf#(mark(X))) (mark#(take(X1, X2)) -> mark#(X1), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(inf(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(X1, X2))) (mark#(take(X1, X2)) -> mark#(X1), mark#(false()) -> active#(false())) (mark#(take(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X))) (mark#(take(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(take(X1, X2)) -> mark#(X1), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(take(X1, X2)) -> mark#(X1), mark#(true()) -> active#(true())) (mark#(inf(X)) -> mark#(X), mark#(length(X)) -> length#(mark(X))) (mark#(inf(X)) -> mark#(X), mark#(length(X)) -> active#(length(mark(X)))) (mark#(inf(X)) -> mark#(X), mark#(length(X)) -> mark#(X)) (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(inf(X)) -> mark#(X), mark#(nil()) -> active#(nil())) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> inf#(mark(X))) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> mark#(X)) (mark#(inf(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(X1, X2))) (mark#(inf(X)) -> mark#(X), mark#(false()) -> active#(false())) (mark#(inf(X)) -> mark#(X), mark#(s(X)) -> active#(s(X))) (mark#(inf(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(inf(X)) -> mark#(X), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(inf(X)) -> mark#(X), mark#(true()) -> active#(true())) (active#(inf(X)) -> s#(X), s#(active(X)) -> s#(X)) (active#(inf(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X)) (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X)) (inf#(active(X)) -> inf#(X), inf#(active(X)) -> inf#(X)) (inf#(active(X)) -> inf#(X), inf#(mark(X)) -> inf#(X)) (length#(active(X)) -> length#(X), length#(active(X)) -> length#(X)) (length#(active(X)) -> length#(X), length#(mark(X)) -> length#(X)) (mark#(length(X)) -> active#(length(mark(X))), active#(length(nil())) -> mark#(0())) (mark#(length(X)) -> active#(length(mark(X))), active#(length(cons(X, L))) -> length#(L)) (mark#(length(X)) -> active#(length(mark(X))), active#(length(cons(X, L))) -> s#(length(L))) (mark#(length(X)) -> active#(length(mark(X))), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(length(X)) -> active#(length(mark(X))), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (mark#(length(X)) -> active#(length(mark(X))), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (mark#(length(X)) -> active#(length(mark(X))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(length(X)) -> active#(length(mark(X))), active#(take(0(), X)) -> mark#(nil())) (mark#(length(X)) -> active#(length(mark(X))), active#(inf(X)) -> inf#(s(X))) (mark#(length(X)) -> active#(length(mark(X))), active#(inf(X)) -> cons#(X, inf(s(X)))) (mark#(length(X)) -> active#(length(mark(X))), active#(inf(X)) -> s#(X)) (mark#(length(X)) -> active#(length(mark(X))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(length(X)) -> active#(length(mark(X))), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (mark#(length(X)) -> active#(length(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(length(X)) -> active#(length(mark(X))), active#(eq(0(), 0())) -> mark#(true())) (mark#(length(X)) -> active#(length(mark(X))), active#(eq(X, Y)) -> mark#(false())) (eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(active(X1), X2) -> eq#(X1, X2)) (eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2)) (eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)) (eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, mark(X2)) -> eq#(X1, X2)) (eq#(mark(X1), X2) -> eq#(X1, X2), eq#(active(X1), X2) -> eq#(X1, X2)) (eq#(mark(X1), X2) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2)) (eq#(mark(X1), X2) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)) (eq#(mark(X1), X2) -> eq#(X1, X2), eq#(X1, mark(X2)) -> eq#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), 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#(X1, active(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(active(X1), 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#(X1, active(X2)) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (take#(mark(X1), X2) -> take#(X1, X2), take#(active(X1), 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#(X1, active(X2)) -> take#(X1, X2)) (take#(mark(X1), X2) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(length(nil())) -> mark#(0())) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(length(cons(X, L))) -> length#(L)) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(length(cons(X, L))) -> s#(length(L))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(take(0(), X)) -> mark#(nil())) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(inf(X)) -> inf#(s(X))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(inf(X)) -> cons#(X, inf(s(X)))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(inf(X)) -> s#(X)) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(0(), 0())) -> mark#(true())) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(X, Y)) -> mark#(false())) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(length(X)) -> length#(mark(X))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(length(X)) -> active#(length(mark(X)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(length(X)) -> mark#(X)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(take(X1, X2)) -> mark#(X2)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(take(X1, X2)) -> mark#(X1)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> inf#(mark(X))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> mark#(X)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(cons(X1, X2)) -> active#(cons(X1, X2))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(s(X)) -> active#(s(X))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(take(X1, X2)) -> take#(mark(X1), mark(X2)), take#(active(X1), 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#(X1, active(X2)) -> take#(X1, X2)) (mark#(take(X1, X2)) -> take#(mark(X1), mark(X2)), take#(X1, mark(X2)) -> take#(X1, X2)) (active#(eq(0(), 0())) -> mark#(true()), mark#(true()) -> active#(true())) (active#(length(nil())) -> mark#(0()), mark#(0()) -> active#(0())) (mark#(s(X)) -> active#(s(X)), active#(length(nil())) -> mark#(0())) (mark#(s(X)) -> active#(s(X)), active#(length(cons(X, L))) -> length#(L)) (mark#(s(X)) -> active#(s(X)), active#(length(cons(X, L))) -> s#(length(L))) (mark#(s(X)) -> active#(s(X)), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(s(X)) -> active#(s(X)), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (mark#(s(X)) -> active#(s(X)), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (mark#(s(X)) -> active#(s(X)), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(s(X)) -> active#(s(X)), active#(take(0(), X)) -> mark#(nil())) (mark#(s(X)) -> active#(s(X)), active#(inf(X)) -> inf#(s(X))) (mark#(s(X)) -> active#(s(X)), active#(inf(X)) -> cons#(X, inf(s(X)))) (mark#(s(X)) -> active#(s(X)), active#(inf(X)) -> s#(X)) (mark#(s(X)) -> active#(s(X)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(s(X)) -> active#(s(X)), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (mark#(s(X)) -> active#(s(X)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(s(X)) -> active#(s(X)), active#(eq(0(), 0())) -> mark#(true())) (mark#(s(X)) -> active#(s(X)), active#(eq(X, Y)) -> mark#(false())) (mark#(length(X)) -> length#(mark(X)), length#(active(X)) -> length#(X)) (mark#(length(X)) -> length#(mark(X)), length#(mark(X)) -> length#(X)) (active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L)), cons#(active(X1), X2) -> cons#(X1, X2)) (active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L)), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L)), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L)), cons#(X1, mark(X2)) -> cons#(X1, X2)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(length(nil())) -> mark#(0())) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(length(cons(X, L))) -> length#(L)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(length(cons(X, L))) -> s#(length(L))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(0(), X)) -> mark#(nil())) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(inf(X)) -> inf#(s(X))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(inf(X)) -> cons#(X, inf(s(X)))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(inf(X)) -> s#(X)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(eq(0(), 0())) -> mark#(true())) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(eq(X, Y)) -> mark#(false())) (active#(eq(s(X), s(Y))) -> eq#(X, Y), eq#(active(X1), X2) -> eq#(X1, X2)) (active#(eq(s(X), s(Y))) -> eq#(X, Y), eq#(mark(X1), X2) -> eq#(X1, X2)) (active#(eq(s(X), s(Y))) -> eq#(X, Y), eq#(X1, active(X2)) -> eq#(X1, X2)) (active#(eq(s(X), s(Y))) -> eq#(X, Y), eq#(X1, mark(X2)) -> eq#(X1, X2)) (active#(inf(X)) -> cons#(X, inf(s(X))), cons#(X1, mark(X2)) -> cons#(X1, X2)) (active#(inf(X)) -> cons#(X, inf(s(X))), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(inf(X)) -> cons#(X, inf(s(X))), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(inf(X)) -> cons#(X, inf(s(X))), cons#(active(X1), X2) -> cons#(X1, X2)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(s(X)) -> active#(s(X))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(cons(X1, X2)) -> active#(cons(X1, X2))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> mark#(X)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> inf#(mark(X))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(take(X1, X2)) -> mark#(X1)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(take(X1, X2)) -> mark#(X2)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(length(X)) -> mark#(X)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(length(X)) -> active#(length(mark(X)))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(length(X)) -> length#(mark(X))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(s(X)) -> active#(s(X))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(cons(X1, X2)) -> active#(cons(X1, X2))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> mark#(X)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> inf#(mark(X))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(take(X1, X2)) -> mark#(X1)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(take(X1, X2)) -> mark#(X2)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(length(X)) -> mark#(X)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(length(X)) -> active#(length(mark(X)))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(length(X)) -> length#(mark(X))) (active#(inf(X)) -> inf#(s(X)), inf#(mark(X)) -> inf#(X)) (active#(inf(X)) -> inf#(s(X)), inf#(active(X)) -> inf#(X)) (mark#(inf(X)) -> inf#(mark(X)), inf#(mark(X)) -> inf#(X)) (mark#(inf(X)) -> inf#(mark(X)), inf#(active(X)) -> inf#(X)) (active#(length(cons(X, L))) -> s#(length(L)), s#(mark(X)) -> s#(X)) (active#(length(cons(X, L))) -> s#(length(L)), s#(active(X)) -> s#(X)) (active#(take(0(), X)) -> mark#(nil()), mark#(nil()) -> active#(nil())) (active#(eq(X, Y)) -> mark#(false()), mark#(false()) -> active#(false())) (active#(take(s(X), cons(Y, L))) -> take#(X, L), take#(X1, mark(X2)) -> take#(X1, X2)) (active#(take(s(X), cons(Y, L))) -> take#(X, L), take#(X1, active(X2)) -> take#(X1, X2)) (active#(take(s(X), cons(Y, L))) -> take#(X, L), take#(mark(X1), X2) -> take#(X1, X2)) (active#(take(s(X), cons(Y, L))) -> take#(X, L), take#(active(X1), X2) -> take#(X1, X2)) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(eq(X, Y)) -> mark#(false())) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(eq(0(), 0())) -> mark#(true())) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(inf(X)) -> s#(X)) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(inf(X)) -> cons#(X, inf(s(X)))) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(inf(X)) -> inf#(s(X))) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(take(0(), X)) -> mark#(nil())) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(length(cons(X, L))) -> s#(length(L))) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(length(cons(X, L))) -> length#(L)) (mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(length(nil())) -> mark#(0())) (take#(active(X1), X2) -> take#(X1, X2), take#(X1, mark(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#(mark(X1), X2) -> take#(X1, X2)) (take#(active(X1), X2) -> take#(X1, X2), take#(active(X1), X2) -> take#(X1, X2)) (take#(X1, active(X2)) -> take#(X1, X2), take#(X1, mark(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#(mark(X1), X2) -> take#(X1, X2)) (take#(X1, active(X2)) -> take#(X1, X2), take#(active(X1), X2) -> take#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (eq#(active(X1), X2) -> eq#(X1, X2), eq#(X1, mark(X2)) -> eq#(X1, X2)) (eq#(active(X1), X2) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)) (eq#(active(X1), X2) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2)) (eq#(active(X1), X2) -> eq#(X1, X2), eq#(active(X1), X2) -> eq#(X1, X2)) (eq#(X1, active(X2)) -> eq#(X1, X2), eq#(X1, mark(X2)) -> eq#(X1, X2)) (eq#(X1, active(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)) (eq#(X1, active(X2)) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2)) (eq#(X1, active(X2)) -> eq#(X1, X2), eq#(active(X1), X2) -> eq#(X1, X2)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(s(X)) -> active#(s(X))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(cons(X1, X2)) -> active#(cons(X1, X2))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(inf(X)) -> mark#(X)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(inf(X)) -> inf#(mark(X))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(take(X1, X2)) -> mark#(X1)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(take(X1, X2)) -> mark#(X2)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(length(X)) -> mark#(X)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(length(X)) -> active#(length(mark(X)))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(length(X)) -> length#(mark(X))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(X, Y)) -> mark#(false())) (mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(0(), 0())) -> mark#(true())) (mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (mark#(inf(X)) -> active#(inf(mark(X))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(inf(X)) -> s#(X)) (mark#(inf(X)) -> active#(inf(mark(X))), active#(inf(X)) -> cons#(X, inf(s(X)))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(inf(X)) -> inf#(s(X))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(take(0(), X)) -> mark#(nil())) (mark#(inf(X)) -> active#(inf(mark(X))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (mark#(inf(X)) -> active#(inf(mark(X))), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(length(cons(X, L))) -> s#(length(L))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(length(cons(X, L))) -> length#(L)) (mark#(inf(X)) -> active#(inf(mark(X))), active#(length(nil())) -> mark#(0())) (length#(mark(X)) -> length#(X), length#(mark(X)) -> length#(X)) (length#(mark(X)) -> length#(X), length#(active(X)) -> length#(X)) (inf#(mark(X)) -> inf#(X), inf#(mark(X)) -> inf#(X)) (inf#(mark(X)) -> inf#(X), inf#(active(X)) -> inf#(X)) (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)) (mark#(length(X)) -> mark#(X), mark#(true()) -> active#(true())) (mark#(length(X)) -> mark#(X), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(length(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(length(X)) -> mark#(X), mark#(s(X)) -> active#(s(X))) (mark#(length(X)) -> mark#(X), mark#(false()) -> active#(false())) (mark#(length(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(X1, X2))) (mark#(length(X)) -> mark#(X), mark#(inf(X)) -> mark#(X)) (mark#(length(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(length(X)) -> mark#(X), mark#(inf(X)) -> inf#(mark(X))) (mark#(length(X)) -> mark#(X), mark#(nil()) -> active#(nil())) (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> take#(mark(X1), mark(X2))) (mark#(length(X)) -> mark#(X), mark#(length(X)) -> mark#(X)) (mark#(length(X)) -> mark#(X), mark#(length(X)) -> active#(length(mark(X)))) (mark#(length(X)) -> mark#(X), mark#(length(X)) -> length#(mark(X))) (active#(length(cons(X, L))) -> length#(L), length#(mark(X)) -> length#(X)) (active#(length(cons(X, L))) -> length#(L), length#(active(X)) -> length#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(true()) -> active#(true())) (mark#(take(X1, X2)) -> mark#(X2), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(take(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(take(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(X))) (mark#(take(X1, X2)) -> mark#(X2), mark#(false()) -> active#(false())) (mark#(take(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(X1, X2))) (mark#(take(X1, X2)) -> mark#(X2), mark#(inf(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(inf(X)) -> inf#(mark(X))) (mark#(take(X1, X2)) -> mark#(X2), mark#(nil()) -> active#(nil())) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> 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)) -> take#(mark(X1), mark(X2))) (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> active#(length(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> length#(mark(X))) } SCCS: Scc: { length#(mark(X)) -> length#(X), length#(active(X)) -> length#(X)} 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: { inf#(mark(X)) -> inf#(X), inf#(active(X)) -> inf#(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: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Scc: { eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2), eq#(active(X1), X2) -> eq#(X1, X2)} Scc: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(s(X)) -> active#(s(X)), mark#(cons(X1, X2)) -> active#(cons(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(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#(length(X)) -> mark#(X), mark#(length(X)) -> active#(length(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} SCC: Strict: { length#(mark(X)) -> length#(X), length#(active(X)) -> length#(X)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(length#) = 0 Strict: {length#(active(X)) -> length#(X)} EDG: {(length#(active(X)) -> length#(X), length#(active(X)) -> length#(X))} SCCS: Scc: {length#(active(X)) -> length#(X)} SCC: Strict: {length#(active(X)) -> length#(X)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(length#) = 0 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(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} 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(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} 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(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} 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(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(take#) = 1 Strict: {} Qed SCC: Strict: { inf#(mark(X)) -> inf#(X), inf#(active(X)) -> inf#(X)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(inf#) = 0 Strict: {inf#(active(X)) -> inf#(X)} EDG: {(inf#(active(X)) -> inf#(X), inf#(active(X)) -> inf#(X))} SCCS: Scc: {inf#(active(X)) -> inf#(X)} SCC: Strict: {inf#(active(X)) -> inf#(X)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(inf#) = 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(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(cons#) = 1 Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} EDG: {(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), 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#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(active(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#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))} SCCS: Scc: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} SCC: Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(cons#) = 0 Strict: {cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)} EDG: {(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))} SCCS: Scc: {cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)} SCC: Strict: {cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(cons#) = 0 Strict: {cons#(X1, mark(X2)) -> cons#(X1, X2)} EDG: {(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))} SCCS: Scc: {cons#(X1, mark(X2)) -> cons#(X1, X2)} SCC: Strict: {cons#(X1, mark(X2)) -> cons#(X1, X2)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(cons#) = 1 Strict: {} Qed SCC: Strict: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} 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(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: { eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2), eq#(active(X1), X2) -> eq#(X1, X2)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(eq#) = 0 Strict: { eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2)} EDG: {(eq#(X1, active(X2)) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2)) (eq#(X1, active(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)) (eq#(X1, active(X2)) -> eq#(X1, X2), eq#(X1, mark(X2)) -> eq#(X1, X2)) (eq#(mark(X1), X2) -> eq#(X1, X2), eq#(X1, mark(X2)) -> eq#(X1, X2)) (eq#(mark(X1), X2) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)) (eq#(mark(X1), X2) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2)) (eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, mark(X2)) -> eq#(X1, X2)) (eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)) (eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2))} SCCS: Scc: { eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2)} SCC: Strict: { eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2), eq#(mark(X1), X2) -> eq#(X1, X2)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(eq#) = 0 Strict: { eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)} EDG: {(eq#(X1, active(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)) (eq#(X1, active(X2)) -> eq#(X1, X2), eq#(X1, mark(X2)) -> eq#(X1, X2)) (eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, mark(X2)) -> eq#(X1, X2)) (eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2))} SCCS: Scc: { eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)} SCC: Strict: { eq#(X1, mark(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(eq#) = 1 Strict: {eq#(X1, active(X2)) -> eq#(X1, X2)} EDG: {(eq#(X1, active(X2)) -> eq#(X1, X2), eq#(X1, active(X2)) -> eq#(X1, X2))} SCCS: Scc: {eq#(X1, active(X2)) -> eq#(X1, X2)} SCC: Strict: {eq#(X1, active(X2)) -> eq#(X1, X2)} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} SPSC: Simple Projection: pi(eq#) = 1 Strict: {} Qed SCC: Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(s(X)) -> active#(s(X)), mark#(cons(X1, X2)) -> active#(cons(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(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#(length(X)) -> mark#(X), mark#(length(X)) -> active#(length(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} POLY: Argument Filtering: pi(length) = [], pi(take) = [], pi(nil) = [], pi(inf) = [], pi(cons) = [], pi(false) = [], pi(s) = [], pi(0) = [], pi(eq) = [], pi(active#) = 0, pi(active) = [], pi(true) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [take] = 1, [cons] = 0, [eq] = 1, [length] = 1, [inf] = 1, [s] = 0 Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(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#(length(X)) -> mark#(X), mark#(length(X)) -> active#(length(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} EDG: {(mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> active#(length(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> mark#(X)) (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#(inf(X)) -> active#(inf(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(inf(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(length(X)) -> active#(length(mark(X)))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(length(X)) -> mark#(X)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(take(X1, X2)) -> mark#(X2)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(take(X1, X2)) -> mark#(X1)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(inf(X)) -> mark#(X)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(length(X)) -> mark#(X), mark#(length(X)) -> active#(length(mark(X)))) (mark#(length(X)) -> mark#(X), mark#(length(X)) -> mark#(X)) (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(length(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(length(X)) -> mark#(X), mark#(inf(X)) -> mark#(X)) (mark#(length(X)) -> mark#(X), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(length(X)) -> active#(length(mark(X)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(length(X)) -> mark#(X)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(take(X1, X2)) -> mark#(X2)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(take(X1, X2)) -> mark#(X1)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> mark#(X)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(length(X)) -> active#(length(mark(X)))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(length(X)) -> mark#(X)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(take(X1, X2)) -> mark#(X2)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(take(X1, X2)) -> mark#(X1)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> mark#(X)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(take(X1, X2)) -> mark#(X1), mark#(inf(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(inf(X)) -> active#(inf(mark(X)))) (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#(length(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> active#(length(mark(X)))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> mark#(X)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(take(X1, X2)) -> mark#(X1)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(take(X1, X2)) -> mark#(X2)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(length(X)) -> mark#(X)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(length(X)) -> active#(length(mark(X)))) (mark#(inf(X)) -> mark#(X), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> mark#(X)) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(inf(X)) -> mark#(X), mark#(length(X)) -> mark#(X)) (mark#(inf(X)) -> mark#(X), mark#(length(X)) -> active#(length(mark(X)))) (mark#(length(X)) -> active#(length(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(length(X)) -> active#(length(mark(X))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(length(X)) -> active#(length(mark(X))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(length(X)) -> active#(length(mark(X))), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(length(cons(X, L))) -> mark#(s(length(L))))} SCCS: Scc: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(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#(length(X)) -> mark#(X), mark#(length(X)) -> active#(length(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} SCC: Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(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#(length(X)) -> mark#(X), mark#(length(X)) -> active#(length(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} POLY: Argument Filtering: pi(length) = [0], pi(take) = [0,1], pi(nil) = [], pi(inf) = 0, pi(cons) = [], pi(false) = [], pi(s) = [], pi(0) = [], pi(eq) = [], pi(active#) = [], pi(active) = [], pi(true) = [], pi(mark#) = 0, pi(mark) = [] Usable Rules: {} Interpretation: [active#] = 0, [take](x0, x1) = x0 + x1, [cons] = 0, [eq] = 0, [length](x0) = x0 + 1, [s] = 0 Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} EDG: {(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#(inf(X)) -> active#(inf(mark(X)))) (mark#(take(X1, X2)) -> mark#(X1), mark#(inf(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(take(X1, X2)) -> mark#(X2)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(take(X1, X2)) -> mark#(X1)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> mark#(X)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(take(X1, X2)) -> mark#(X2)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(take(X1, X2)) -> mark#(X1)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> mark#(X)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(take(X1, X2)) -> mark#(X2)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(take(X1, X2)) -> mark#(X1)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(inf(X)) -> mark#(X)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(length(cons(X, L))) -> mark#(s(length(L)))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> mark#(X)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(take(X1, X2)) -> mark#(X1)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(take(X1, X2)) -> mark#(X2)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(take(X1, X2)) -> mark#(X2), mark#(inf(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2)))) (mark#(inf(X)) -> mark#(X), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> mark#(X)) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))))} SCCS: Scc: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} SCC: Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> active#(take(mark(X1), mark(X2))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} POLY: Argument Filtering: pi(length) = [], pi(take) = [0,1], pi(nil) = [], pi(inf) = 0, pi(cons) = [], pi(false) = [], pi(s) = [], pi(0) = [], pi(eq) = [], pi(active#) = [], pi(active) = [], pi(true) = [], pi(mark#) = 0, pi(mark) = [] Usable Rules: {} Interpretation: [active#] = 0, [take](x0, x1) = x0 + x1 + 1, [cons] = 0, [eq] = 0, [s] = 0 Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} EDG: {(active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(inf(X)) -> mark#(X)) (active#(length(cons(X, L))) -> mark#(s(length(L))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> mark#(X)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> mark#(X)) (mark#(inf(X)) -> mark#(X), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> mark#(X)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> mark#(X)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(length(cons(X, L))) -> mark#(s(length(L)))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(length(cons(X, L))) -> mark#(s(length(L))))} SCCS: Scc: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} SCC: Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), active#(length(cons(X, L))) -> mark#(s(length(L)))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} POLY: Argument Filtering: pi(length) = [], pi(take) = [], pi(nil) = [], pi(inf) = [], pi(cons) = [], pi(false) = [], pi(s) = [], pi(0) = [], pi(eq) = [], pi(active#) = 0, pi(active) = [], pi(true) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 0, [take] = 0, [eq] = 0, [length] = 1, [inf] = 0 Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} EDG: {(mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> mark#(X)) (mark#(inf(X)) -> mark#(X), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(inf(X)) -> mark#(X)) (active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> mark#(X)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> mark#(X)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> active#(inf(mark(X)))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L))))} SCCS: Scc: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))} SCC: Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X)))), active#(take(s(X), cons(Y, L))) -> mark#(cons(Y, take(X, L)))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} POLY: Argument Filtering: pi(length) = [], pi(take) = [0,1], pi(nil) = [], pi(inf) = [], pi(cons) = [], pi(false) = [], pi(s) = [], pi(0) = [], pi(eq) = [], pi(active#) = 0, pi(active) = [], pi(true) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 0, [take](x0, x1) = x0 + x1 + 1, [cons] = 0, [eq] = 0, [inf] = 0, [s] = 1 Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} EDG: {(active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(inf(X)) -> mark#(X)) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> active#(inf(mark(X)))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(inf(X)) -> mark#(X)) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(inf(X)) -> active#(inf(mark(X))), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(inf(X)) -> mark#(X), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> mark#(X)) (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))))} SCCS: Scc: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))} SCC: Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> active#(inf(mark(X))), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} POLY: Argument Filtering: pi(length) = [], pi(take) = [], pi(nil) = [], pi(inf) = [0], pi(cons) = [], pi(false) = [], pi(s) = [], pi(0) = [], pi(eq) = [], pi(active#) = [], pi(active) = [], pi(true) = [], pi(mark#) = 0, pi(mark) = [] Usable Rules: {} Interpretation: [active#] = 0, [cons] = 0, [eq] = 0, [inf](x0) = x0 + 1 Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} EDG: {(mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))) (active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (active#(inf(X)) -> mark#(cons(X, inf(s(X)))), mark#(eq(X1, X2)) -> active#(eq(X1, X2)))} SCCS: Scc: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))} SCC: Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), active#(inf(X)) -> mark#(cons(X, inf(s(X))))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} POLY: Argument Filtering: pi(length) = [], pi(take) = [], pi(nil) = [], pi(inf) = [], pi(cons) = [], pi(false) = [], pi(s) = [], pi(0) = [], pi(eq) = [], pi(active#) = [], pi(active) = [], pi(true) = [], pi(mark#) = 0, pi(mark) = [] Usable Rules: {} Interpretation: [active#] = 1, [cons] = 0, [eq] = 1 Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} EDG: {(active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)), mark#(eq(X1, X2)) -> active#(eq(X1, X2))) (mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y)))} SCCS: Scc: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))} SCC: Strict: { mark#(eq(X1, X2)) -> active#(eq(X1, X2)), active#(eq(s(X), s(Y))) -> mark#(eq(X, Y))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} POLY: Argument Filtering: pi(length) = [], pi(take) = [], pi(nil) = [], pi(inf) = [], pi(cons) = [], pi(false) = [], pi(s) = [0], pi(0) = [], pi(eq) = 1, pi(active#) = [0], pi(active) = 0, pi(true) = [], pi(mark#) = [0], pi(mark) = 0 Usable Rules: {} Interpretation: [active#](x0) = x0 + 1, [mark#](x0) = x0 + 1, [s](x0) = x0 + 1 Strict: {mark#(eq(X1, X2)) -> active#(eq(X1, X2))} Weak: { mark(true()) -> active(true()), mark(eq(X1, X2)) -> active(eq(X1, X2)), mark(0()) -> active(0()), mark(s(X)) -> active(s(X)), mark(false()) -> active(false()), mark(cons(X1, X2)) -> active(cons(X1, X2)), mark(inf(X)) -> active(inf(mark(X))), mark(nil()) -> active(nil()), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(length(X)) -> active(length(mark(X))), active(eq(X, Y)) -> mark(false()), active(eq(0(), 0())) -> mark(true()), active(eq(s(X), s(Y))) -> mark(eq(X, Y)), active(inf(X)) -> mark(cons(X, inf(s(X)))), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(X1, mark(X2)) -> eq(X1, X2), eq(X1, active(X2)) -> eq(X1, X2), eq(mark(X1), X2) -> eq(X1, X2), eq(active(X1), X2) -> eq(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), 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), inf(mark(X)) -> inf(X), inf(active(X)) -> inf(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), length(mark(X)) -> length(X), length(active(X)) -> length(X)} EDG: {} SCCS: Qed