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