/home/nowonder/forschung/aprove/TPDB05/TRS/TRCSR/ExSec11_1_Luc02a_Z.trs

The program

(VAR N X Y Z X1 X2)
(RULES 
terms(N) -> cons(recip(sqr(N)),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,n__first(X,activate(Z)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(X))) -> s(half(X))
half(dbl(X)) -> X
terms(X) -> n__terms(X)
first(X1,X2) -> n__first(X1,X2)
activate(n__terms(X)) -> terms(X)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(X) -> X
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend