MAYBE TRS: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} DP: Strict: { cons#(mark(X1), X2) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2), recip#(mark(X)) -> recip#(X), recip#(ok(X)) -> recip#(X), sqr#(mark(X)) -> sqr#(X), sqr#(ok(X)) -> sqr#(X), terms#(mark(X)) -> terms#(X), terms#(ok(X)) -> terms#(X), s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2), active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> recip#(active(X)), active#(recip(X)) -> active#(X), active#(sqr(X)) -> sqr#(active(X)), active#(sqr(X)) -> active#(X), active#(sqr(s(X))) -> sqr#(X), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X))), active#(sqr(s(X))) -> add#(sqr(X), dbl(X)), active#(sqr(s(X))) -> dbl#(X), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N))), active#(terms(N)) -> recip#(sqr(N)), active#(terms(N)) -> sqr#(N), active#(terms(N)) -> terms#(s(N)), active#(terms(N)) -> s#(N), active#(terms(X)) -> terms#(active(X)), active#(terms(X)) -> active#(X), active#(s(X)) -> s#(active(X)), active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(X1, active(X2)), active#(add(X1, X2)) -> add#(active(X1), X2), active#(add(s(X), Y)) -> s#(add(X, Y)), active#(add(s(X), Y)) -> add#(X, Y), active#(dbl(X)) -> active#(X), active#(dbl(X)) -> dbl#(active(X)), active#(dbl(s(X))) -> s#(s(dbl(X))), active#(dbl(s(X))) -> s#(dbl(X)), active#(dbl(s(X))) -> dbl#(X), active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> first#(X1, active(X2)), active#(first(X1, X2)) -> first#(active(X1), X2), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)), active#(first(s(X), cons(Y, Z))) -> first#(X, Z), add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2), dbl#(mark(X)) -> dbl#(X), dbl#(ok(X)) -> dbl#(X), first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2), first#(ok(X1), ok(X2)) -> first#(X1, X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> recip#(proper(X)), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> sqr#(proper(X)), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> terms#(proper(X)), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)), proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> dbl#(proper(X)), proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)), proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2), top#(mark(X)) -> proper#(X), top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X), top#(ok(X)) -> top#(active(X))} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} EDG: { (active#(add(X1, X2)) -> add#(X1, active(X2)), add#(ok(X1), ok(X2)) -> add#(X1, X2)) (active#(add(X1, X2)) -> add#(X1, active(X2)), add#(mark(X1), X2) -> add#(X1, X2)) (active#(add(X1, X2)) -> add#(X1, active(X2)), add#(X1, mark(X2)) -> add#(X1, X2)) (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)) (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(mark(X1), X2) -> cons#(X1, X2)) (proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)), first#(ok(X1), ok(X2)) -> first#(X1, X2)) (proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)), first#(mark(X1), X2) -> first#(X1, X2)) (proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)), first#(X1, mark(X2)) -> first#(X1, X2)) (active#(cons(X1, X2)) -> cons#(active(X1), X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)) (active#(cons(X1, X2)) -> cons#(active(X1), X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(first(X1, X2)) -> first#(active(X1), X2), first#(ok(X1), ok(X2)) -> first#(X1, X2)) (active#(first(X1, X2)) -> first#(active(X1), X2), first#(mark(X1), X2) -> first#(X1, X2)) (active#(first(X1, X2)) -> first#(active(X1), X2), first#(X1, mark(X2)) -> first#(X1, X2)) (active#(add(X1, X2)) -> active#(X2), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (active#(add(X1, X2)) -> active#(X2), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> first#(active(X1), X2)) (active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> first#(X1, active(X2))) (active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(dbl(s(X))) -> dbl#(X)) (active#(add(X1, X2)) -> active#(X2), active#(dbl(s(X))) -> s#(dbl(X))) (active#(add(X1, X2)) -> active#(X2), active#(dbl(s(X))) -> s#(s(dbl(X)))) (active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> dbl#(active(X))) (active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> add#(X, Y)) (active#(add(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> s#(add(X, Y))) (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(active(X1), X2)) (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(X1, active(X2))) (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X))) (active#(add(X1, X2)) -> active#(X2), active#(terms(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(terms(X)) -> terms#(active(X))) (active#(add(X1, X2)) -> active#(X2), active#(terms(N)) -> s#(N)) (active#(add(X1, X2)) -> active#(X2), active#(terms(N)) -> terms#(s(N))) (active#(add(X1, X2)) -> active#(X2), active#(terms(N)) -> sqr#(N)) (active#(add(X1, X2)) -> active#(X2), active#(terms(N)) -> recip#(sqr(N))) (active#(add(X1, X2)) -> active#(X2), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (active#(add(X1, X2)) -> active#(X2), active#(sqr(s(X))) -> dbl#(X)) (active#(add(X1, X2)) -> active#(X2), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (active#(add(X1, X2)) -> active#(X2), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (active#(add(X1, X2)) -> active#(X2), active#(sqr(s(X))) -> sqr#(X)) (active#(add(X1, X2)) -> active#(X2), active#(sqr(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(sqr(X)) -> sqr#(active(X))) (active#(add(X1, X2)) -> active#(X2), active#(recip(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(recip(X)) -> recip#(active(X))) (active#(add(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(cons(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(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#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(terms(X)) -> terms#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> recip#(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#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(first(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2))) (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X))) (proper#(first(X1, X2)) -> proper#(X2), proper#(terms(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(terms(X)) -> terms#(proper(X))) (proper#(first(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(first(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(recip(X)) -> recip#(proper(X))) (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (cons#(ok(X1), ok(X2)) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)) (cons#(ok(X1), ok(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (add#(mark(X1), X2) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2)) (add#(mark(X1), X2) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2)) (add#(mark(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2)) (first#(X1, mark(X2)) -> first#(X1, X2), first#(ok(X1), ok(X2)) -> first#(X1, X2)) (first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2)) (first#(X1, mark(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2)) (first#(ok(X1), ok(X2)) -> first#(X1, X2), first#(ok(X1), ok(X2)) -> first#(X1, X2)) (first#(ok(X1), ok(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2)) (first#(ok(X1), ok(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2)) (recip#(mark(X)) -> recip#(X), recip#(ok(X)) -> recip#(X)) (recip#(mark(X)) -> recip#(X), recip#(mark(X)) -> recip#(X)) (sqr#(mark(X)) -> sqr#(X), sqr#(ok(X)) -> sqr#(X)) (sqr#(mark(X)) -> sqr#(X), sqr#(mark(X)) -> sqr#(X)) (terms#(mark(X)) -> terms#(X), terms#(ok(X)) -> terms#(X)) (terms#(mark(X)) -> terms#(X), terms#(mark(X)) -> terms#(X)) (s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X)) (active#(recip(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (active#(recip(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (active#(recip(X)) -> active#(X), active#(first(X1, X2)) -> first#(active(X1), X2)) (active#(recip(X)) -> active#(X), active#(first(X1, X2)) -> first#(X1, active(X2))) (active#(recip(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2)) (active#(recip(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(dbl(s(X))) -> dbl#(X)) (active#(recip(X)) -> active#(X), active#(dbl(s(X))) -> s#(dbl(X))) (active#(recip(X)) -> active#(X), active#(dbl(s(X))) -> s#(s(dbl(X)))) (active#(recip(X)) -> active#(X), active#(dbl(X)) -> dbl#(active(X))) (active#(recip(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y)) (active#(recip(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y))) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2)) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2))) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(s(X)) -> s#(active(X))) (active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(terms(X)) -> terms#(active(X))) (active#(recip(X)) -> active#(X), active#(terms(N)) -> s#(N)) (active#(recip(X)) -> active#(X), active#(terms(N)) -> terms#(s(N))) (active#(recip(X)) -> active#(X), active#(terms(N)) -> sqr#(N)) (active#(recip(X)) -> active#(X), active#(terms(N)) -> recip#(sqr(N))) (active#(recip(X)) -> active#(X), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (active#(recip(X)) -> active#(X), active#(sqr(s(X))) -> dbl#(X)) (active#(recip(X)) -> active#(X), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (active#(recip(X)) -> active#(X), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (active#(recip(X)) -> active#(X), active#(sqr(s(X))) -> sqr#(X)) (active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(sqr(X)) -> sqr#(active(X))) (active#(recip(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(recip(X)) -> recip#(active(X))) (active#(recip(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (active#(sqr(s(X))) -> sqr#(X), sqr#(ok(X)) -> sqr#(X)) (active#(sqr(s(X))) -> sqr#(X), sqr#(mark(X)) -> sqr#(X)) (active#(terms(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (active#(terms(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> first#(active(X1), X2)) (active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> first#(X1, active(X2))) (active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2)) (active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(dbl(s(X))) -> dbl#(X)) (active#(terms(X)) -> active#(X), active#(dbl(s(X))) -> s#(dbl(X))) (active#(terms(X)) -> active#(X), active#(dbl(s(X))) -> s#(s(dbl(X)))) (active#(terms(X)) -> active#(X), active#(dbl(X)) -> dbl#(active(X))) (active#(terms(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y)) (active#(terms(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y))) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2)) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2))) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(s(X)) -> s#(active(X))) (active#(terms(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(terms(X)) -> terms#(active(X))) (active#(terms(X)) -> active#(X), active#(terms(N)) -> s#(N)) (active#(terms(X)) -> active#(X), active#(terms(N)) -> terms#(s(N))) (active#(terms(X)) -> active#(X), active#(terms(N)) -> sqr#(N)) (active#(terms(X)) -> active#(X), active#(terms(N)) -> recip#(sqr(N))) (active#(terms(X)) -> active#(X), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (active#(terms(X)) -> active#(X), active#(sqr(s(X))) -> dbl#(X)) (active#(terms(X)) -> active#(X), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (active#(terms(X)) -> active#(X), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (active#(terms(X)) -> active#(X), active#(sqr(s(X))) -> sqr#(X)) (active#(terms(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(sqr(X)) -> sqr#(active(X))) (active#(terms(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(recip(X)) -> recip#(active(X))) (active#(terms(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (active#(dbl(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (active#(dbl(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> first#(active(X1), X2)) (active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> first#(X1, active(X2))) (active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2)) (active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(dbl(X)) -> active#(X), active#(dbl(s(X))) -> dbl#(X)) (active#(dbl(X)) -> active#(X), active#(dbl(s(X))) -> s#(dbl(X))) (active#(dbl(X)) -> active#(X), active#(dbl(s(X))) -> s#(s(dbl(X)))) (active#(dbl(X)) -> active#(X), active#(dbl(X)) -> dbl#(active(X))) (active#(dbl(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y)) (active#(dbl(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y))) (active#(dbl(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2)) (active#(dbl(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2))) (active#(dbl(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(dbl(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(dbl(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(s(X)) -> s#(active(X))) (active#(dbl(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(terms(X)) -> terms#(active(X))) (active#(dbl(X)) -> active#(X), active#(terms(N)) -> s#(N)) (active#(dbl(X)) -> active#(X), active#(terms(N)) -> terms#(s(N))) (active#(dbl(X)) -> active#(X), active#(terms(N)) -> sqr#(N)) (active#(dbl(X)) -> active#(X), active#(terms(N)) -> recip#(sqr(N))) (active#(dbl(X)) -> active#(X), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (active#(dbl(X)) -> active#(X), active#(sqr(s(X))) -> dbl#(X)) (active#(dbl(X)) -> active#(X), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (active#(dbl(X)) -> active#(X), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (active#(dbl(X)) -> active#(X), active#(sqr(s(X))) -> sqr#(X)) (active#(dbl(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(sqr(X)) -> sqr#(active(X))) (active#(dbl(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(recip(X)) -> recip#(active(X))) (active#(dbl(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(dbl(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (dbl#(mark(X)) -> dbl#(X), dbl#(ok(X)) -> dbl#(X)) (dbl#(mark(X)) -> dbl#(X), dbl#(mark(X)) -> dbl#(X)) (proper#(recip(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(recip(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(recip(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2))) (proper#(recip(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (proper#(recip(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(terms(X)) -> terms#(proper(X))) (proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(recip(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(recip(X)) -> recip#(proper(X))) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(terms(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(terms(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(terms(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(terms(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2)) (proper#(terms(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2))) (proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (proper#(terms(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(terms(X)) -> terms#(proper(X))) (proper#(terms(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(terms(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(recip(X)) -> recip#(proper(X))) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(dbl(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(dbl(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2))) (proper#(dbl(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (proper#(dbl(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(terms(X)) -> terms#(proper(X))) (proper#(dbl(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(dbl(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(recip(X)) -> recip#(proper(X))) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (top#(ok(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (top#(ok(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (top#(ok(X)) -> active#(X), active#(first(X1, X2)) -> first#(active(X1), X2)) (top#(ok(X)) -> active#(X), active#(first(X1, X2)) -> first#(X1, active(X2))) (top#(ok(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2)) (top#(ok(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (top#(ok(X)) -> active#(X), active#(dbl(s(X))) -> dbl#(X)) (top#(ok(X)) -> active#(X), active#(dbl(s(X))) -> s#(dbl(X))) (top#(ok(X)) -> active#(X), active#(dbl(s(X))) -> s#(s(dbl(X)))) (top#(ok(X)) -> active#(X), active#(dbl(X)) -> dbl#(active(X))) (top#(ok(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (top#(ok(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y)) (top#(ok(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y))) (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2)) (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2))) (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (top#(ok(X)) -> active#(X), active#(s(X)) -> active#(X)) (top#(ok(X)) -> active#(X), active#(s(X)) -> s#(active(X))) (top#(ok(X)) -> active#(X), active#(terms(X)) -> active#(X)) (top#(ok(X)) -> active#(X), active#(terms(X)) -> terms#(active(X))) (top#(ok(X)) -> active#(X), active#(terms(N)) -> s#(N)) (top#(ok(X)) -> active#(X), active#(terms(N)) -> terms#(s(N))) (top#(ok(X)) -> active#(X), active#(terms(N)) -> sqr#(N)) (top#(ok(X)) -> active#(X), active#(terms(N)) -> recip#(sqr(N))) (top#(ok(X)) -> active#(X), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (top#(ok(X)) -> active#(X), active#(sqr(s(X))) -> dbl#(X)) (top#(ok(X)) -> active#(X), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (top#(ok(X)) -> active#(X), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (top#(ok(X)) -> active#(X), active#(sqr(s(X))) -> sqr#(X)) (top#(ok(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (top#(ok(X)) -> active#(X), active#(sqr(X)) -> sqr#(active(X))) (top#(ok(X)) -> active#(X), active#(recip(X)) -> active#(X)) (top#(ok(X)) -> active#(X), active#(recip(X)) -> recip#(active(X))) (top#(ok(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (top#(ok(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)) (active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(add(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (active#(add(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(active(X1), X2)) (active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(X1, active(X2))) (active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(dbl(s(X))) -> dbl#(X)) (active#(add(X1, X2)) -> active#(X1), active#(dbl(s(X))) -> s#(dbl(X))) (active#(add(X1, X2)) -> active#(X1), active#(dbl(s(X))) -> s#(s(dbl(X)))) (active#(add(X1, X2)) -> active#(X1), active#(dbl(X)) -> dbl#(active(X))) (active#(add(X1, X2)) -> active#(X1), active#(dbl(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y)) (active#(add(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y))) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2)) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(X1, active(X2))) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X))) (active#(add(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(terms(X)) -> terms#(active(X))) (active#(add(X1, X2)) -> active#(X1), active#(terms(N)) -> s#(N)) (active#(add(X1, X2)) -> active#(X1), active#(terms(N)) -> terms#(s(N))) (active#(add(X1, X2)) -> active#(X1), active#(terms(N)) -> sqr#(N)) (active#(add(X1, X2)) -> active#(X1), active#(terms(N)) -> recip#(sqr(N))) (active#(add(X1, X2)) -> active#(X1), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (active#(add(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> dbl#(X)) (active#(add(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (active#(add(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (active#(add(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> sqr#(X)) (active#(add(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(sqr(X)) -> sqr#(active(X))) (active#(add(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(recip(X)) -> recip#(active(X))) (active#(add(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(cons(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(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#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(terms(X)) -> terms#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(cons(X1, X2)) -> proper#(X1), proper#(recip(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(recip(X)) -> recip#(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#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(first(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(first(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2))) (proper#(first(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X))) (proper#(first(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X1), proper#(terms(X)) -> terms#(proper(X))) (proper#(first(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(first(X1, X2)) -> proper#(X1), proper#(recip(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X1), proper#(recip(X)) -> recip#(proper(X))) (proper#(first(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (active#(terms(N)) -> s#(N), s#(ok(X)) -> s#(X)) (active#(terms(N)) -> s#(N), s#(mark(X)) -> s#(X)) (active#(recip(X)) -> recip#(active(X)), recip#(ok(X)) -> recip#(X)) (active#(recip(X)) -> recip#(active(X)), recip#(mark(X)) -> recip#(X)) (active#(terms(X)) -> terms#(active(X)), terms#(ok(X)) -> terms#(X)) (active#(terms(X)) -> terms#(active(X)), terms#(mark(X)) -> terms#(X)) (active#(dbl(X)) -> dbl#(active(X)), dbl#(ok(X)) -> dbl#(X)) (active#(dbl(X)) -> dbl#(active(X)), dbl#(mark(X)) -> dbl#(X)) (proper#(recip(X)) -> recip#(proper(X)), recip#(ok(X)) -> recip#(X)) (proper#(recip(X)) -> recip#(proper(X)), recip#(mark(X)) -> recip#(X)) (proper#(terms(X)) -> terms#(proper(X)), terms#(ok(X)) -> terms#(X)) (proper#(terms(X)) -> terms#(proper(X)), terms#(mark(X)) -> terms#(X)) (proper#(dbl(X)) -> dbl#(proper(X)), dbl#(ok(X)) -> dbl#(X)) (proper#(dbl(X)) -> dbl#(proper(X)), dbl#(mark(X)) -> dbl#(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)) (active#(terms(N)) -> terms#(s(N)), terms#(ok(X)) -> terms#(X)) (active#(terms(N)) -> terms#(s(N)), terms#(mark(X)) -> terms#(X)) (active#(first(s(X), cons(Y, Z))) -> first#(X, Z), first#(X1, mark(X2)) -> first#(X1, X2)) (active#(first(s(X), cons(Y, Z))) -> first#(X, Z), first#(mark(X1), X2) -> first#(X1, X2)) (active#(first(s(X), cons(Y, Z))) -> first#(X, Z), first#(ok(X1), ok(X2)) -> first#(X1, X2)) (active#(terms(N)) -> recip#(sqr(N)), recip#(mark(X)) -> recip#(X)) (active#(terms(N)) -> recip#(sqr(N)), recip#(ok(X)) -> recip#(X)) (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#(s(X)) -> s#(proper(X)), s#(mark(X)) -> s#(X)) (proper#(s(X)) -> s#(proper(X)), s#(ok(X)) -> s#(X)) (proper#(sqr(X)) -> sqr#(proper(X)), sqr#(mark(X)) -> sqr#(X)) (proper#(sqr(X)) -> sqr#(proper(X)), sqr#(ok(X)) -> sqr#(X)) (active#(dbl(s(X))) -> s#(dbl(X)), s#(mark(X)) -> s#(X)) (active#(dbl(s(X))) -> s#(dbl(X)), s#(ok(X)) -> s#(X)) (active#(s(X)) -> s#(active(X)), s#(mark(X)) -> s#(X)) (active#(s(X)) -> s#(active(X)), s#(ok(X)) -> s#(X)) (active#(sqr(X)) -> sqr#(active(X)), sqr#(mark(X)) -> sqr#(X)) (active#(sqr(X)) -> sqr#(active(X)), sqr#(ok(X)) -> sqr#(X)) (active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N))), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N))), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)) (active#(terms(N)) -> sqr#(N), sqr#(mark(X)) -> sqr#(X)) (active#(terms(N)) -> sqr#(N), sqr#(ok(X)) -> sqr#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(add(X1, X2)) -> proper#(X1), proper#(recip(X)) -> recip#(proper(X))) (proper#(add(X1, X2)) -> proper#(X1), proper#(recip(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(add(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(terms(X)) -> terms#(proper(X))) (proper#(add(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X))) (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2))) (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2)) (proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(add(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)) (active#(first(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (active#(first(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(recip(X)) -> recip#(active(X))) (active#(first(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(sqr(X)) -> sqr#(active(X))) (active#(first(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> sqr#(X)) (active#(first(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (active#(first(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (active#(first(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> dbl#(X)) (active#(first(X1, X2)) -> active#(X1), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (active#(first(X1, X2)) -> active#(X1), active#(terms(N)) -> recip#(sqr(N))) (active#(first(X1, X2)) -> active#(X1), active#(terms(N)) -> sqr#(N)) (active#(first(X1, X2)) -> active#(X1), active#(terms(N)) -> terms#(s(N))) (active#(first(X1, X2)) -> active#(X1), active#(terms(N)) -> s#(N)) (active#(first(X1, X2)) -> active#(X1), active#(terms(X)) -> terms#(active(X))) (active#(first(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X))) (active#(first(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(X1, active(X2))) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2)) (active#(first(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y))) (active#(first(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y)) (active#(first(X1, X2)) -> active#(X1), active#(dbl(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(dbl(X)) -> dbl#(active(X))) (active#(first(X1, X2)) -> active#(X1), active#(dbl(s(X))) -> s#(s(dbl(X)))) (active#(first(X1, X2)) -> active#(X1), active#(dbl(s(X))) -> s#(dbl(X))) (active#(first(X1, X2)) -> active#(X1), active#(dbl(s(X))) -> dbl#(X)) (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2)) (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(X1, active(X2))) (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(active(X1), X2)) (active#(first(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (active#(first(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> recip#(active(X))) (active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(X)) -> sqr#(active(X))) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> sqr#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(s(X))) -> dbl#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (active#(cons(X1, X2)) -> active#(X1), active#(terms(N)) -> recip#(sqr(N))) (active#(cons(X1, X2)) -> active#(X1), active#(terms(N)) -> sqr#(N)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(N)) -> terms#(s(N))) (active#(cons(X1, X2)) -> active#(X1), active#(terms(N)) -> s#(N)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> terms#(active(X))) (active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X))) (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(X1, active(X2))) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2)) (active#(cons(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y))) (active#(cons(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y)) (active#(cons(X1, X2)) -> active#(X1), active#(dbl(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(dbl(X)) -> dbl#(active(X))) (active#(cons(X1, X2)) -> active#(X1), active#(dbl(s(X))) -> s#(s(dbl(X)))) (active#(cons(X1, X2)) -> active#(X1), active#(dbl(s(X))) -> s#(dbl(X))) (active#(cons(X1, X2)) -> active#(X1), active#(dbl(s(X))) -> dbl#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2)) (active#(cons(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(X1, active(X2))) (active#(cons(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(active(X1), X2)) (active#(cons(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (active#(cons(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (active#(add(s(X), Y)) -> s#(add(X, Y)), s#(mark(X)) -> s#(X)) (active#(add(s(X), Y)) -> s#(add(X, Y)), s#(ok(X)) -> s#(X)) (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (top#(mark(X)) -> proper#(X), proper#(recip(X)) -> recip#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(sqr(X)) -> sqr#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(terms(X)) -> terms#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2))) (top#(mark(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2)) (top#(mark(X)) -> proper#(X), proper#(dbl(X)) -> dbl#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (top#(mark(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (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#(recip(X)) -> recip#(proper(X))) (proper#(s(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(s(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(terms(X)) -> terms#(proper(X))) (proper#(s(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (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#(add(X1, X2)) -> add#(proper(X1), proper(X2))) (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(s(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(recip(X)) -> recip#(proper(X))) (proper#(sqr(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> terms#(proper(X))) (proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (proper#(sqr(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2))) (proper#(sqr(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(sqr(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(sqr(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (proper#(sqr(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (dbl#(ok(X)) -> dbl#(X), dbl#(mark(X)) -> dbl#(X)) (dbl#(ok(X)) -> dbl#(X), dbl#(ok(X)) -> dbl#(X)) (active#(dbl(s(X))) -> dbl#(X), dbl#(mark(X)) -> dbl#(X)) (active#(dbl(s(X))) -> dbl#(X), dbl#(ok(X)) -> dbl#(X)) (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(s(X)) -> active#(X), active#(recip(X)) -> recip#(active(X))) (active#(s(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(sqr(X)) -> sqr#(active(X))) (active#(s(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(sqr(s(X))) -> sqr#(X)) (active#(s(X)) -> active#(X), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (active#(s(X)) -> active#(X), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (active#(s(X)) -> active#(X), active#(sqr(s(X))) -> dbl#(X)) (active#(s(X)) -> active#(X), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (active#(s(X)) -> active#(X), active#(terms(N)) -> recip#(sqr(N))) (active#(s(X)) -> active#(X), active#(terms(N)) -> sqr#(N)) (active#(s(X)) -> active#(X), active#(terms(N)) -> terms#(s(N))) (active#(s(X)) -> active#(X), active#(terms(N)) -> s#(N)) (active#(s(X)) -> active#(X), active#(terms(X)) -> terms#(active(X))) (active#(s(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(s(X)) -> s#(active(X))) (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2))) (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2)) (active#(s(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y))) (active#(s(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y)) (active#(s(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(dbl(X)) -> dbl#(active(X))) (active#(s(X)) -> active#(X), active#(dbl(s(X))) -> s#(s(dbl(X)))) (active#(s(X)) -> active#(X), active#(dbl(s(X))) -> s#(dbl(X))) (active#(s(X)) -> active#(X), active#(dbl(s(X))) -> dbl#(X)) (active#(s(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(s(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2)) (active#(s(X)) -> active#(X), active#(first(X1, X2)) -> first#(X1, active(X2))) (active#(s(X)) -> active#(X), active#(first(X1, X2)) -> first#(active(X1), X2)) (active#(s(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (active#(s(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (active#(sqr(s(X))) -> dbl#(X), dbl#(mark(X)) -> dbl#(X)) (active#(sqr(s(X))) -> dbl#(X), dbl#(ok(X)) -> dbl#(X)) (active#(sqr(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (active#(sqr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(recip(X)) -> recip#(active(X))) (active#(sqr(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(sqr(X)) -> sqr#(active(X))) (active#(sqr(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(sqr(s(X))) -> sqr#(X)) (active#(sqr(X)) -> active#(X), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (active#(sqr(X)) -> active#(X), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (active#(sqr(X)) -> active#(X), active#(sqr(s(X))) -> dbl#(X)) (active#(sqr(X)) -> active#(X), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (active#(sqr(X)) -> active#(X), active#(terms(N)) -> recip#(sqr(N))) (active#(sqr(X)) -> active#(X), active#(terms(N)) -> sqr#(N)) (active#(sqr(X)) -> active#(X), active#(terms(N)) -> terms#(s(N))) (active#(sqr(X)) -> active#(X), active#(terms(N)) -> s#(N)) (active#(sqr(X)) -> active#(X), active#(terms(X)) -> terms#(active(X))) (active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(s(X)) -> s#(active(X))) (active#(sqr(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2))) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2)) (active#(sqr(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y))) (active#(sqr(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y)) (active#(sqr(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(dbl(X)) -> dbl#(active(X))) (active#(sqr(X)) -> active#(X), active#(dbl(s(X))) -> s#(s(dbl(X)))) (active#(sqr(X)) -> active#(X), active#(dbl(s(X))) -> s#(dbl(X))) (active#(sqr(X)) -> active#(X), active#(dbl(s(X))) -> dbl#(X)) (active#(sqr(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2)) (active#(sqr(X)) -> active#(X), active#(first(X1, X2)) -> first#(X1, active(X2))) (active#(sqr(X)) -> active#(X), active#(first(X1, X2)) -> first#(active(X1), X2)) (active#(sqr(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (active#(sqr(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (s#(ok(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X)) (terms#(ok(X)) -> terms#(X), terms#(mark(X)) -> terms#(X)) (terms#(ok(X)) -> terms#(X), terms#(ok(X)) -> terms#(X)) (sqr#(ok(X)) -> sqr#(X), sqr#(mark(X)) -> sqr#(X)) (sqr#(ok(X)) -> sqr#(X), sqr#(ok(X)) -> sqr#(X)) (recip#(ok(X)) -> recip#(X), recip#(mark(X)) -> recip#(X)) (recip#(ok(X)) -> recip#(X), recip#(ok(X)) -> recip#(X)) (active#(add(s(X), Y)) -> add#(X, Y), add#(X1, mark(X2)) -> add#(X1, X2)) (active#(add(s(X), Y)) -> add#(X, Y), add#(mark(X1), X2) -> add#(X1, X2)) (active#(add(s(X), Y)) -> add#(X, Y), add#(ok(X1), ok(X2)) -> add#(X1, X2)) (first#(mark(X1), X2) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2)) (first#(mark(X1), X2) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2)) (first#(mark(X1), X2) -> first#(X1, X2), first#(ok(X1), ok(X2)) -> first#(X1, X2)) (add#(ok(X1), ok(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2)) (add#(ok(X1), ok(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2)) (add#(ok(X1), ok(X2)) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2)) (add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2)) (add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2)) (add#(X1, mark(X2)) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)) (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2))) (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(add(X1, X2)) -> proper#(X2), proper#(recip(X)) -> recip#(proper(X))) (proper#(add(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> sqr#(proper(X))) (proper#(add(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X2), proper#(terms(X)) -> terms#(proper(X))) (proper#(add(X1, X2)) -> proper#(X2), proper#(terms(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X))) (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2))) (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2)) (proper#(add(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> dbl#(proper(X))) (proper#(add(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2))) (proper#(add(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2)) (active#(first(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> cons#(active(X1), X2)) (active#(first(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X2), active#(recip(X)) -> recip#(active(X))) (active#(first(X1, X2)) -> active#(X2), active#(recip(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X2), active#(sqr(X)) -> sqr#(active(X))) (active#(first(X1, X2)) -> active#(X2), active#(sqr(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X2), active#(sqr(s(X))) -> sqr#(X)) (active#(first(X1, X2)) -> active#(X2), active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X)))) (active#(first(X1, X2)) -> active#(X2), active#(sqr(s(X))) -> add#(sqr(X), dbl(X))) (active#(first(X1, X2)) -> active#(X2), active#(sqr(s(X))) -> dbl#(X)) (active#(first(X1, X2)) -> active#(X2), active#(terms(N)) -> cons#(recip(sqr(N)), terms(s(N)))) (active#(first(X1, X2)) -> active#(X2), active#(terms(N)) -> recip#(sqr(N))) (active#(first(X1, X2)) -> active#(X2), active#(terms(N)) -> sqr#(N)) (active#(first(X1, X2)) -> active#(X2), active#(terms(N)) -> terms#(s(N))) (active#(first(X1, X2)) -> active#(X2), active#(terms(N)) -> s#(N)) (active#(first(X1, X2)) -> active#(X2), active#(terms(X)) -> terms#(active(X))) (active#(first(X1, X2)) -> active#(X2), active#(terms(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X))) (active#(first(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2)) (active#(first(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(X1, active(X2))) (active#(first(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(active(X1), X2)) (active#(first(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> s#(add(X, Y))) (active#(first(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> add#(X, Y)) (active#(first(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X2), active#(dbl(X)) -> dbl#(active(X))) (active#(first(X1, X2)) -> active#(X2), active#(dbl(s(X))) -> s#(s(dbl(X)))) (active#(first(X1, X2)) -> active#(X2), active#(dbl(s(X))) -> s#(dbl(X))) (active#(first(X1, X2)) -> active#(X2), active#(dbl(s(X))) -> dbl#(X)) (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X2)) (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> first#(X1, active(X2))) (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> first#(active(X1), X2)) (active#(first(X1, X2)) -> active#(X2), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z))) (active#(first(X1, X2)) -> active#(X2), active#(first(s(X), cons(Y, Z))) -> first#(X, Z)) (active#(dbl(s(X))) -> s#(s(dbl(X))), s#(mark(X)) -> s#(X)) (active#(dbl(s(X))) -> s#(s(dbl(X))), s#(ok(X)) -> s#(X)) (active#(add(X1, X2)) -> add#(active(X1), X2), add#(X1, mark(X2)) -> add#(X1, X2)) (active#(add(X1, X2)) -> add#(active(X1), X2), add#(mark(X1), X2) -> add#(X1, X2)) (active#(add(X1, X2)) -> add#(active(X1), X2), add#(ok(X1), ok(X2)) -> add#(X1, X2)) (active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X))), s#(mark(X)) -> s#(X)) (active#(sqr(s(X))) -> s#(add(sqr(X), dbl(X))), s#(ok(X)) -> s#(X)) (proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)), add#(X1, mark(X2)) -> add#(X1, X2)) (proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)), add#(mark(X1), X2) -> add#(X1, X2)) (proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)), add#(ok(X1), ok(X2)) -> add#(X1, X2)) (active#(first(X1, X2)) -> first#(X1, active(X2)), first#(X1, mark(X2)) -> first#(X1, X2)) (active#(first(X1, X2)) -> first#(X1, active(X2)), first#(mark(X1), X2) -> first#(X1, X2)) (active#(first(X1, X2)) -> first#(X1, active(X2)), first#(ok(X1), ok(X2)) -> first#(X1, X2)) (active#(sqr(s(X))) -> add#(sqr(X), dbl(X)), add#(X1, mark(X2)) -> add#(X1, X2)) (active#(sqr(s(X))) -> add#(sqr(X), dbl(X)), add#(mark(X1), X2) -> add#(X1, X2)) (active#(sqr(s(X))) -> add#(sqr(X), dbl(X)), add#(ok(X1), ok(X2)) -> add#(X1, X2)) } SCCS: Scc: {top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))} Scc: { proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)} Scc: { first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2), first#(ok(X1), ok(X2)) -> first#(X1, X2)} Scc: {dbl#(mark(X)) -> dbl#(X), dbl#(ok(X)) -> dbl#(X)} Scc: { add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2)} Scc: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2)} Scc: {s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X)} Scc: {terms#(mark(X)) -> terms#(X), terms#(ok(X)) -> terms#(X)} Scc: {sqr#(mark(X)) -> sqr#(X), sqr#(ok(X)) -> sqr#(X)} Scc: {recip#(mark(X)) -> recip#(X), recip#(ok(X)) -> recip#(X)} Scc: { cons#(mark(X1), X2) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)} SCC: Strict: {top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} Fail SCC: Strict: { proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)} EDG: {(proper#(sqr(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (proper#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(sqr(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(recip(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#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(recip(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#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X1), proper#(recip(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(terms(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (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#(recip(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2)) (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(add(X1, X2)) -> proper#(X1), proper#(recip(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(terms(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))} SCCS: Scc: { proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)} SCC: Strict: { proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)} EDG: {(proper#(add(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2)) (proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(recip(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(sqr(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(sqr(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(recip(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#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> 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#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(first(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(terms(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1)) (proper#(first(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X)) (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(terms(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(first(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)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(recip(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))} SCCS: Scc: { proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)} SCC: Strict: { proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)} EDG: {(proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1)) (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(recip(X)) -> proper#(X)) (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(sqr(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(recip(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#(cons(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> 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#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(terms(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(dbl(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#(recip(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X))} SCCS: Scc: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)} SCC: Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)} EDG: {(proper#(cons(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(recip(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#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(recip(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#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(terms(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(dbl(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#(recip(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X))} SCCS: Scc: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)} SCC: Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)} EDG: {(proper#(cons(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> 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#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(terms(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(terms(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(terms(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(terms(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(dbl(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#(recip(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(terms(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X))} SCCS: Scc: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)} SCC: Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(terms(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)} EDG: {(proper#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(dbl(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(recip(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#(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#(recip(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(dbl(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(dbl(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(dbl(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(dbl(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X))} SCCS: Scc: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)} SCC: Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X), proper#(dbl(X)) -> proper#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)} EDG: {(proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> 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#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1)) (proper#(recip(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(recip(X)) -> proper#(X), proper#(recip(X)) -> proper#(X)) (proper#(recip(X)) -> proper#(X), proper#(sqr(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#(recip(X)) -> proper#(X)) (proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X))} SCCS: Scc: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)} SCC: Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(recip(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)} EDG: {(proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(sqr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(sqr(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#(X2), proper#(cons(X1, X2)) -> proper#(X2)) (proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(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#(sqr(X)) -> proper#(X))} SCCS: Scc: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)} SCC: Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2), proper#(sqr(X)) -> proper#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)} EDG: {(proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X)) (proper#(sqr(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#(X1), proper#(sqr(X)) -> proper#(X))} SCCS: Scc: {proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)} SCC: Strict: {proper#(cons(X1, X2)) -> proper#(X1), proper#(sqr(X)) -> proper#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(sqr(X)) -> proper#(X)} EDG: {(proper#(sqr(X)) -> proper#(X), proper#(sqr(X)) -> proper#(X))} SCCS: Scc: {proper#(sqr(X)) -> proper#(X)} SCC: Strict: {proper#(sqr(X)) -> proper#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {} Qed SCC: Strict: { first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2), first#(ok(X1), ok(X2)) -> first#(X1, X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(first#) = 0 Strict: {first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2)} EDG: {(first#(mark(X1), X2) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2)) (first#(mark(X1), X2) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2)) (first#(X1, mark(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2)) (first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))} SCCS: Scc: {first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2)} SCC: Strict: {first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(first#) = 1 Strict: {first#(mark(X1), X2) -> first#(X1, X2)} EDG: {(first#(mark(X1), X2) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))} SCCS: Scc: {first#(mark(X1), X2) -> first#(X1, X2)} SCC: Strict: {first#(mark(X1), X2) -> first#(X1, X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(first#) = 0 Strict: {} Qed SCC: Strict: {dbl#(mark(X)) -> dbl#(X), dbl#(ok(X)) -> dbl#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(dbl#) = 0 Strict: {dbl#(ok(X)) -> dbl#(X)} EDG: {(dbl#(ok(X)) -> dbl#(X), dbl#(ok(X)) -> dbl#(X))} SCCS: Scc: {dbl#(ok(X)) -> dbl#(X)} SCC: Strict: {dbl#(ok(X)) -> dbl#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(dbl#) = 0 Strict: {} Qed SCC: Strict: { add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(add#) = 0 Strict: {add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2)} EDG: {(add#(mark(X1), X2) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2)) (add#(mark(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2)) (add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2)) (add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))} SCCS: Scc: {add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2)} SCC: Strict: {add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(add#) = 0 Strict: {add#(X1, mark(X2)) -> add#(X1, X2)} EDG: {(add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))} SCCS: Scc: {add#(X1, mark(X2)) -> add#(X1, X2)} SCC: Strict: {add#(X1, mark(X2)) -> add#(X1, X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(add#) = 1 Strict: {} Qed SCC: Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2)} EDG: {(active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(dbl(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2)) (active#(recip(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2)) (active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(terms(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(sqr(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(recip(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X2), active#(recip(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X2), active#(sqr(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X2), active#(terms(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2)) (active#(first(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X2)) (active#(dbl(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(dbl(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(dbl(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(dbl(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2)) (active#(sqr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(sqr(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2)) (active#(first(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(first(X1, X2)) -> active#(X1), active#(dbl(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2)) (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(cons(X1, X2)) -> active#(X1), active#(dbl(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2))} SCCS: Scc: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2)} SCC: Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)} EDG: {(active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(dbl(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(terms(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(sqr(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(recip(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1)) (active#(dbl(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(dbl(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(dbl(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(dbl(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(sqr(X)) -> active#(X), active#(dbl(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(first(X1, X2)) -> active#(X1), active#(dbl(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(cons(X1, X2)) -> active#(X1), active#(dbl(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1))} SCCS: Scc: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)} SCC: Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(dbl(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X1)} EDG: {(active#(cons(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2)) (active#(recip(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(recip(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(sqr(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(terms(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2)) (active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X1))} SCCS: Scc: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X1)} SCC: Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X1)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)} EDG: {(active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(add(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(add(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1))} SCCS: Scc: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)} SCC: Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)} EDG: {(active#(sqr(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(first(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)) (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(recip(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1))} SCCS: Scc: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)} SCC: Strict: { active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X), active#(first(X1, X2)) -> active#(X1)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X)} EDG: {(active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(sqr(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(sqr(X)) -> active#(X)) (active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(sqr(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X))} SCCS: Scc: {active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X)} SCC: Strict: {active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(sqr(X)) -> active#(X), active#(terms(X)) -> active#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)} EDG: {(active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(recip(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(terms(X)) -> active#(X), active#(recip(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X))} SCCS: Scc: {active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)} SCC: Strict: {active#(cons(X1, X2)) -> active#(X1), active#(recip(X)) -> active#(X), active#(terms(X)) -> active#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)} EDG: {(active#(terms(X)) -> active#(X), active#(terms(X)) -> active#(X)) (active#(terms(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1)) (active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X))} SCCS: Scc: {active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)} SCC: Strict: {active#(cons(X1, X2)) -> active#(X1), active#(terms(X)) -> active#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {active#(terms(X)) -> active#(X)} EDG: {(active#(terms(X)) -> active#(X), active#(terms(X)) -> active#(X))} SCCS: Scc: {active#(terms(X)) -> active#(X)} SCC: Strict: {active#(terms(X)) -> active#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {} Qed SCC: Strict: {s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(s#) = 0 Strict: {s#(ok(X)) -> s#(X)} EDG: {(s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))} SCCS: Scc: {s#(ok(X)) -> s#(X)} SCC: Strict: {s#(ok(X)) -> s#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: {terms#(mark(X)) -> terms#(X), terms#(ok(X)) -> terms#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(terms#) = 0 Strict: {terms#(ok(X)) -> terms#(X)} EDG: {(terms#(ok(X)) -> terms#(X), terms#(ok(X)) -> terms#(X))} SCCS: Scc: {terms#(ok(X)) -> terms#(X)} SCC: Strict: {terms#(ok(X)) -> terms#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(terms#) = 0 Strict: {} Qed SCC: Strict: {sqr#(mark(X)) -> sqr#(X), sqr#(ok(X)) -> sqr#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(sqr#) = 0 Strict: {sqr#(ok(X)) -> sqr#(X)} EDG: {(sqr#(ok(X)) -> sqr#(X), sqr#(ok(X)) -> sqr#(X))} SCCS: Scc: {sqr#(ok(X)) -> sqr#(X)} SCC: Strict: {sqr#(ok(X)) -> sqr#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(sqr#) = 0 Strict: {} Qed SCC: Strict: {recip#(mark(X)) -> recip#(X), recip#(ok(X)) -> recip#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(recip#) = 0 Strict: {recip#(ok(X)) -> recip#(X)} EDG: {(recip#(ok(X)) -> recip#(X), recip#(ok(X)) -> recip#(X))} SCCS: Scc: {recip#(ok(X)) -> recip#(X)} SCC: Strict: {recip#(ok(X)) -> recip#(X)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(recip#) = 0 Strict: {} Qed SCC: Strict: { cons#(mark(X1), X2) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(cons#) = 0 Strict: {cons#(mark(X1), X2) -> cons#(X1, X2)} EDG: {(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))} SCCS: Scc: {cons#(mark(X1), X2) -> cons#(X1, X2)} SCC: Strict: {cons#(mark(X1), X2) -> cons#(X1, X2)} Weak: { cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), recip(mark(X)) -> mark(recip(X)), recip(ok(X)) -> ok(recip(X)), sqr(mark(X)) -> mark(sqr(X)), sqr(ok(X)) -> ok(sqr(X)), terms(mark(X)) -> mark(terms(X)), terms(ok(X)) -> ok(terms(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(recip(X)) -> recip(active(X)), active(sqr(X)) -> sqr(active(X)), active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))), active(sqr(0())) -> mark(0()), active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))), active(terms(X)) -> terms(active(X)), active(s(X)) -> s(active(X)), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), active(dbl(X)) -> dbl(active(X)), active(dbl(s(X))) -> mark(s(s(dbl(X)))), active(dbl(0())) -> mark(0()), active(first(X1, X2)) -> first(X1, active(X2)), active(first(X1, X2)) -> first(active(X1), X2), active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))), active(first(0(), X)) -> mark(nil()), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), dbl(mark(X)) -> mark(dbl(X)), dbl(ok(X)) -> ok(dbl(X)), first(X1, mark(X2)) -> mark(first(X1, X2)), first(mark(X1), X2) -> mark(first(X1, X2)), first(ok(X1), ok(X2)) -> ok(first(X1, X2)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(recip(X)) -> recip(proper(X)), proper(sqr(X)) -> sqr(proper(X)), proper(terms(X)) -> terms(proper(X)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), proper(dbl(X)) -> dbl(proper(X)), proper(nil()) -> ok(nil()), proper(first(X1, X2)) -> first(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(cons#) = 0 Strict: {} Qed