The TRS could not be proven terminating. The proof attempt took 60001 ms.
Problem 1 was processed with processor DependencyGraph (1562ms). | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (709ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (560ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (601ms), ReductionPairSAT (13012ms), DependencyGraph (577ms), SizeChangePrinciple (timeout)].
| take#(s(M), cons(N, IL)) | → | isNatIList#(activate(IL)) | isNatList#(n__take(N, IL)) | → | isNat#(activate(N)) | |
| length#(cons(N, L)) | → | isNat#(N) | activate#(n__length(X)) | → | activate#(X) | |
| isNatList#(n__take(N, IL)) | → | activate#(IL) | activate#(n__s(X)) | → | activate#(X) | |
| uLength#(tt, L) | → | length#(activate(L)) | isNatList#(n__take(N, IL)) | → | isNatIList#(activate(IL)) | |
| uTake2#(tt, M, N, IL) | → | activate#(IL) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| isNat#(n__length(L)) | → | isNatList#(activate(L)) | isNatList#(n__cons(N, L)) | → | isNatList#(activate(L)) | |
| uTake2#(tt, M, N, IL) | → | activate#(M) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| isNatIList#(IL) | → | activate#(IL) | isNatIList#(n__cons(N, IL)) | → | isNat#(activate(N)) | |
| isNat#(n__s(N)) | → | isNat#(activate(N)) | take#(s(M), cons(N, IL)) | → | isNat#(N) | |
| isNatList#(n__cons(N, L)) | → | activate#(L) | activate#(n__take(X1, X2)) | → | activate#(X2) | |
| isNat#(n__length(L)) | → | activate#(L) | length#(cons(N, L)) | → | uLength#(and(isNat(N), isNatList(activate(L))), activate(L)) | |
| isNatList#(n__take(N, IL)) | → | activate#(N) | isNatList#(n__cons(N, L)) | → | activate#(N) | |
| isNatIList#(n__cons(N, IL)) | → | isNatIList#(activate(IL)) | isNatIList#(IL) | → | isNatList#(activate(IL)) | |
| uLength#(tt, L) | → | activate#(L) | isNat#(n__s(N)) | → | activate#(N) | |
| take#(s(M), cons(N, IL)) | → | uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)) | activate#(n__length(X)) | → | length#(activate(X)) | |
| isNatIList#(n__cons(N, IL)) | → | activate#(IL) | uTake2#(tt, M, N, IL) | → | activate#(N) | |
| length#(cons(N, L)) | → | isNatList#(activate(L)) | isNatList#(n__cons(N, L)) | → | isNat#(activate(N)) | |
| activate#(n__take(X1, X2)) | → | activate#(X1) | isNatIList#(n__cons(N, IL)) | → | activate#(N) | |
| take#(s(M), cons(N, IL)) | → | activate#(IL) | take#(0, IL) | → | isNatIList#(IL) | |
| take#(s(M), cons(N, IL)) | → | isNat#(M) | length#(cons(N, L)) | → | activate#(L) |
| and(tt, T) | → | T | isNatIList(IL) | → | isNatList(activate(IL)) | |
| isNat(n__0) | → | tt | isNat(n__s(N)) | → | isNat(activate(N)) | |
| isNat(n__length(L)) | → | isNatList(activate(L)) | isNatIList(n__zeros) | → | tt | |
| isNatIList(n__cons(N, IL)) | → | and(isNat(activate(N)), isNatIList(activate(IL))) | isNatList(n__nil) | → | tt | |
| isNatList(n__cons(N, L)) | → | and(isNat(activate(N)), isNatList(activate(L))) | isNatList(n__take(N, IL)) | → | and(isNat(activate(N)), isNatIList(activate(IL))) | |
| zeros | → | cons(0, n__zeros) | take(0, IL) | → | uTake1(isNatIList(IL)) | |
| uTake1(tt) | → | nil | take(s(M), cons(N, IL)) | → | uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)) | |
| uTake2(tt, M, N, IL) | → | cons(activate(N), n__take(activate(M), activate(IL))) | length(cons(N, L)) | → | uLength(and(isNat(N), isNatList(activate(L))), activate(L)) | |
| uLength(tt, L) | → | s(length(activate(L))) | 0 | → | n__0 | |
| s(X) | → | n__s(X) | length(X) | → | n__length(X) | |
| zeros | → | n__zeros | cons(X1, X2) | → | n__cons(X1, X2) | |
| nil | → | n__nil | take(X1, X2) | → | n__take(X1, X2) | |
| activate(n__0) | → | 0 | activate(n__s(X)) | → | s(activate(X)) | |
| activate(n__length(X)) | → | length(activate(X)) | activate(n__zeros) | → | zeros | |
| activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | activate(n__nil) | → | nil | |
| activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) | activate(X) | → | X |
Termination of terms over the following signature is verified: isNatIList, uLength, n__length, n__take, and, uTake1, activate, isNat, n__s, n__cons, uTake2, 0, n__0, s, isNatList, zeros, tt, take, length, n__nil, n__zeros, nil, cons
| take#(s(M), cons(N, IL)) | → | isNatIList#(activate(IL)) | isNatList#(n__take(N, IL)) | → | isNat#(activate(N)) | |
| zeros# | → | 0# | uLength#(tt, L) | → | length#(activate(L)) | |
| uTake1#(tt) | → | nil# | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| uTake2#(tt, M, N, IL) | → | activate#(IL) | activate#(n__cons(X1, X2)) | → | cons#(activate(X1), X2) | |
| uTake2#(tt, M, N, IL) | → | activate#(M) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| take#(s(M), cons(N, IL)) | → | and#(isNat(N), isNatIList(activate(IL))) | isNat#(n__s(N)) | → | isNat#(activate(N)) | |
| isNatList#(n__cons(N, L)) | → | activate#(L) | isNat#(n__length(L)) | → | activate#(L) | |
| isNatList#(n__take(N, IL)) | → | activate#(N) | uLength#(tt, L) | → | s#(length(activate(L))) | |
| isNatList#(n__cons(N, L)) | → | activate#(N) | isNatIList#(n__cons(N, IL)) | → | and#(isNat(activate(N)), isNatIList(activate(IL))) | |
| isNatIList#(IL) | → | isNatList#(activate(IL)) | uLength#(tt, L) | → | activate#(L) | |
| isNat#(n__s(N)) | → | activate#(N) | take#(s(M), cons(N, IL)) | → | uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)) | |
| activate#(n__length(X)) | → | length#(activate(X)) | length#(cons(N, L)) | → | isNatList#(activate(L)) | |
| uTake2#(tt, M, N, IL) | → | activate#(N) | isNatIList#(n__cons(N, IL)) | → | activate#(N) | |
| activate#(n__0) | → | 0# | take#(s(M), cons(N, IL)) | → | activate#(IL) | |
| activate#(n__zeros) | → | zeros# | length#(cons(N, L)) | → | isNat#(N) | |
| activate#(n__length(X)) | → | activate#(X) | isNatList#(n__take(N, IL)) | → | activate#(IL) | |
| activate#(n__s(X)) | → | activate#(X) | take#(s(M), cons(N, IL)) | → | and#(isNat(M), and(isNat(N), isNatIList(activate(IL)))) | |
| isNatList#(n__take(N, IL)) | → | isNatIList#(activate(IL)) | uTake2#(tt, M, N, IL) | → | cons#(activate(N), n__take(activate(M), activate(IL))) | |
| isNat#(n__length(L)) | → | isNatList#(activate(L)) | isNatList#(n__cons(N, L)) | → | isNatList#(activate(L)) | |
| isNatIList#(IL) | → | activate#(IL) | isNatIList#(n__cons(N, IL)) | → | isNat#(activate(N)) | |
| take#(s(M), cons(N, IL)) | → | isNat#(N) | activate#(n__take(X1, X2)) | → | activate#(X2) | |
| length#(cons(N, L)) | → | uLength#(and(isNat(N), isNatList(activate(L))), activate(L)) | zeros# | → | cons#(0, n__zeros) | |
| length#(cons(N, L)) | → | and#(isNat(N), isNatList(activate(L))) | isNatIList#(n__cons(N, IL)) | → | isNatIList#(activate(IL)) | |
| take#(0, IL) | → | uTake1#(isNatIList(IL)) | isNatList#(n__cons(N, L)) | → | and#(isNat(activate(N)), isNatList(activate(L))) | |
| isNatIList#(n__cons(N, IL)) | → | activate#(IL) | activate#(n__nil) | → | nil# | |
| isNatList#(n__cons(N, L)) | → | isNat#(activate(N)) | activate#(n__take(X1, X2)) | → | activate#(X1) | |
| isNatList#(n__take(N, IL)) | → | and#(isNat(activate(N)), isNatIList(activate(IL))) | activate#(n__s(X)) | → | s#(activate(X)) | |
| take#(0, IL) | → | isNatIList#(IL) | take#(s(M), cons(N, IL)) | → | isNat#(M) | |
| length#(cons(N, L)) | → | activate#(L) |
| and(tt, T) | → | T | isNatIList(IL) | → | isNatList(activate(IL)) | |
| isNat(n__0) | → | tt | isNat(n__s(N)) | → | isNat(activate(N)) | |
| isNat(n__length(L)) | → | isNatList(activate(L)) | isNatIList(n__zeros) | → | tt | |
| isNatIList(n__cons(N, IL)) | → | and(isNat(activate(N)), isNatIList(activate(IL))) | isNatList(n__nil) | → | tt | |
| isNatList(n__cons(N, L)) | → | and(isNat(activate(N)), isNatList(activate(L))) | isNatList(n__take(N, IL)) | → | and(isNat(activate(N)), isNatIList(activate(IL))) | |
| zeros | → | cons(0, n__zeros) | take(0, IL) | → | uTake1(isNatIList(IL)) | |
| uTake1(tt) | → | nil | take(s(M), cons(N, IL)) | → | uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)) | |
| uTake2(tt, M, N, IL) | → | cons(activate(N), n__take(activate(M), activate(IL))) | length(cons(N, L)) | → | uLength(and(isNat(N), isNatList(activate(L))), activate(L)) | |
| uLength(tt, L) | → | s(length(activate(L))) | 0 | → | n__0 | |
| s(X) | → | n__s(X) | length(X) | → | n__length(X) | |
| zeros | → | n__zeros | cons(X1, X2) | → | n__cons(X1, X2) | |
| nil | → | n__nil | take(X1, X2) | → | n__take(X1, X2) | |
| activate(n__0) | → | 0 | activate(n__s(X)) | → | s(activate(X)) | |
| activate(n__length(X)) | → | length(activate(X)) | activate(n__zeros) | → | zeros | |
| activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | activate(n__nil) | → | nil | |
| activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) | activate(X) | → | X |
Termination of terms over the following signature is verified: isNatIList, uLength, n__length, n__take, and, uTake1, activate, isNat, n__s, n__cons, uTake2, 0, n__0, isNatList, s, tt, zeros, take, length, n__nil, n__zeros, cons, nil
| take#(s(M), cons(N, IL)) → isNatIList#(activate(IL)) | isNatList#(n__take(N, IL)) → isNat#(activate(N)) |
| length#(cons(N, L)) → isNat#(N) | activate#(n__length(X)) → activate#(X) |
| isNatList#(n__take(N, IL)) → activate#(IL) | activate#(n__s(X)) → activate#(X) |
| uLength#(tt, L) → length#(activate(L)) | isNatList#(n__take(N, IL)) → isNatIList#(activate(IL)) |
| activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) | uTake2#(tt, M, N, IL) → activate#(IL) |
| isNat#(n__length(L)) → isNatList#(activate(L)) | isNatList#(n__cons(N, L)) → isNatList#(activate(L)) |
| uTake2#(tt, M, N, IL) → activate#(M) | activate#(n__cons(X1, X2)) → activate#(X1) |
| isNatIList#(IL) → activate#(IL) | isNatIList#(n__cons(N, IL)) → isNat#(activate(N)) |
| isNat#(n__s(N)) → isNat#(activate(N)) | take#(s(M), cons(N, IL)) → isNat#(N) |
| isNatList#(n__cons(N, L)) → activate#(L) | isNat#(n__length(L)) → activate#(L) |
| activate#(n__take(X1, X2)) → activate#(X2) | length#(cons(N, L)) → uLength#(and(isNat(N), isNatList(activate(L))), activate(L)) |
| isNatList#(n__take(N, IL)) → activate#(N) | isNatIList#(n__cons(N, IL)) → isNatIList#(activate(IL)) |
| isNatList#(n__cons(N, L)) → activate#(N) | isNatIList#(IL) → isNatList#(activate(IL)) |
| isNat#(n__s(N)) → activate#(N) | uLength#(tt, L) → activate#(L) |
| take#(s(M), cons(N, IL)) → uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)) | activate#(n__length(X)) → length#(activate(X)) |
| isNatIList#(n__cons(N, IL)) → activate#(IL) | length#(cons(N, L)) → isNatList#(activate(L)) |
| uTake2#(tt, M, N, IL) → activate#(N) | isNatList#(n__cons(N, L)) → isNat#(activate(N)) |
| activate#(n__take(X1, X2)) → activate#(X1) | isNatIList#(n__cons(N, IL)) → activate#(N) |
| take#(s(M), cons(N, IL)) → activate#(IL) | take#(0, IL) → isNatIList#(IL) |
| take#(s(M), cons(N, IL)) → isNat#(M) | length#(cons(N, L)) → activate#(L) |