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

The program

(VAR N X Y)
(RULES 
terms(N) -> cons(recip(sqr(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)) -> cons(Y)
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend