Term Rewriting System R:

   [X, Y, Z]
   f(X) -> cons(X, f(g(X)))
   g(0) -> s(0)
   g(s(X)) -> s(s(g(X)))
   sel(0, cons(X, Y)) -> X
   sel(s(X), cons(Y, Z)) -> sel(X, Z)

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   G(s(X)) -> G(X)
   F(X) -> F(g(X))
   F(X) -> G(X)
   SEL(s(X), cons(Y, Z)) -> SEL(X, Z)

Furthermore, R contains three SCCs.


SCC1:

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

The following Dependency Pairs can be deleted:

   G(s(X)) -> G(X)



 This transformation is resulting in no new subcycles.


SCC2:

SEL(s(X), cons(Y, Z)) -> SEL(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(SEL(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:

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



 This transformation is resulting in no new subcycles.


SCC3:

F(X) -> F(g(X))

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


Non-Termination of R could be shown.

Duration: 0.542 seconds.