Term Rewriting System R:

   [N, X, Y, XS]
   fib(N) -> sel(N, fib1(s(0), s(0)))
   fib1(X, Y) -> cons(X, fib1(Y, add(X, Y)))
   add(0, X) -> X
   add(s(X), Y) -> s(add(X, Y))
   sel(0, cons(X, XS)) -> X
   sel(s(N), cons(X, XS)) -> sel(N, XS)

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: 


   ADD(s(X), Y) -> ADD(X, Y)
   SEL(s(N), cons(X, XS)) -> SEL(N, XS)
   FIB(N) -> SEL(N, fib1(s(0), s(0)))
   FIB(N) -> FIB1(s(0), s(0))
   FIB1(X, Y) -> FIB1(Y, add(X, Y))
   FIB1(X, Y) -> ADD(X, Y)

Furthermore, R contains three 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:

SEL(s(N), cons(X, XS)) -> SEL(N, XS)

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(N), cons(X, XS)) -> SEL(N, XS)



 This transformation is resulting in no new subcycles.


SCC3:

FIB1(X, Y) -> FIB1(Y, add(X, Y))

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


Non-Termination of R could be shown.

Duration: 0.589 seconds.