NO
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 QDP
↳5 TransformationProof (⇔, 0 ms)
↳6 QDP
↳7 TransformationProof (⇔, 0 ms)
↳8 QDP
↳9 DependencyGraphProof (⇔, 0 ms)
↳10 QDP
↳11 TransformationProof (⇔, 0 ms)
↳12 QDP
↳13 DependencyGraphProof (⇔, 0 ms)
↳14 QDP
↳15 TransformationProof (⇔, 0 ms)
↳16 QDP
↳17 NonTerminationLoopProof (⇒, 0 ms)
↳18 NO
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(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
FROM(X) → CONS(X, n__from(s(X)))
LENGTH(n__cons(X, Y)) → LENGTH1(activate(Y))
LENGTH(n__cons(X, Y)) → ACTIVATE(Y)
LENGTH1(X) → LENGTH(activate(X))
LENGTH1(X) → ACTIVATE(X)
ACTIVATE(n__from(X)) → FROM(X)
ACTIVATE(n__nil) → NIL
ACTIVATE(n__cons(X1, X2)) → CONS(X1, X2)
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(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
LENGTH(n__cons(X, Y)) → LENGTH1(activate(Y))
LENGTH1(X) → LENGTH(activate(X))
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(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
LENGTH1(n__from(x0)) → LENGTH(from(x0)) → LENGTH1(n__from(x0)) → LENGTH(from(x0))
LENGTH1(n__nil) → LENGTH(nil) → LENGTH1(n__nil) → LENGTH(nil)
LENGTH1(n__cons(x0, x1)) → LENGTH(cons(x0, x1)) → LENGTH1(n__cons(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH1(x0) → LENGTH(x0) → LENGTH1(x0) → LENGTH(x0)
LENGTH(n__cons(X, Y)) → LENGTH1(activate(Y))
LENGTH1(n__from(x0)) → LENGTH(from(x0))
LENGTH1(n__nil) → LENGTH(nil)
LENGTH1(n__cons(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH1(x0) → LENGTH(x0)
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(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
LENGTH1(n__from(x0)) → LENGTH(cons(x0, n__from(s(x0)))) → LENGTH1(n__from(x0)) → LENGTH(cons(x0, n__from(s(x0))))
LENGTH1(n__from(x0)) → LENGTH(n__from(x0)) → LENGTH1(n__from(x0)) → LENGTH(n__from(x0))
LENGTH(n__cons(X, Y)) → LENGTH1(activate(Y))
LENGTH1(n__nil) → LENGTH(nil)
LENGTH1(n__cons(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH1(x0) → LENGTH(x0)
LENGTH1(n__from(x0)) → LENGTH(cons(x0, n__from(s(x0))))
LENGTH1(n__from(x0)) → LENGTH(n__from(x0))
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(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
LENGTH1(n__nil) → LENGTH(nil)
LENGTH(n__cons(X, Y)) → LENGTH1(activate(Y))
LENGTH1(n__cons(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH1(x0) → LENGTH(x0)
LENGTH1(n__from(x0)) → LENGTH(cons(x0, n__from(s(x0))))
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(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
LENGTH1(n__nil) → LENGTH(n__nil) → LENGTH1(n__nil) → LENGTH(n__nil)
LENGTH(n__cons(X, Y)) → LENGTH1(activate(Y))
LENGTH1(n__cons(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH1(x0) → LENGTH(x0)
LENGTH1(n__from(x0)) → LENGTH(cons(x0, n__from(s(x0))))
LENGTH1(n__nil) → LENGTH(n__nil)
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(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
LENGTH1(n__cons(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH(n__cons(X, Y)) → LENGTH1(activate(Y))
LENGTH1(x0) → LENGTH(x0)
LENGTH1(n__from(x0)) → LENGTH(cons(x0, n__from(s(x0))))
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(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
LENGTH1(n__cons(x0, x1)) → LENGTH(n__cons(x0, x1)) → LENGTH1(n__cons(x0, x1)) → LENGTH(n__cons(x0, x1))
LENGTH(n__cons(X, Y)) → LENGTH1(activate(Y))
LENGTH1(x0) → LENGTH(x0)
LENGTH1(n__from(x0)) → LENGTH(cons(x0, n__from(s(x0))))
LENGTH1(n__cons(x0, x1)) → LENGTH(n__cons(x0, x1))
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(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