Term Rewriting System R:
[N, X, Y, X1, X2, Z]
terms(N) -> cons(recip(sqr(N)), nterms(s(N)))
terms(X) -> nterms(X)
sqr(0) -> 0
sqr(s(X)) -> s(nadd(sqr(activate(X)), dbl(activate(X))))
dbl(0) -> 0
dbl(s(X)) -> s(ns(ndbl(activate(X))))
dbl(X) -> ndbl(X)
add(0, X) -> X
add(s(X), Y) -> s(nadd(activate(X), Y))
add(X1, X2) -> nadd(X1, X2)
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, nfirst(activate(X), activate(Z)))
first(X1, X2) -> nfirst(X1, X2)
s(X) -> ns(X)
activate(nterms(X)) -> terms(X)
activate(nadd(X1, X2)) -> add(X1, X2)
activate(ns(X)) -> s(X)
activate(ndbl(X)) -> dbl(X)
activate(nfirst(X1, X2)) -> first(X1, X2)
activate(X) -> X
Innermost Termination of R to be shown.
R
↳Removing Redundant Rules for Innermost Termination
Removing the following rules from R which left hand sides contain non normal subterms
sqr(s(X)) -> s(nadd(sqr(activate(X)), dbl(activate(X))))
dbl(s(X)) -> s(ns(ndbl(activate(X))))
add(s(X), Y) -> s(nadd(activate(X), Y))
first(s(X), cons(Y, Z)) -> cons(Y, nfirst(activate(X), activate(Z)))
R
↳RRRI
→TRS2
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
terms(N) -> cons(recip(sqr(N)), nterms(s(N)))
terms(X) -> nterms(X)
where the Polynomial interpretation:
| POL(activate(x1)) | = 2·x1 |
| POL(n__terms(x1)) | = 1 + x1 |
| POL(sqr(x1)) | = x1 |
| POL(n__s(x1)) | = x1 |
| POL(terms(x1)) | = 2 + 2·x1 |
| POL(n__dbl(x1)) | = x1 |
| POL(add(x1, x2)) | = x1 + x2 |
| POL(0) | = 0 |
| POL(first(x1, x2)) | = x1 + x2 |
| POL(cons(x1, x2)) | = x1 + x2 |
| POL(dbl(x1)) | = x1 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(recip(x1)) | = x1 |
| POL(n__add(x1, x2)) | = x1 + x2 |
| POL(n__first(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRI
→TRS2
↳RRRPolo
→TRS3
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
add(X1, X2) -> nadd(X1, X2)
add(0, X) -> X
where the Polynomial interpretation:
| POL(activate(x1)) | = 2·x1 |
| POL(n__terms(x1)) | = x1 |
| POL(sqr(x1)) | = x1 |
| POL(n__s(x1)) | = x1 |
| POL(terms(x1)) | = x1 |
| POL(n__dbl(x1)) | = x1 |
| POL(add(x1, x2)) | = 2 + x1 + x2 |
| POL(0) | = 0 |
| POL(first(x1, x2)) | = x1 + x2 |
| POL(dbl(x1)) | = x1 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(n__add(x1, x2)) | = 1 + x1 + x2 |
| POL(n__first(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRI
→TRS2
↳RRRPolo
→TRS3
↳RRRPolo
...
→TRS4
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
dbl(X) -> ndbl(X)
dbl(0) -> 0
where the Polynomial interpretation:
| POL(activate(x1)) | = 2·x1 |
| POL(n__terms(x1)) | = x1 |
| POL(sqr(x1)) | = x1 |
| POL(n__s(x1)) | = x1 |
| POL(terms(x1)) | = x1 |
| POL(n__dbl(x1)) | = 1 + x1 |
| POL(add(x1, x2)) | = x1 + x2 |
| POL(0) | = 0 |
| POL(first(x1, x2)) | = x1 + x2 |
| POL(dbl(x1)) | = 2 + x1 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(n__add(x1, x2)) | = x1 + x2 |
| POL(n__first(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRI
→TRS2
↳RRRPolo
→TRS3
↳RRRPolo
...
→TRS5
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
first(X1, X2) -> nfirst(X1, X2)
first(0, X) -> nil
activate(nadd(X1, X2)) -> add(X1, X2)
activate(ns(X)) -> s(X)
activate(X) -> X
activate(ndbl(X)) -> dbl(X)
activate(nterms(X)) -> terms(X)
where the Polynomial interpretation:
| POL(activate(x1)) | = 1 + x1 |
| POL(n__terms(x1)) | = x1 |
| POL(sqr(x1)) | = x1 |
| POL(n__s(x1)) | = x1 |
| POL(terms(x1)) | = x1 |
| POL(n__dbl(x1)) | = x1 |
| POL(add(x1, x2)) | = x1 + x2 |
| POL(first(x1, x2)) | = 1 + x1 + x2 |
| POL(0) | = 0 |
| POL(dbl(x1)) | = x1 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(n__add(x1, x2)) | = x1 + x2 |
| POL(n__first(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRI
→TRS2
↳RRRPolo
→TRS3
↳RRRPolo
...
→TRS6
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
sqr(0) -> 0
where the Polynomial interpretation:
| POL(activate(x1)) | = x1 |
| POL(first(x1, x2)) | = x1 + x2 |
| POL(0) | = 0 |
| POL(sqr(x1)) | = 1 + x1 |
| POL(n__s(x1)) | = x1 |
| POL(s(x1)) | = x1 |
| POL(n__first(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRI
→TRS2
↳RRRPolo
→TRS3
↳RRRPolo
...
→TRS7
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
s(X) -> ns(X)
where the Polynomial interpretation:
| POL(activate(x1)) | = x1 |
| POL(first(x1, x2)) | = x1 + x2 |
| POL(n__s(x1)) | = x1 |
| POL(s(x1)) | = 1 + x1 |
| POL(n__first(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRI
→TRS2
↳RRRPolo
→TRS3
↳RRRPolo
...
→TRS8
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
activate(nfirst(X1, X2)) -> first(X1, X2)
where the Polynomial interpretation:
| POL(activate(x1)) | = 1 + x1 |
| POL(first(x1, x2)) | = x1 + x2 |
| POL(n__first(x1, x2)) | = x1 + x2 |
was used.
All Rules of R can be deleted.
R
↳RRRI
→TRS2
↳RRRPolo
→TRS3
↳RRRPolo
...
→TRS9
↳Dependency Pair Analysis
R contains no Dependency Pairs and therefore no SCCs.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes