Term Rewriting System R:

   [N, X, Y, Z]
   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))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(X))) -> s(half(X))
   half(dbl(X)) -> X

Termination of R to be shown.


R contains the following Dependency Pairs: 


   ADD(s(X), Y) -> ADD(X, Y)
   HALF(s(s(X))) -> HALF(X)
   SQR(s(X)) -> ADD(sqr(X), dbl(X))
   SQR(s(X)) -> SQR(X)
   SQR(s(X)) -> DBL(X)
   DBL(s(X)) -> DBL(X)
   FIRST(s(X), cons(Y, Z)) -> FIRST(X, Z)
   TERMS(N) -> SQR(N)
   TERMS(N) -> TERMS(s(N))

Furthermore, R contains six SCCs.


SCC1:

ADD(s(X), Y) -> ADD(X, Y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(ADD(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   ADD(s(X), Y) -> ADD(X, Y)



 This transformation is resulting in no new subcycles.


SCC2:

HALF(s(s(X))) -> HALF(X)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(HALF(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   HALF(s(s(X))) -> HALF(X)



 This transformation is resulting in no new subcycles.


SCC3:

DBL(s(X)) -> DBL(X)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(DBL(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   DBL(s(X)) -> DBL(X)



 This transformation is resulting in no new subcycles.


SCC4:

FIRST(s(X), cons(Y, Z)) -> FIRST(X, Z)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(FIRST(x_1, x_2)) = 1 + x_1 + x_2
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   FIRST(s(X), cons(Y, Z)) -> FIRST(X, Z)



 This transformation is resulting in no new subcycles.


SCC5:

SQR(s(X)) -> SQR(X)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(SQR(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   SQR(s(X)) -> SQR(X)



 This transformation is resulting in no new subcycles.


SCC6:

TERMS(N) -> TERMS(s(N))

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = x_1
POL(TERMS(x_1)) = 1 + x_1

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   add(0, X) -> X
   add(s(X), Y) -> s(add(X, Y))
   half(0) -> 0
   half(s(0)) -> 0
   half(dbl(X)) -> X
   half(s(s(X))) -> s(half(X))
   sqr(0) -> 0
   sqr(s(X)) -> s(add(sqr(X), dbl(X)))
   dbl(0) -> 0
   dbl(s(X)) -> s(s(dbl(X)))
   first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
   first(0, X) -> nil
   terms(N) -> cons(recip(sqr(N)), terms(s(N)))


 This transformation is resulting in one new subcycle:


SCC6.MRR1:

TERMS(N) -> TERMS(s(N))

Applying the non-overlappingness check to the DPs.

The transformation is resulting in one subcycle:

SCC6.MRR1.NOC1:

TERMS(N) -> TERMS(s(N))

Found an infinite P-chain over R:
P = TERMS(N) -> TERMS(s(N))
R = []
s = TERMS(N) evaluates to t = TERMS(s(N))
Thus, s starts an infinite reduction as s matches t.


Non-Termination of R could be shown.

Duration: 0.772 seconds.