YES TRS: { sqr(s(X)) -> s(add(sqr(X), dbl(X))), sqr(0()) -> 0(), terms(N) -> cons(recip(sqr(N)), n__terms(s(N))), terms(X) -> n__terms(X), add(s(X), Y) -> s(add(X, Y)), add(0(), X) -> X, dbl(s(X)) -> s(s(dbl(X))), dbl(0()) -> 0(), first(X1, X2) -> n__first(X1, X2), first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))), first(0(), X) -> nil(), activate(X) -> X, activate(n__terms(X)) -> terms(X), activate(n__first(X1, X2)) -> first(X1, X2), half(s(s(X))) -> s(half(X)), half(s(0())) -> 0(), half(0()) -> 0(), half(dbl(X)) -> X} DP: Strict: { sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> add#(sqr(X), dbl(X)), sqr#(s(X)) -> dbl#(X), terms#(N) -> sqr#(N), add#(s(X), Y) -> add#(X, Y), dbl#(s(X)) -> dbl#(X), first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__terms(X)) -> terms#(X), activate#(n__first(X1, X2)) -> first#(X1, X2), half#(s(s(X))) -> half#(X)} Weak: { sqr(s(X)) -> s(add(sqr(X), dbl(X))), sqr(0()) -> 0(), terms(N) -> cons(recip(sqr(N)), n__terms(s(N))), terms(X) -> n__terms(X), add(s(X), Y) -> s(add(X, Y)), add(0(), X) -> X, dbl(s(X)) -> s(s(dbl(X))), dbl(0()) -> 0(), first(X1, X2) -> n__first(X1, X2), first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))), first(0(), X) -> nil(), activate(X) -> X, activate(n__terms(X)) -> terms(X), activate(n__first(X1, X2)) -> first(X1, X2), half(s(s(X))) -> s(half(X)), half(s(0())) -> 0(), half(0()) -> 0(), half(dbl(X)) -> X} EDG: {(sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> dbl#(X)) (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> add#(sqr(X), dbl(X))) (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> sqr#(X)) (dbl#(s(X)) -> dbl#(X), dbl#(s(X)) -> dbl#(X)) (half#(s(s(X))) -> half#(X), half#(s(s(X))) -> half#(X)) (sqr#(s(X)) -> add#(sqr(X), dbl(X)), add#(s(X), Y) -> add#(X, Y)) (add#(s(X), Y) -> add#(X, Y), add#(s(X), Y) -> add#(X, Y)) (activate#(n__first(X1, X2)) -> first#(X1, X2), first#(s(X), cons(Y, Z)) -> activate#(Z)) (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__terms(X)) -> terms#(X)) (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> first#(X1, X2)) (activate#(n__terms(X)) -> terms#(X), terms#(N) -> sqr#(N)) (sqr#(s(X)) -> dbl#(X), dbl#(s(X)) -> dbl#(X)) (terms#(N) -> sqr#(N), sqr#(s(X)) -> sqr#(X)) (terms#(N) -> sqr#(N), sqr#(s(X)) -> add#(sqr(X), dbl(X))) (terms#(N) -> sqr#(N), sqr#(s(X)) -> dbl#(X))} SCCS: Scc: {half#(s(s(X))) -> half#(X)} Scc: { first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> first#(X1, X2)} Scc: {dbl#(s(X)) -> dbl#(X)} Scc: {add#(s(X), Y) -> add#(X, Y)} Scc: {sqr#(s(X)) -> sqr#(X)} SCC: Strict: {half#(s(s(X))) -> half#(X)} Weak: { sqr(s(X)) -> s(add(sqr(X), dbl(X))), sqr(0()) -> 0(), terms(N) -> cons(recip(sqr(N)), n__terms(s(N))), terms(X) -> n__terms(X), add(s(X), Y) -> s(add(X, Y)), add(0(), X) -> X, dbl(s(X)) -> s(s(dbl(X))), dbl(0()) -> 0(), first(X1, X2) -> n__first(X1, X2), first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))), first(0(), X) -> nil(), activate(X) -> X, activate(n__terms(X)) -> terms(X), activate(n__first(X1, X2)) -> first(X1, X2), half(s(s(X))) -> s(half(X)), half(s(0())) -> 0(), half(0()) -> 0(), half(dbl(X)) -> X} SPSC: Simple Projection: pi(half#) = 0 Strict: {} Qed SCC: Strict: { first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> first#(X1, X2)} Weak: { sqr(s(X)) -> s(add(sqr(X), dbl(X))), sqr(0()) -> 0(), terms(N) -> cons(recip(sqr(N)), n__terms(s(N))), terms(X) -> n__terms(X), add(s(X), Y) -> s(add(X, Y)), add(0(), X) -> X, dbl(s(X)) -> s(s(dbl(X))), dbl(0()) -> 0(), first(X1, X2) -> n__first(X1, X2), first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))), first(0(), X) -> nil(), activate(X) -> X, activate(n__terms(X)) -> terms(X), activate(n__first(X1, X2)) -> first(X1, X2), half(s(s(X))) -> s(half(X)), half(s(0())) -> 0(), half(0()) -> 0(), half(dbl(X)) -> X} SPSC: Simple Projection: pi(activate#) = 0, pi(first#) = 1 Strict: {first#(s(X), cons(Y, Z)) -> activate#(Z)} EDG: {} SCCS: Qed SCC: Strict: {dbl#(s(X)) -> dbl#(X)} Weak: { sqr(s(X)) -> s(add(sqr(X), dbl(X))), sqr(0()) -> 0(), terms(N) -> cons(recip(sqr(N)), n__terms(s(N))), terms(X) -> n__terms(X), add(s(X), Y) -> s(add(X, Y)), add(0(), X) -> X, dbl(s(X)) -> s(s(dbl(X))), dbl(0()) -> 0(), first(X1, X2) -> n__first(X1, X2), first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))), first(0(), X) -> nil(), activate(X) -> X, activate(n__terms(X)) -> terms(X), activate(n__first(X1, X2)) -> first(X1, X2), half(s(s(X))) -> s(half(X)), half(s(0())) -> 0(), half(0()) -> 0(), half(dbl(X)) -> X} SPSC: Simple Projection: pi(dbl#) = 0 Strict: {} Qed SCC: Strict: {add#(s(X), Y) -> add#(X, Y)} Weak: { sqr(s(X)) -> s(add(sqr(X), dbl(X))), sqr(0()) -> 0(), terms(N) -> cons(recip(sqr(N)), n__terms(s(N))), terms(X) -> n__terms(X), add(s(X), Y) -> s(add(X, Y)), add(0(), X) -> X, dbl(s(X)) -> s(s(dbl(X))), dbl(0()) -> 0(), first(X1, X2) -> n__first(X1, X2), first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))), first(0(), X) -> nil(), activate(X) -> X, activate(n__terms(X)) -> terms(X), activate(n__first(X1, X2)) -> first(X1, X2), half(s(s(X))) -> s(half(X)), half(s(0())) -> 0(), half(0()) -> 0(), half(dbl(X)) -> X} SPSC: Simple Projection: pi(add#) = 0 Strict: {} Qed SCC: Strict: {sqr#(s(X)) -> sqr#(X)} Weak: { sqr(s(X)) -> s(add(sqr(X), dbl(X))), sqr(0()) -> 0(), terms(N) -> cons(recip(sqr(N)), n__terms(s(N))), terms(X) -> n__terms(X), add(s(X), Y) -> s(add(X, Y)), add(0(), X) -> X, dbl(s(X)) -> s(s(dbl(X))), dbl(0()) -> 0(), first(X1, X2) -> n__first(X1, X2), first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))), first(0(), X) -> nil(), activate(X) -> X, activate(n__terms(X)) -> terms(X), activate(n__first(X1, X2)) -> first(X1, X2), half(s(s(X))) -> s(half(X)), half(s(0())) -> 0(), half(0()) -> 0(), half(dbl(X)) -> X} SPSC: Simple Projection: pi(sqr#) = 0 Strict: {} Qed