MAYBE Time: 0.063287 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: DP: { 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} 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} UR: { 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} 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)) (proper# eq(X1, X2) -> eq#(proper X1, proper X2), eq#(ok X1, ok X2) -> eq#(X1, X2)) (proper# take(X1, X2) -> take#(proper X1, proper X2), take#(ok X1, ok 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#(X1, mark X2) -> take#(X1, 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# X1, proper# length X -> proper# X) (proper# eq(X1, X2) -> proper# X1, proper# length X -> length# proper X) (proper# eq(X1, X2) -> proper# X1, proper# take(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) -> take#(proper X1, proper X2)) (proper# eq(X1, X2) -> proper# X1, proper# inf X -> proper# X) (proper# eq(X1, X2) -> proper# X1, proper# inf X -> inf# proper X) (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# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# eq(X1, X2) -> proper# X1, proper# s X -> proper# X) (proper# eq(X1, X2) -> proper# X1, proper# s X -> s# proper X) (proper# eq(X1, X2) -> proper# X1, proper# eq(X1, X2) -> proper# X2) (proper# eq(X1, X2) -> proper# X1, proper# eq(X1, X2) -> proper# X1) (proper# eq(X1, X2) -> proper# X1, proper# eq(X1, X2) -> eq#(proper X1, proper X2)) (proper# take(X1, X2) -> proper# X1, proper# length X -> proper# X) (proper# take(X1, X2) -> proper# X1, proper# length X -> length# proper X) (proper# take(X1, X2) -> proper# X1, proper# take(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) -> take#(proper X1, proper X2)) (proper# take(X1, X2) -> proper# X1, proper# inf X -> proper# X) (proper# take(X1, X2) -> proper# X1, proper# inf X -> inf# proper X) (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# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# take(X1, X2) -> proper# X1, proper# s X -> proper# X) (proper# take(X1, X2) -> proper# X1, proper# s X -> s# proper X) (proper# take(X1, X2) -> proper# X1, proper# eq(X1, X2) -> proper# X2) (proper# take(X1, X2) -> proper# X1, proper# eq(X1, X2) -> proper# X1) (proper# take(X1, X2) -> proper# X1, proper# eq(X1, X2) -> eq#(proper X1, proper X2)) (active# take(X1, X2) -> active# X2, active# length cons(X, L) -> length# L) (active# take(X1, X2) -> active# X2, active# length cons(X, L) -> s# length L) (active# take(X1, X2) -> active# X2, active# length X -> length# active X) (active# take(X1, X2) -> active# X2, active# length X -> active# X) (active# take(X1, X2) -> active# X2, active# take(s X, cons(Y, L)) -> take#(X, L)) (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(X1, X2) -> take#(active X1, 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) -> active# X2) (active# take(X1, X2) -> active# X2, active# take(X1, X2) -> active# X1) (active# take(X1, X2) -> active# X2, active# inf 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 -> cons#(X, inf s X)) (active# take(X1, X2) -> active# X2, active# inf X -> s# X) (active# take(X1, X2) -> active# X2, active# inf X -> active# X) (active# take(X1, X2) -> active# X2, active# eq(s X, s Y) -> eq#(X, Y)) (proper# cons(X1, X2) -> proper# X2, proper# length X -> proper# X) (proper# cons(X1, X2) -> proper# X2, proper# length X -> length# proper X) (proper# cons(X1, X2) -> proper# X2, proper# take(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) -> take#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X2, proper# inf X -> proper# X) (proper# cons(X1, X2) -> proper# X2, proper# inf X -> inf# proper X) (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X) (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X) (proper# cons(X1, X2) -> proper# X2, proper# eq(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X2, proper# eq(X1, X2) -> proper# X1) (proper# cons(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)) (proper# take(X1, X2) -> proper# X2, proper# eq(X1, X2) -> eq#(proper X1, proper X2)) (proper# take(X1, X2) -> proper# X2, proper# eq(X1, X2) -> proper# X1) (proper# take(X1, X2) -> proper# X2, proper# eq(X1, X2) -> proper# X2) (proper# take(X1, X2) -> proper# X2, proper# s X -> s# proper X) (proper# take(X1, X2) -> proper# X2, proper# s X -> proper# X) (proper# take(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# take(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1) (proper# take(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2) (proper# take(X1, X2) -> proper# X2, proper# inf X -> inf# proper X) (proper# take(X1, X2) -> proper# X2, proper# inf X -> proper# X) (proper# take(X1, X2) -> proper# X2, proper# take(X1, X2) -> take#(proper X1, proper X2)) (proper# take(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X1) (proper# take(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X2) (proper# take(X1, X2) -> proper# X2, proper# length X -> length# proper X) (proper# take(X1, X2) -> proper# X2, proper# length X -> proper# X) (proper# eq(X1, X2) -> proper# X2, proper# eq(X1, X2) -> eq#(proper X1, proper X2)) (proper# eq(X1, X2) -> proper# X2, proper# eq(X1, X2) -> proper# X1) (proper# eq(X1, X2) -> proper# X2, proper# eq(X1, X2) -> proper# X2) (proper# eq(X1, X2) -> proper# X2, proper# s X -> s# proper X) (proper# eq(X1, X2) -> proper# X2, proper# s X -> proper# X) (proper# eq(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# eq(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1) (proper# eq(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2) (proper# eq(X1, X2) -> proper# X2, proper# inf X -> inf# proper X) (proper# eq(X1, X2) -> proper# X2, proper# inf X -> proper# X) (proper# eq(X1, X2) -> proper# X2, proper# take(X1, X2) -> take#(proper X1, proper X2)) (proper# eq(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X1) (proper# eq(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X2) (proper# eq(X1, X2) -> proper# X2, proper# length X -> length# proper X) (proper# eq(X1, X2) -> proper# X2, proper# length X -> proper# X) (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# X1, proper# eq(X1, X2) -> eq#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X1, proper# eq(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X1, proper# eq(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X) (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (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# inf X -> inf# proper X) (proper# cons(X1, X2) -> proper# X1, proper# inf X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> take#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X1, proper# length X -> length# proper X) (proper# cons(X1, X2) -> proper# X1, proper# length X -> proper# X) (active# take(X1, X2) -> active# X1, active# eq(s X, s Y) -> eq#(X, Y)) (active# take(X1, X2) -> active# X1, active# inf X -> active# X) (active# take(X1, X2) -> active# X1, active# inf X -> s# X) (active# take(X1, X2) -> active# X1, active# inf X -> cons#(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 -> inf# s X) (active# take(X1, X2) -> active# X1, active# take(X1, X2) -> active# X1) (active# take(X1, X2) -> active# X1, active# take(X1, X2) -> active# 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) -> take#(active X1, X2)) (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(s X, cons(Y, L)) -> take#(X, L)) (active# take(X1, X2) -> active# X1, active# length X -> active# X) (active# take(X1, X2) -> active# X1, active# length X -> length# active X) (active# take(X1, X2) -> active# X1, active# length cons(X, L) -> s# length L) (active# take(X1, X2) -> active# X1, 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) (active# length cons(X, L) -> length# L, length# mark X -> length# X) (active# length cons(X, L) -> length# L, length# ok X -> length# X) (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2)) (active# take(X1, X2) -> take#(X1, active X2), take#(X1, mark 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#(ok X1, ok X2) -> take#(X1, X2)) (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) } STATUS: arrows: 0.856790 SCCS (9): 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: { active# inf X -> active# X, active# take(X1, X2) -> active# X1, active# take(X1, X2) -> active# X2, active# length X -> active# 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 (2): 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} Open SCC (9): 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} Open SCC (4): 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} Open SCC (2): 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} Open SCC (3): 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} Open SCC (2): 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} Open SCC (1): 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} Open SCC (1): 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} Open SCC (1): 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} Open