Term Rewriting System R:

   [X, Y, X1, X2, L]
   a__eq(0, 0) -> true
   a__eq(s(X), s(Y)) -> a__eq(X, Y)
   a__eq(X, Y) -> false
   a__eq(X1, X2) -> eq(X1, X2)
   a__inf(X) -> cons(X, inf(s(X)))
   a__inf(X) -> inf(X)
   a__take(0, X) -> nil
   a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
   a__take(X1, X2) -> take(X1, X2)
   a__length(nil) -> 0
   a__length(cons(X, L)) -> s(length(L))
   a__length(X) -> length(X)
   mark(eq(X1, X2)) -> a__eq(X1, X2)
   mark(inf(X)) -> a__inf(mark(X))
   mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
   mark(length(X)) -> a__length(mark(X))
   mark(0) -> 0
   mark(true) -> true
   mark(s(X)) -> s(X)
   mark(false) -> false
   mark(cons(X1, X2)) -> cons(X1, X2)
   mark(nil) -> nil

Termination of R to be shown.


R contains the following Dependency Pairs: 


   A__EQ(s(X), s(Y)) -> A__EQ(X, Y)
   MARK(eq(X1, X2)) -> A__EQ(X1, X2)
   MARK(inf(X)) -> A__INF(mark(X))
   MARK(inf(X)) -> MARK(X)
   MARK(length(X)) -> A__LENGTH(mark(X))
   MARK(length(X)) -> MARK(X)
   MARK(take(X1, X2)) -> A__TAKE(mark(X1), mark(X2))
   MARK(take(X1, X2)) -> MARK(X1)
   MARK(take(X1, X2)) -> MARK(X2)

Furthermore, R contains two SCCs.


SCC1:

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

The following Dependency Pairs can be deleted:

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



 This transformation is resulting in no new subcycles.


SCC2:

MARK(take(X1, X2)) -> MARK(X2)
MARK(take(X1, X2)) -> MARK(X1)
MARK(length(X)) -> MARK(X)
MARK(inf(X)) -> MARK(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(length(x_1)) = 1 + x_1
POL(take(x_1, x_2)) = 1 + x_1 + x_2
POL(MARK(x_1)) = 1 + x_1
POL(inf(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   MARK(take(X1, X2)) -> MARK(X2)
   MARK(take(X1, X2)) -> MARK(X1)
   MARK(length(X)) -> MARK(X)
   MARK(inf(X)) -> MARK(X)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 0.951 seconds.