YES TRS: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} DP: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(sqr(X)) -> a__sqr#(mark(X)), mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__terms#(N) -> a__sqr#(mark(N)), a__terms#(N) -> mark#(N), a__add#(0(), X) -> mark#(X), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} EDG: { (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> a__dbl#(mark(X))) (mark#(add(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> a__sqr#(mark(X))) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(add(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(terms(X)) -> a__terms#(mark(X)), a__terms#(N) -> mark#(N)) (mark#(terms(X)) -> a__terms#(mark(X)), a__terms#(N) -> a__sqr#(mark(N))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(dbl(X)) -> a__dbl#(mark(X))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(dbl(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> a__sqr#(mark(X))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> a__terms#(mark(X))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(recip(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)) (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(terms(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X))) (mark#(terms(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(terms(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(terms(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X))) (mark#(terms(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(terms(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(terms(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> mark#(X)) (mark#(terms(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(terms(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X))) (mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X))) (mark#(dbl(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(dbl(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(dbl(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> mark#(X2)) (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> mark#(X1)) (a__terms#(N) -> mark#(N), mark#(dbl(X)) -> a__dbl#(mark(X))) (a__terms#(N) -> mark#(N), mark#(dbl(X)) -> mark#(X)) (a__terms#(N) -> mark#(N), mark#(sqr(X)) -> mark#(X)) (a__terms#(N) -> mark#(N), mark#(sqr(X)) -> a__sqr#(mark(X))) (a__terms#(N) -> mark#(N), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (a__terms#(N) -> mark#(N), mark#(add(X1, X2)) -> mark#(X2)) (a__terms#(N) -> mark#(N), mark#(add(X1, X2)) -> mark#(X1)) (a__terms#(N) -> mark#(N), mark#(terms(X)) -> a__terms#(mark(X))) (a__terms#(N) -> mark#(N), mark#(terms(X)) -> mark#(X)) (a__terms#(N) -> mark#(N), mark#(recip(X)) -> mark#(X)) (a__terms#(N) -> mark#(N), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> a__dbl#(mark(X))) (mark#(first(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> a__sqr#(mark(X))) (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(terms(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> a__sqr#(mark(X))) (mark#(add(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> a__dbl#(mark(X))) (mark#(add(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (a__add#(0(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(recip(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(terms(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (a__add#(0(), X) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X))) (a__add#(0(), X) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X))) (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(sqr(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(sqr(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X))) (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X))) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(recip(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(recip(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(recip(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(recip(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(recip(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X))) (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X))) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(0(), X) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> a__sqr#(mark(X))) (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> a__dbl#(mark(X))) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> a__sqr#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> a__dbl#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) } SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__terms#(N) -> mark#(N), a__add#(0(), X) -> mark#(X), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__terms#(N) -> mark#(N), a__add#(0(), X) -> mark#(X), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} POLY: Argument Filtering: pi(first) = [0,1], pi(a__first#) = 1, pi(a__first) = [0,1], pi(nil) = [], pi(a__add#) = 1, pi(a__add) = [0,1], pi(a__dbl) = 0, pi(dbl) = 0, pi(sqr) = 0, pi(add) = [0,1], pi(0) = [], pi(a__terms#) = 0, pi(a__terms) = 0, pi(s) = [], pi(terms) = 0, pi(mark#) = 0, pi(mark) = 0, pi(a__sqr) = 0, pi(recip) = 0, pi(cons) = 0 Usable Rules: {} Interpretation: [first](x0, x1) = x0 + x1, [add](x0, x1) = x0 + x1 + 1 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)), mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__terms#(N) -> mark#(N), a__add#(0(), X) -> mark#(X), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} EDG: {(mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(terms(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(terms(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> mark#(X)) (mark#(terms(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(terms(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(terms(X)) -> a__terms#(mark(X)), a__terms#(N) -> mark#(N)) (a__add#(0(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(recip(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(terms(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (a__add#(0(), X) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(recip(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(recip(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(recip(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> a__terms#(mark(X))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(dbl(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (a__terms#(N) -> mark#(N), mark#(cons(X1, X2)) -> mark#(X1)) (a__terms#(N) -> mark#(N), mark#(recip(X)) -> mark#(X)) (a__terms#(N) -> mark#(N), mark#(terms(X)) -> mark#(X)) (a__terms#(N) -> mark#(N), mark#(terms(X)) -> a__terms#(mark(X))) (a__terms#(N) -> mark#(N), mark#(sqr(X)) -> mark#(X)) (a__terms#(N) -> mark#(N), mark#(dbl(X)) -> mark#(X)) (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> mark#(X1)) (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> mark#(X2)) (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)), mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__terms#(N) -> mark#(N), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)), mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__terms#(N) -> mark#(N), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} POLY: Argument Filtering: pi(first) = [0,1], pi(a__first#) = 1, pi(a__first) = [0,1], pi(nil) = [], pi(a__add) = 1, pi(a__dbl) = 0, pi(dbl) = 0, pi(sqr) = 0, pi(add) = 1, pi(0) = [], pi(a__terms#) = [0], pi(a__terms) = [0], pi(s) = [], pi(terms) = [0], pi(mark#) = 0, pi(mark) = 0, pi(a__sqr) = 0, pi(recip) = 0, pi(cons) = 0 Usable Rules: {} Interpretation: [a__terms#](x0) = x0 + 1, [first](x0, x1) = x0 + x1, [terms](x0) = x0 + 1 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)), mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} EDG: {(mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(first(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(sqr(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(dbl(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> a__terms#(mark(X))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(recip(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)) (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(dbl(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(dbl(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(dbl(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(recip(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(recip(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} POLY: Argument Filtering: pi(first) = [0,1], pi(a__first#) = 1, pi(a__first) = [0,1], pi(nil) = [], pi(a__add) = 1, pi(a__dbl) = [0], pi(dbl) = [0], pi(sqr) = 0, pi(add) = 1, pi(0) = [], pi(a__terms) = 0, pi(s) = [], pi(terms) = 0, pi(mark#) = 0, pi(mark) = 0, pi(a__sqr) = 0, pi(recip) = 0, pi(cons) = 0 Usable Rules: {} Interpretation: [first](x0, x1) = x0 + x1, [dbl](x0) = x0 + 1 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} EDG: {(mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(recip(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(recip(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(recip(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} POLY: Argument Filtering: pi(first) = [0,1], pi(a__first#) = 1, pi(a__first) = [0,1], pi(nil) = [], pi(a__add) = 1, pi(a__dbl) = [], pi(dbl) = [], pi(sqr) = 0, pi(add) = 1, pi(0) = [], pi(a__terms) = [0], pi(s) = [], pi(terms) = [0], pi(mark#) = 0, pi(mark) = 0, pi(a__sqr) = 0, pi(recip) = [0], pi(cons) = 0 Usable Rules: {} Interpretation: [first](x0, x1) = x0 + x1, [recip](x0) = x0 + 1 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} EDG: {(mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2)) (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X)) (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2)) (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1)) (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X)) (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2)) (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} POLY: Argument Filtering: pi(first) = [0,1], pi(a__first#) = [0,1], pi(a__first) = [0,1], pi(nil) = [], pi(a__add) = [0,1], pi(a__dbl) = 0, pi(dbl) = 0, pi(sqr) = 0, pi(add) = [0,1], pi(0) = [], pi(a__terms) = [], pi(s) = [], pi(terms) = [], pi(mark#) = [0], pi(mark) = 0, pi(a__sqr) = 0, pi(recip) = [], pi(cons) = [0] Usable Rules: {} Interpretation: [a__first#](x0, x1) = x0 + x1, [mark#](x0) = x0 + 1, [first](x0, x1) = x0 + x1 + 1, [cons](x0) = x0 + 1, [s] = 1 Strict: {mark#(sqr(X)) -> mark#(X)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} EDG: {(mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))} SCCS: Scc: {mark#(sqr(X)) -> mark#(X)} SCC: Strict: {mark#(sqr(X)) -> mark#(X)} Weak: { a__sqr(X) -> sqr(X), a__sqr(s(X)) -> s(add(sqr(X), dbl(X))), a__sqr(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(recip(X)) -> recip(mark(X)), mark(terms(X)) -> a__terms(mark(X)), mark(s(X)) -> s(X), mark(0()) -> 0(), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(sqr(X)) -> a__sqr(mark(X)), mark(dbl(X)) -> a__dbl(mark(X)), mark(nil()) -> nil(), mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)), a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))), a__terms(X) -> terms(X), a__dbl(X) -> dbl(X), a__dbl(s(X)) -> s(s(dbl(X))), a__dbl(0()) -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s(X), Y) -> s(add(X, Y)), a__add(0(), X) -> mark(X), a__first(X1, X2) -> first(X1, X2), a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)), a__first(0(), X) -> nil()} SPSC: Simple Projection: pi(mark#) = 0 Strict: {} Qed