MAYBE Problem: terms(N) -> cons(recip(sqr(N)),terms(s(N))) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) Proof: DP Processor: DPs: terms#(N) -> terms#(s(N)) terms#(N) -> sqr#(N) sqr#(s(X)) -> dbl#(X) sqr#(s(X)) -> sqr#(X) sqr#(s(X)) -> add#(sqr(X),dbl(X)) dbl#(s(X)) -> dbl#(X) add#(s(X),Y) -> add#(X,Y) first#(s(X),cons(Y,Z)) -> first#(X,Z) TRS: terms(N) -> cons(recip(sqr(N)),terms(s(N))) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) TDG Processor: DPs: terms#(N) -> terms#(s(N)) terms#(N) -> sqr#(N) sqr#(s(X)) -> dbl#(X) sqr#(s(X)) -> sqr#(X) sqr#(s(X)) -> add#(sqr(X),dbl(X)) dbl#(s(X)) -> dbl#(X) add#(s(X),Y) -> add#(X,Y) first#(s(X),cons(Y,Z)) -> first#(X,Z) TRS: terms(N) -> cons(recip(sqr(N)),terms(s(N))) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) graph: first#(s(X),cons(Y,Z)) -> first#(X,Z) -> first#(s(X),cons(Y,Z)) -> first#(X,Z) add#(s(X),Y) -> add#(X,Y) -> add#(s(X),Y) -> add#(X,Y) dbl#(s(X)) -> dbl#(X) -> dbl#(s(X)) -> dbl#(X) sqr#(s(X)) -> add#(sqr(X),dbl(X)) -> add#(s(X),Y) -> add#(X,Y) sqr#(s(X)) -> dbl#(X) -> dbl#(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) sqr#(s(X)) -> sqr#(X) -> sqr#(s(X)) -> dbl#(X) terms#(N) -> sqr#(N) -> sqr#(s(X)) -> add#(sqr(X),dbl(X)) terms#(N) -> sqr#(N) -> sqr#(s(X)) -> sqr#(X) terms#(N) -> sqr#(N) -> sqr#(s(X)) -> dbl#(X) terms#(N) -> terms#(s(N)) -> terms#(N) -> sqr#(N) terms#(N) -> terms#(s(N)) -> terms#(N) -> terms#(s(N)) SCC Processor: #sccs: 5 #rules: 5 #arcs: 13/64 DPs: terms#(N) -> terms#(s(N)) TRS: terms(N) -> cons(recip(sqr(N)),terms(s(N))) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) Open DPs: sqr#(s(X)) -> sqr#(X) TRS: terms(N) -> cons(recip(sqr(N)),terms(s(N))) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) Open DPs: dbl#(s(X)) -> dbl#(X) TRS: terms(N) -> cons(recip(sqr(N)),terms(s(N))) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) Open DPs: add#(s(X),Y) -> add#(X,Y) TRS: terms(N) -> cons(recip(sqr(N)),terms(s(N))) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) Open DPs: first#(s(X),cons(Y,Z)) -> first#(X,Z) TRS: terms(N) -> cons(recip(sqr(N)),terms(s(N))) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) Open