Term Rewriting System R:
[N, X, Y]
terms(N) -> cons(recip(sqr(N)))
sqr(0) -> 0
sqr(s) -> s
dbl(0) -> 0
dbl(s) -> s
add(0, X) -> X
add(s, Y) -> s
first(0, X) -> nil
first(s, cons(Y)) -> cons(Y)

Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

TERMS(N) -> SQR(N)

R contains no SCCs.

Termination of R successfully shown.
Duration:
0:00 minutes