MAYBE TRS: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} DP: Strict: { active#(eq(s(X), s(Y))) -> eq#(X, Y), active#(inf(X)) -> active#(X), active#(inf(X)) -> s#(X), active#(inf(X)) -> cons#(X, inf(s(X))), active#(inf(X)) -> inf#(active(X)), active#(inf(X)) -> inf#(s(X)), active#(take(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> take#(X1, active(X2)), active#(take(X1, X2)) -> take#(active(X1), X2), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L)), active#(take(s(X), cons(Y, L))) -> take#(X, L), active#(length(X)) -> active#(X), active#(length(X)) -> length#(active(X)), active#(length(cons(X, L))) -> s#(length(L)), active#(length(cons(X, L))) -> length#(L), eq#(ok(X1), ok(X2)) -> eq#(X1, X2), s#(ok(X)) -> s#(X), cons#(ok(X1), ok(X2)) -> cons#(X1, X2), inf#(mark(X)) -> inf#(X), inf#(ok(X)) -> inf#(X), take#(X1, mark(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2), take#(ok(X1), ok(X2)) -> take#(X1, X2), length#(mark(X)) -> length#(X), length#(ok(X)) -> length#(X), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2)), proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(inf(X)) -> inf#(proper(X)), proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)), proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> length#(proper(X)), proper#(length(X)) -> proper#(X), top#(mark(X)) -> proper#(X), top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X), top#(ok(X)) -> top#(active(X))} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} EDG: { (active#(inf(X)) -> s#(X), s#(ok(X)) -> s#(X)) (s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X)) (inf#(ok(X)) -> inf#(X), inf#(ok(X)) -> inf#(X)) (inf#(ok(X)) -> inf#(X), inf#(mark(X)) -> inf#(X)) (length#(ok(X)) -> length#(X), length#(ok(X)) -> length#(X)) (length#(ok(X)) -> length#(X), length#(mark(X)) -> length#(X)) (proper#(inf(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(inf(X)) -> proper#(X), proper#(length(X)) -> length#(proper(X))) (proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2)) (proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2))) (proper#(inf(X)) -> proper#(X), proper#(inf(X)) -> proper#(X)) (proper#(inf(X)) -> proper#(X), proper#(inf(X)) -> inf#(proper(X))) (proper#(inf(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(inf(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(inf(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(inf(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(inf(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (proper#(inf(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X2)) (proper#(inf(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(inf(X)) -> proper#(X), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2))) (top#(mark(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(length(X)) -> length#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2)) (top#(mark(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2))) (top#(mark(X)) -> proper#(X), proper#(inf(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(inf(X)) -> inf#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (top#(mark(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X2)) (top#(mark(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2))) (active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)) (active#(take(X1, X2)) -> take#(X1, active(X2)), take#(ok(X1), ok(X2)) -> take#(X1, X2)) (active#(take(X1, X2)) -> take#(X1, active(X2)), take#(mark(X1), X2) -> take#(X1, X2)) (active#(take(X1, X2)) -> take#(X1, active(X2)), take#(X1, mark(X2)) -> take#(X1, X2)) (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)) (active#(take(X1, X2)) -> active#(X1), active#(length(cons(X, L))) -> length#(L)) (active#(take(X1, X2)) -> active#(X1), active#(length(cons(X, L))) -> s#(length(L))) (active#(take(X1, X2)) -> active#(X1), active#(length(X)) -> length#(active(X))) (active#(take(X1, X2)) -> active#(X1), active#(length(X)) -> active#(X)) (active#(take(X1, X2)) -> active#(X1), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (active#(take(X1, X2)) -> active#(X1), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (active#(take(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> take#(active(X1), X2)) (active#(take(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> take#(X1, active(X2))) (active#(take(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X2)) (active#(take(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X1)) (active#(take(X1, X2)) -> active#(X1), active#(inf(X)) -> inf#(s(X))) (active#(take(X1, X2)) -> active#(X1), active#(inf(X)) -> inf#(active(X))) (active#(take(X1, X2)) -> active#(X1), active#(inf(X)) -> cons#(X, inf(s(X)))) (active#(take(X1, X2)) -> active#(X1), active#(inf(X)) -> s#(X)) (active#(take(X1, X2)) -> active#(X1), active#(inf(X)) -> active#(X)) (active#(take(X1, X2)) -> active#(X1), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(length(X)) -> length#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2))) (proper#(cons(X1, X2)) -> proper#(X1), proper#(inf(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(inf(X)) -> inf#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2))) (active#(length(cons(X, L))) -> s#(length(L)), s#(ok(X)) -> s#(X)) (active#(inf(X)) -> inf#(s(X)), inf#(ok(X)) -> inf#(X)) (active#(inf(X)) -> inf#(s(X)), inf#(mark(X)) -> inf#(X)) (proper#(s(X)) -> s#(proper(X)), s#(ok(X)) -> s#(X)) (proper#(length(X)) -> length#(proper(X)), length#(ok(X)) -> length#(X)) (proper#(length(X)) -> length#(proper(X)), length#(mark(X)) -> length#(X)) (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X))) (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X)) (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X))) (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X2), proper#(length(X)) -> length#(proper(X))) (proper#(eq(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2))) (proper#(eq(X1, X2)) -> proper#(X2), proper#(inf(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X2), proper#(inf(X)) -> inf#(proper(X))) (proper#(eq(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(eq(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X))) (proper#(eq(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2))) (proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> length#(proper(X))) (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2))) (proper#(take(X1, X2)) -> proper#(X2), proper#(inf(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X2), proper#(inf(X)) -> inf#(proper(X))) (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(take(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X))) (proper#(take(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2))) (active#(inf(X)) -> cons#(X, inf(s(X))), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)) (cons#(ok(X1), ok(X2)) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)) (take#(mark(X1), X2) -> take#(X1, X2), take#(ok(X1), ok(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, mark(X2)) -> take#(X1, X2)) (active#(take(s(X), cons(Y, L))) -> take#(X, L), take#(ok(X1), ok(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#(X1, mark(X2)) -> take#(X1, X2)) (active#(eq(s(X), s(Y))) -> eq#(X, Y), eq#(ok(X1), ok(X2)) -> eq#(X1, X2)) (take#(ok(X1), ok(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2)) (take#(ok(X1), ok(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)) (take#(ok(X1), ok(X2)) -> take#(X1, X2), take#(ok(X1), ok(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#(mark(X1), X2) -> take#(X1, X2)) (take#(X1, mark(X2)) -> take#(X1, X2), take#(ok(X1), ok(X2)) -> take#(X1, X2)) (eq#(ok(X1), ok(X2)) -> eq#(X1, X2), eq#(ok(X1), ok(X2)) -> eq#(X1, X2)) (active#(take(X1, X2)) -> take#(active(X1), X2), take#(X1, mark(X2)) -> take#(X1, X2)) (active#(take(X1, X2)) -> take#(active(X1), X2), take#(mark(X1), X2) -> take#(X1, X2)) (active#(take(X1, X2)) -> take#(active(X1), X2), take#(ok(X1), ok(X2)) -> take#(X1, X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2))) (proper#(cons(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(inf(X)) -> inf#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X2), proper#(inf(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2))) (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(length(X)) -> length#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)) (active#(take(X1, X2)) -> active#(X2), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (active#(take(X1, X2)) -> active#(X2), active#(inf(X)) -> active#(X)) (active#(take(X1, X2)) -> active#(X2), active#(inf(X)) -> s#(X)) (active#(take(X1, X2)) -> active#(X2), active#(inf(X)) -> cons#(X, inf(s(X)))) (active#(take(X1, X2)) -> active#(X2), active#(inf(X)) -> inf#(active(X))) (active#(take(X1, X2)) -> active#(X2), active#(inf(X)) -> inf#(s(X))) (active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> active#(X1)) (active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> active#(X2)) (active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> take#(X1, active(X2))) (active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> take#(active(X1), X2)) (active#(take(X1, X2)) -> active#(X2), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (active#(take(X1, X2)) -> active#(X2), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (active#(take(X1, X2)) -> active#(X2), active#(length(X)) -> active#(X)) (active#(take(X1, X2)) -> active#(X2), active#(length(X)) -> length#(active(X))) (active#(take(X1, X2)) -> active#(X2), active#(length(cons(X, L))) -> s#(length(L))) (active#(take(X1, X2)) -> active#(X2), active#(length(cons(X, L))) -> length#(L)) (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X)) (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X))) (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X)) (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))) (proper#(inf(X)) -> inf#(proper(X)), inf#(mark(X)) -> inf#(X)) (proper#(inf(X)) -> inf#(proper(X)), inf#(ok(X)) -> inf#(X)) (active#(length(X)) -> length#(active(X)), length#(mark(X)) -> length#(X)) (active#(length(X)) -> length#(active(X)), length#(ok(X)) -> length#(X)) (active#(inf(X)) -> inf#(active(X)), inf#(mark(X)) -> inf#(X)) (active#(inf(X)) -> inf#(active(X)), inf#(ok(X)) -> inf#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2))) (proper#(take(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X))) (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X1), proper#(inf(X)) -> inf#(proper(X))) (proper#(take(X1, X2)) -> proper#(X1), proper#(inf(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2))) (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> length#(proper(X))) (proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2))) (proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X))) (proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(inf(X)) -> inf#(proper(X))) (proper#(eq(X1, X2)) -> proper#(X1), proper#(inf(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2))) (proper#(eq(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> length#(proper(X))) (proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)), take#(X1, mark(X2)) -> take#(X1, X2)) (proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)), take#(mark(X1), X2) -> take#(X1, X2)) (proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)), take#(ok(X1), ok(X2)) -> take#(X1, X2)) (proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2)), eq#(ok(X1), ok(X2)) -> eq#(X1, X2)) (active#(length(cons(X, L))) -> length#(L), length#(mark(X)) -> length#(X)) (active#(length(cons(X, L))) -> length#(L), length#(ok(X)) -> length#(X)) (top#(ok(X)) -> active#(X), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (top#(ok(X)) -> active#(X), active#(inf(X)) -> active#(X)) (top#(ok(X)) -> active#(X), active#(inf(X)) -> s#(X)) (top#(ok(X)) -> active#(X), active#(inf(X)) -> cons#(X, inf(s(X)))) (top#(ok(X)) -> active#(X), active#(inf(X)) -> inf#(active(X))) (top#(ok(X)) -> active#(X), active#(inf(X)) -> inf#(s(X))) (top#(ok(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1)) (top#(ok(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2)) (top#(ok(X)) -> active#(X), active#(take(X1, X2)) -> take#(X1, active(X2))) (top#(ok(X)) -> active#(X), active#(take(X1, X2)) -> take#(active(X1), X2)) (top#(ok(X)) -> active#(X), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (top#(ok(X)) -> active#(X), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (top#(ok(X)) -> active#(X), active#(length(X)) -> active#(X)) (top#(ok(X)) -> active#(X), active#(length(X)) -> length#(active(X))) (top#(ok(X)) -> active#(X), active#(length(cons(X, L))) -> s#(length(L))) (top#(ok(X)) -> active#(X), active#(length(cons(X, L))) -> length#(L)) (proper#(length(X)) -> proper#(X), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2))) (proper#(length(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X2)) (proper#(length(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (proper#(length(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(length(X)) -> proper#(X), proper#(inf(X)) -> inf#(proper(X))) (proper#(length(X)) -> proper#(X), proper#(inf(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2))) (proper#(length(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2)) (proper#(length(X)) -> proper#(X), proper#(length(X)) -> length#(proper(X))) (proper#(length(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(eq(X1, X2)) -> eq#(proper(X1), proper(X2))) (proper#(s(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(inf(X)) -> inf#(proper(X))) (proper#(s(X)) -> proper#(X), proper#(inf(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2))) (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(length(X)) -> length#(proper(X))) (proper#(s(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (length#(mark(X)) -> length#(X), length#(mark(X)) -> length#(X)) (length#(mark(X)) -> length#(X), length#(ok(X)) -> length#(X)) (inf#(mark(X)) -> inf#(X), inf#(mark(X)) -> inf#(X)) (inf#(mark(X)) -> inf#(X), inf#(ok(X)) -> inf#(X)) (active#(length(X)) -> active#(X), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (active#(length(X)) -> active#(X), active#(inf(X)) -> active#(X)) (active#(length(X)) -> active#(X), active#(inf(X)) -> s#(X)) (active#(length(X)) -> active#(X), active#(inf(X)) -> cons#(X, inf(s(X)))) (active#(length(X)) -> active#(X), active#(inf(X)) -> inf#(active(X))) (active#(length(X)) -> active#(X), active#(inf(X)) -> inf#(s(X))) (active#(length(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1)) (active#(length(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2)) (active#(length(X)) -> active#(X), active#(take(X1, X2)) -> take#(X1, active(X2))) (active#(length(X)) -> active#(X), active#(take(X1, X2)) -> take#(active(X1), X2)) (active#(length(X)) -> active#(X), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (active#(length(X)) -> active#(X), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (active#(length(X)) -> active#(X), active#(length(X)) -> active#(X)) (active#(length(X)) -> active#(X), active#(length(X)) -> length#(active(X))) (active#(length(X)) -> active#(X), active#(length(cons(X, L))) -> s#(length(L))) (active#(length(X)) -> active#(X), active#(length(cons(X, L))) -> length#(L)) (active#(inf(X)) -> active#(X), active#(eq(s(X), s(Y))) -> eq#(X, Y)) (active#(inf(X)) -> active#(X), active#(inf(X)) -> active#(X)) (active#(inf(X)) -> active#(X), active#(inf(X)) -> s#(X)) (active#(inf(X)) -> active#(X), active#(inf(X)) -> cons#(X, inf(s(X)))) (active#(inf(X)) -> active#(X), active#(inf(X)) -> inf#(active(X))) (active#(inf(X)) -> active#(X), active#(inf(X)) -> inf#(s(X))) (active#(inf(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1)) (active#(inf(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2)) (active#(inf(X)) -> active#(X), active#(take(X1, X2)) -> take#(X1, active(X2))) (active#(inf(X)) -> active#(X), active#(take(X1, X2)) -> take#(active(X1), X2)) (active#(inf(X)) -> active#(X), active#(take(s(X), cons(Y, L))) -> cons#(Y, take(X, L))) (active#(inf(X)) -> active#(X), active#(take(s(X), cons(Y, L))) -> take#(X, L)) (active#(inf(X)) -> active#(X), active#(length(X)) -> active#(X)) (active#(inf(X)) -> active#(X), active#(length(X)) -> length#(active(X))) (active#(inf(X)) -> active#(X), active#(length(cons(X, L))) -> s#(length(L))) (active#(inf(X)) -> active#(X), active#(length(cons(X, L))) -> length#(L)) } SCCS: Scc: {top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))} Scc: { proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)} Scc: {length#(mark(X)) -> length#(X), length#(ok(X)) -> length#(X)} Scc: { take#(X1, mark(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2), take#(ok(X1), ok(X2)) -> take#(X1, X2)} Scc: {inf#(mark(X)) -> inf#(X), inf#(ok(X)) -> inf#(X)} Scc: {cons#(ok(X1), ok(X2)) -> cons#(X1, X2)} Scc: {s#(ok(X)) -> s#(X)} Scc: {eq#(ok(X1), ok(X2)) -> eq#(X1, X2)} Scc: { active#(inf(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X2), active#(length(X)) -> active#(X)} SCC: Strict: {top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} Fail SCC: Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)} EDG: {(proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X2), proper#(inf(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(inf(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(inf(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2)) (proper#(length(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(inf(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(inf(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(inf(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(inf(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(inf(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(inf(X)) -> proper#(X), proper#(inf(X)) -> proper#(X)) (proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2)) (proper#(inf(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X1), proper#(inf(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(inf(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(inf(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X))} SCCS: Scc: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)} SCC: Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(inf(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)} EDG: {(proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(length(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2)) (proper#(length(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X))} SCCS: Scc: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)} SCC: Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} EDG: {(proper#(s(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(length(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(length(X)) -> proper#(X))} SCCS: Scc: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} SCC: Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} EDG: {(proper#(length(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(length(X)) -> proper#(X))} SCCS: Scc: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} SCC: Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} EDG: {(proper#(length(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(length(X)) -> proper#(X))} SCCS: Scc: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} SCC: Strict: { proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(length(X)) -> proper#(X)} EDG: {(proper#(s(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(length(X)) -> proper#(X), proper#(length(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X))} SCCS: Scc: {proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(length(X)) -> proper#(X)} SCC: Strict: {proper#(eq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X), proper#(length(X)) -> proper#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} EDG: {(proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)) (proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(eq(X1, X2)) -> proper#(X1)) (proper#(length(X)) -> proper#(X), proper#(length(X)) -> proper#(X))} SCCS: Scc: {proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} SCC: Strict: {proper#(eq(X1, X2)) -> proper#(X1), proper#(length(X)) -> proper#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(eq(X1, X2)) -> proper#(X1)} EDG: {(proper#(eq(X1, X2)) -> proper#(X1), proper#(eq(X1, X2)) -> proper#(X1))} SCCS: Scc: {proper#(eq(X1, X2)) -> proper#(X1)} SCC: Strict: {proper#(eq(X1, X2)) -> proper#(X1)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {} Qed SCC: Strict: {length#(mark(X)) -> length#(X), length#(ok(X)) -> length#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(length#) = 0 Strict: {length#(ok(X)) -> length#(X)} EDG: {(length#(ok(X)) -> length#(X), length#(ok(X)) -> length#(X))} SCCS: Scc: {length#(ok(X)) -> length#(X)} SCC: Strict: {length#(ok(X)) -> length#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(length#) = 0 Strict: {} Qed SCC: Strict: { take#(X1, mark(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2), take#(ok(X1), ok(X2)) -> take#(X1, X2)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(take#) = 0 Strict: {take#(X1, mark(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)} EDG: {(take#(mark(X1), 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, mark(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2))} SCCS: Scc: {take#(X1, mark(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)} SCC: Strict: {take#(X1, mark(X2)) -> take#(X1, X2), take#(mark(X1), X2) -> take#(X1, X2)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(take#) = 0 Strict: {take#(X1, mark(X2)) -> take#(X1, X2)} EDG: {(take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2))} SCCS: Scc: {take#(X1, mark(X2)) -> take#(X1, X2)} SCC: Strict: {take#(X1, mark(X2)) -> take#(X1, X2)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(take#) = 1 Strict: {} Qed SCC: Strict: {inf#(mark(X)) -> inf#(X), inf#(ok(X)) -> inf#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(inf#) = 0 Strict: {inf#(ok(X)) -> inf#(X)} EDG: {(inf#(ok(X)) -> inf#(X), inf#(ok(X)) -> inf#(X))} SCCS: Scc: {inf#(ok(X)) -> inf#(X)} SCC: Strict: {inf#(ok(X)) -> inf#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(inf#) = 0 Strict: {} Qed SCC: Strict: {cons#(ok(X1), ok(X2)) -> cons#(X1, X2)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(cons#) = 0 Strict: {} Qed SCC: Strict: {s#(ok(X)) -> s#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: {eq#(ok(X1), ok(X2)) -> eq#(X1, X2)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(eq#) = 0 Strict: {} Qed SCC: Strict: { active#(inf(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X2), active#(length(X)) -> active#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(inf(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1), active#(length(X)) -> active#(X)} EDG: {(active#(inf(X)) -> active#(X), active#(length(X)) -> active#(X)) (active#(inf(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1)) (active#(inf(X)) -> active#(X), active#(inf(X)) -> active#(X)) (active#(length(X)) -> active#(X), active#(inf(X)) -> active#(X)) (active#(length(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1)) (active#(length(X)) -> active#(X), active#(length(X)) -> active#(X)) (active#(take(X1, X2)) -> active#(X1), active#(inf(X)) -> active#(X)) (active#(take(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X1)) (active#(take(X1, X2)) -> active#(X1), active#(length(X)) -> active#(X))} SCCS: Scc: { active#(inf(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1), active#(length(X)) -> active#(X)} SCC: Strict: { active#(inf(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1), active#(length(X)) -> active#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(inf(X)) -> active#(X), active#(length(X)) -> active#(X)} EDG: {(active#(length(X)) -> active#(X), active#(length(X)) -> active#(X)) (active#(length(X)) -> active#(X), active#(inf(X)) -> active#(X)) (active#(inf(X)) -> active#(X), active#(inf(X)) -> active#(X)) (active#(inf(X)) -> active#(X), active#(length(X)) -> active#(X))} SCCS: Scc: { active#(inf(X)) -> active#(X), active#(length(X)) -> active#(X)} SCC: Strict: { active#(inf(X)) -> active#(X), active#(length(X)) -> active#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {active#(length(X)) -> active#(X)} EDG: {(active#(length(X)) -> active#(X), active#(length(X)) -> active#(X))} SCCS: Scc: {active#(length(X)) -> active#(X)} SCC: Strict: {active#(length(X)) -> active#(X)} Weak: { 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(inf(X)) -> inf(active(X)), active(take(X1, X2)) -> take(X1, active(X2)), active(take(X1, X2)) -> take(active(X1), X2), active(take(0(), X)) -> mark(nil()), active(take(s(X), cons(Y, L))) -> mark(cons(Y, take(X, L))), active(length(X)) -> length(active(X)), active(length(cons(X, L))) -> mark(s(length(L))), active(length(nil())) -> mark(0()), eq(ok(X1), ok(X2)) -> ok(eq(X1, X2)), s(ok(X)) -> ok(s(X)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), inf(mark(X)) -> mark(inf(X)), inf(ok(X)) -> ok(inf(X)), take(X1, mark(X2)) -> mark(take(X1, X2)), take(mark(X1), X2) -> mark(take(X1, X2)), take(ok(X1), ok(X2)) -> ok(take(X1, X2)), length(mark(X)) -> mark(length(X)), length(ok(X)) -> ok(length(X)), proper(true()) -> ok(true()), proper(eq(X1, X2)) -> eq(proper(X1), proper(X2)), proper(0()) -> ok(0()), proper(s(X)) -> s(proper(X)), proper(false()) -> ok(false()), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(inf(X)) -> inf(proper(X)), proper(nil()) -> ok(nil()), proper(take(X1, X2)) -> take(proper(X1), proper(X2)), proper(length(X)) -> length(proper(X)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {} Qed