The rewrite relation of the following TRS is considered.
terms(N) | → | cons(recip(sqr(N)),terms(s(N))) | (1) |
sqr(0) | → | 0 | (2) |
sqr(s(X)) | → | s(add(sqr(X),dbl(X))) | (3) |
dbl(0) | → | 0 | (4) |
dbl(s(X)) | → | s(s(dbl(X))) | (5) |
add(0,X) | → | X | (6) |
add(s(X),Y) | → | s(add(X,Y)) | (7) |
first(0,X) | → | nil | (8) |
first(s(X),cons(Y,Z)) | → | cons(Y,first(X,Z)) | (9) |
half(0) | → | 0 | (10) |
half(s(0)) | → | 0 | (11) |
half(s(s(X))) | → | s(half(X)) | (12) |
half(dbl(X)) | → | X | (13) |
t0 | = | terms(N) |
→ | cons(recip(sqr(N)),terms(s(N))) | |
= | t1 |