/home/nowonder/forschung/aprove/TPDB05/TRS/nontermin/CSR/Ex26_Luc03b.trs

The program

(VAR N X Y Z)

(RULES 
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))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend