Term Rewriting System R:

   [X, Y, X1, X2]
   from(X) -> cons(X, n__from(s(X)))
   from(X) -> n__from(X)
   length(n__nil) -> 0
   length(n__cons(X, Y)) -> s(length1(activate(Y)))
   length1(X) -> length(activate(X))
   nil -> n__nil
   cons(X1, X2) -> n__cons(X1, X2)
   activate(n__from(X)) -> from(X)
   activate(n__nil) -> nil
   activate(n__cons(X1, X2)) -> cons(X1, X2)
   activate(X) -> X

Termination of R to be shown.


R contains the following Dependency Pairs: 


   LENGTH(n__cons(X, Y)) -> LENGTH1(activate(Y))
   LENGTH(n__cons(X, Y)) -> ACTIVATE(Y)
   FROM(X) -> CONS(X, n__from(s(X)))
   LENGTH1(X) -> LENGTH(activate(X))
   LENGTH1(X) -> ACTIVATE(X)
   ACTIVATE(n__from(X)) -> FROM(X)
   ACTIVATE(n__cons(X1, X2)) -> CONS(X1, X2)
   ACTIVATE(n__nil) -> NIL

Furthermore, R contains one SCC.


SCC1:

LENGTH1(X) -> LENGTH(activate(X))
LENGTH(n__cons(X, Y)) -> LENGTH1(activate(Y))

On this Scc, a Narrowing SCC transformation can be performed.
 
As a result of transforming the rule 

   LENGTH1(X) -> LENGTH(activate(X))
four new Dependency Pairs
are created:


   LENGTH1(n__from(X'')) -> LENGTH(from(X''))
   LENGTH1(n__cons(X1', X2')) -> LENGTH(cons(X1', X2'))
   LENGTH1(X'') -> LENGTH(X'')
   LENGTH1(n__nil) -> LENGTH(nil)

The transformation is resulting in one subcycle:


SCC1.Nar1:

LENGTH1(n__nil) -> LENGTH(nil)
LENGTH1(X'') -> LENGTH(X'')
LENGTH1(n__cons(X1', X2')) -> LENGTH(cons(X1', X2'))
LENGTH1(n__from(X'')) -> LENGTH(from(X''))
LENGTH(n__cons(X, Y)) -> LENGTH1(activate(Y))

Found an infinite P-chain over R:
P = LENGTH1(n__nil) -> LENGTH(nil)
LENGTH1(X'') -> LENGTH(X'')
LENGTH1(n__cons(X1', X2')) -> LENGTH(cons(X1', X2'))
LENGTH1(n__from(X'')) -> LENGTH(from(X''))
LENGTH(n__cons(X, Y)) -> LENGTH1(activate(Y))
R = [cons(X1, X2) -> n__cons(X1, X2), length(n__nil) -> 0, length(n__cons(X, Y)) -> s(length1(activate(Y))), from(X) -> cons(X, n__from(s(X))), from(X) -> n__from(X), length1(X) -> length(activate(X)), activate(n__from(X)) -> from(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(X) -> X, activate(n__nil) -> nil, nil -> n__nil]
s = LENGTH1(n__cons(X', n__from(X''''))) evaluates to t = LENGTH1(n__cons(X'''', n__from(s(X''''))))
Thus, s starts an infinite reduction as s matches t.


Non-Termination of R could be shown.

Duration: 20.377 seconds.