Term Rewriting System R:

   [X, Y, L]
   eq(0, 0) -> true
   eq(s(X), s(Y)) -> eq(X, Y)
   eq(X, Y) -> false
   inf(X) -> cons(X, inf(s(X)))
   take(0, X) -> nil
   take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
   length(nil) -> 0
   length(cons(X, L)) -> s(length(L))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   EQ(s(X), s(Y)) -> EQ(X, Y)
   LENGTH(cons(X, L)) -> LENGTH(L)
   TAKE(s(X), cons(Y, L)) -> TAKE(X, L)
   INF(X) -> INF(s(X))

Furthermore, R contains four SCCs.


SCC1:

EQ(s(X), s(Y)) -> EQ(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(EQ(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

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



 This transformation is resulting in no new subcycles.


SCC2:

LENGTH(cons(X, L)) -> LENGTH(L)

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(LENGTH(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   LENGTH(cons(X, L)) -> LENGTH(L)



 This transformation is resulting in no new subcycles.


SCC3:

TAKE(s(X), cons(Y, L)) -> TAKE(X, L)

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(TAKE(x_1, x_2)) = 1 + x_1 + x_2
POL(s(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   TAKE(s(X), cons(Y, L)) -> TAKE(X, L)



 This transformation is resulting in no new subcycles.


SCC4:

INF(X) -> INF(s(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)) = x_1
POL(INF(x_1)) = 1 + x_1

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   eq(0, 0) -> true
   eq(s(X), s(Y)) -> eq(X, Y)
   eq(X, Y) -> false
   length(cons(X, L)) -> s(length(L))
   length(nil) -> 0
   take(0, X) -> nil
   take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
   inf(X) -> cons(X, inf(s(X)))


 This transformation is resulting in one new subcycle:


SCC4.MRR1:

INF(X) -> INF(s(X))

Applying the non-overlappingness check to the DPs.

The transformation is resulting in one subcycle:

SCC4.MRR1.NOC1:

INF(X) -> INF(s(X))

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


Non-Termination of R could be shown.

Duration: 0.592 seconds.