The TRS could not be proven terminating. The proof attempt took 60014 ms.
Problem 1 was processed with processor DependencyGraph (8468ms). | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (25ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (20ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (22ms), ReductionPairSAT (timeout)]. | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (2572ms), PolynomialLinearRange4iUR (45ms), DependencyGraph (2588ms), PolynomialLinearRange8NegiUR (26ms), DependencyGraph (2537ms)].
| U45#(tt, V2) | → | isNatIList#(activate(V2)) | U44#(tt, V1, V2) | → | U45#(isNat(activate(V1)), activate(V2)) | |
| U42#(tt, V1, V2) | → | U43#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | isNatIList#(n__cons(V1, V2)) | → | U41#(isNatKind(activate(V1)), activate(V1), activate(V2)) | |
| U43#(tt, V1, V2) | → | U44#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | U41#(tt, V1, V2) | → | U42#(isNatKind(activate(V1)), activate(V1), activate(V2)) |
| zeros | → | cons(0, n__zeros) | U11(tt, V1) | → | U12(isNatIListKind(activate(V1)), activate(V1)) | |
| U12(tt, V1) | → | U13(isNatList(activate(V1))) | U13(tt) | → | tt | |
| U21(tt, V1) | → | U22(isNatKind(activate(V1)), activate(V1)) | U22(tt, V1) | → | U23(isNat(activate(V1))) | |
| U23(tt) | → | tt | U31(tt, V) | → | U32(isNatIListKind(activate(V)), activate(V)) | |
| U32(tt, V) | → | U33(isNatList(activate(V))) | U33(tt) | → | tt | |
| U41(tt, V1, V2) | → | U42(isNatKind(activate(V1)), activate(V1), activate(V2)) | U42(tt, V1, V2) | → | U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | |
| U43(tt, V1, V2) | → | U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | U44(tt, V1, V2) | → | U45(isNat(activate(V1)), activate(V2)) | |
| U45(tt, V2) | → | U46(isNatIList(activate(V2))) | U46(tt) | → | tt | |
| U51(tt, V2) | → | U52(isNatIListKind(activate(V2))) | U52(tt) | → | tt | |
| U61(tt) | → | tt | U71(tt) | → | tt | |
| U81(tt, V1, V2) | → | U82(isNatKind(activate(V1)), activate(V1), activate(V2)) | U82(tt, V1, V2) | → | U83(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | |
| U83(tt, V1, V2) | → | U84(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | U84(tt, V1, V2) | → | U85(isNat(activate(V1)), activate(V2)) | |
| U85(tt, V2) | → | U86(isNatList(activate(V2))) | U86(tt) | → | tt | |
| U91(tt, L, N) | → | U92(isNatIListKind(activate(L)), activate(L), activate(N)) | U92(tt, L, N) | → | U93(isNat(activate(N)), activate(L), activate(N)) | |
| U93(tt, L, N) | → | U94(isNatKind(activate(N)), activate(L)) | U94(tt, L) | → | s(length(activate(L))) | |
| isNat(n__0) | → | tt | isNat(n__length(V1)) | → | U11(isNatIListKind(activate(V1)), activate(V1)) | |
| isNat(n__s(V1)) | → | U21(isNatKind(activate(V1)), activate(V1)) | isNatIList(V) | → | U31(isNatIListKind(activate(V)), activate(V)) | |
| isNatIList(n__zeros) | → | tt | isNatIList(n__cons(V1, V2)) | → | U41(isNatKind(activate(V1)), activate(V1), activate(V2)) | |
| isNatIListKind(n__nil) | → | tt | isNatIListKind(n__zeros) | → | tt | |
| isNatIListKind(n__cons(V1, V2)) | → | U51(isNatKind(activate(V1)), activate(V2)) | isNatKind(n__0) | → | tt | |
| isNatKind(n__length(V1)) | → | U61(isNatIListKind(activate(V1))) | isNatKind(n__s(V1)) | → | U71(isNatKind(activate(V1))) | |
| isNatList(n__nil) | → | tt | isNatList(n__cons(V1, V2)) | → | U81(isNatKind(activate(V1)), activate(V1), activate(V2)) | |
| length(nil) | → | 0 | length(cons(N, L)) | → | U91(isNatList(activate(L)), activate(L), N) | |
| zeros | → | n__zeros | 0 | → | n__0 | |
| length(X) | → | n__length(X) | s(X) | → | n__s(X) | |
| cons(X1, X2) | → | n__cons(X1, X2) | nil | → | n__nil | |
| activate(n__zeros) | → | zeros | activate(n__0) | → | 0 | |
| activate(n__length(X)) | → | length(activate(X)) | activate(n__s(X)) | → | s(activate(X)) | |
| activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | activate(n__nil) | → | nil | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: isNatIListKind, U94, n__s, activate, isNat, U46, U45, U44, n__0, U61, U43, U93, U42, U92, U41, U91, length, n__nil, U23, n__zeros, U21, cons, U22, isNatIList, n__length, isNatKind, U83, U84, U85, U86, U71, n__cons, 0, s, U51, isNatList, tt, zeros, U82, U81, U52, U11, U12, U13, U31, U32, U33, nil
| U91#(tt, L, N) | → | activate#(L) | U12#(tt, V1) | → | activate#(V1) | |
| U81#(tt, V1, V2) | → | isNatKind#(activate(V1)) | U83#(tt, V1, V2) | → | activate#(V2) | |
| U83#(tt, V1, V2) | → | activate#(V1) | U92#(tt, L, N) | → | U93#(isNat(activate(N)), activate(L), activate(N)) | |
| U21#(tt, V1) | → | isNatKind#(activate(V1)) | U11#(tt, V1) | → | U12#(isNatIListKind(activate(V1)), activate(V1)) | |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | U51#(tt, V2) | → | activate#(V2) | |
| isNat#(n__length(V1)) | → | activate#(V1) | U94#(tt, L) | → | activate#(L) | |
| U91#(tt, L, N) | → | activate#(N) | U91#(tt, L, N) | → | isNatIListKind#(activate(L)) | |
| isNat#(n__s(V1)) | → | activate#(V1) | isNatIListKind#(n__cons(V1, V2)) | → | activate#(V2) | |
| isNatList#(n__cons(V1, V2)) | → | activate#(V2) | isNatKind#(n__length(V1)) | → | isNatIListKind#(activate(V1)) | |
| isNatIListKind#(n__cons(V1, V2)) | → | isNatKind#(activate(V1)) | U84#(tt, V1, V2) | → | activate#(V2) | |
| U83#(tt, V1, V2) | → | U84#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | U92#(tt, L, N) | → | activate#(L) | |
| activate#(n__length(X)) | → | length#(activate(X)) | U82#(tt, V1, V2) | → | activate#(V1) | |
| length#(cons(N, L)) | → | isNatList#(activate(L)) | U22#(tt, V1) | → | activate#(V1) | |
| U12#(tt, V1) | → | isNatList#(activate(V1)) | U94#(tt, L) | → | length#(activate(L)) | |
| U83#(tt, V1, V2) | → | isNatIListKind#(activate(V2)) | isNatKind#(n__s(V1)) | → | isNatKind#(activate(V1)) | |
| isNatIListKind#(n__cons(V1, V2)) | → | activate#(V1) | U82#(tt, V1, V2) | → | U83#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | |
| isNat#(n__s(V1)) | → | U21#(isNatKind(activate(V1)), activate(V1)) | isNat#(n__s(V1)) | → | isNatKind#(activate(V1)) | |
| isNatIListKind#(n__cons(V1, V2)) | → | U51#(isNatKind(activate(V1)), activate(V2)) | U82#(tt, V1, V2) | → | isNatIListKind#(activate(V2)) | |
| activate#(n__length(X)) | → | activate#(X) | U22#(tt, V1) | → | isNat#(activate(V1)) | |
| activate#(n__s(X)) | → | activate#(X) | U92#(tt, L, N) | → | activate#(N) | |
| U93#(tt, L, N) | → | activate#(N) | isNatKind#(n__length(V1)) | → | activate#(V1) | |
| isNatKind#(n__s(V1)) | → | activate#(V1) | U51#(tt, V2) | → | isNatIListKind#(activate(V2)) | |
| isNatList#(n__cons(V1, V2)) | → | isNatKind#(activate(V1)) | U85#(tt, V2) | → | isNatList#(activate(V2)) | |
| isNatList#(n__cons(V1, V2)) | → | U81#(isNatKind(activate(V1)), activate(V1), activate(V2)) | U81#(tt, V1, V2) | → | U82#(isNatKind(activate(V1)), activate(V1), activate(V2)) | |
| U84#(tt, V1, V2) | → | isNat#(activate(V1)) | U84#(tt, V1, V2) | → | activate#(V1) | |
| U21#(tt, V1) | → | activate#(V1) | U81#(tt, V1, V2) | → | activate#(V2) | |
| U85#(tt, V2) | → | activate#(V2) | isNat#(n__length(V1)) | → | U11#(isNatIListKind(activate(V1)), activate(V1)) | |
| U11#(tt, V1) | → | activate#(V1) | U11#(tt, V1) | → | isNatIListKind#(activate(V1)) | |
| U84#(tt, V1, V2) | → | U85#(isNat(activate(V1)), activate(V2)) | U92#(tt, L, N) | → | isNat#(activate(N)) | |
| U93#(tt, L, N) | → | isNatKind#(activate(N)) | U91#(tt, L, N) | → | U92#(isNatIListKind(activate(L)), activate(L), activate(N)) | |
| length#(cons(N, L)) | → | U91#(isNatList(activate(L)), activate(L), N) | U21#(tt, V1) | → | U22#(isNatKind(activate(V1)), activate(V1)) | |
| U82#(tt, V1, V2) | → | activate#(V2) | isNatList#(n__cons(V1, V2)) | → | activate#(V1) | |
| U81#(tt, V1, V2) | → | activate#(V1) | U93#(tt, L, N) | → | activate#(L) | |
| isNat#(n__length(V1)) | → | isNatIListKind#(activate(V1)) | U93#(tt, L, N) | → | U94#(isNatKind(activate(N)), activate(L)) | |
| length#(cons(N, L)) | → | activate#(L) |
| zeros | → | cons(0, n__zeros) | U11(tt, V1) | → | U12(isNatIListKind(activate(V1)), activate(V1)) | |
| U12(tt, V1) | → | U13(isNatList(activate(V1))) | U13(tt) | → | tt | |
| U21(tt, V1) | → | U22(isNatKind(activate(V1)), activate(V1)) | U22(tt, V1) | → | U23(isNat(activate(V1))) | |
| U23(tt) | → | tt | U31(tt, V) | → | U32(isNatIListKind(activate(V)), activate(V)) | |
| U32(tt, V) | → | U33(isNatList(activate(V))) | U33(tt) | → | tt | |
| U41(tt, V1, V2) | → | U42(isNatKind(activate(V1)), activate(V1), activate(V2)) | U42(tt, V1, V2) | → | U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | |
| U43(tt, V1, V2) | → | U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | U44(tt, V1, V2) | → | U45(isNat(activate(V1)), activate(V2)) | |
| U45(tt, V2) | → | U46(isNatIList(activate(V2))) | U46(tt) | → | tt | |
| U51(tt, V2) | → | U52(isNatIListKind(activate(V2))) | U52(tt) | → | tt | |
| U61(tt) | → | tt | U71(tt) | → | tt | |
| U81(tt, V1, V2) | → | U82(isNatKind(activate(V1)), activate(V1), activate(V2)) | U82(tt, V1, V2) | → | U83(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | |
| U83(tt, V1, V2) | → | U84(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | U84(tt, V1, V2) | → | U85(isNat(activate(V1)), activate(V2)) | |
| U85(tt, V2) | → | U86(isNatList(activate(V2))) | U86(tt) | → | tt | |
| U91(tt, L, N) | → | U92(isNatIListKind(activate(L)), activate(L), activate(N)) | U92(tt, L, N) | → | U93(isNat(activate(N)), activate(L), activate(N)) | |
| U93(tt, L, N) | → | U94(isNatKind(activate(N)), activate(L)) | U94(tt, L) | → | s(length(activate(L))) | |
| isNat(n__0) | → | tt | isNat(n__length(V1)) | → | U11(isNatIListKind(activate(V1)), activate(V1)) | |
| isNat(n__s(V1)) | → | U21(isNatKind(activate(V1)), activate(V1)) | isNatIList(V) | → | U31(isNatIListKind(activate(V)), activate(V)) | |
| isNatIList(n__zeros) | → | tt | isNatIList(n__cons(V1, V2)) | → | U41(isNatKind(activate(V1)), activate(V1), activate(V2)) | |
| isNatIListKind(n__nil) | → | tt | isNatIListKind(n__zeros) | → | tt | |
| isNatIListKind(n__cons(V1, V2)) | → | U51(isNatKind(activate(V1)), activate(V2)) | isNatKind(n__0) | → | tt | |
| isNatKind(n__length(V1)) | → | U61(isNatIListKind(activate(V1))) | isNatKind(n__s(V1)) | → | U71(isNatKind(activate(V1))) | |
| isNatList(n__nil) | → | tt | isNatList(n__cons(V1, V2)) | → | U81(isNatKind(activate(V1)), activate(V1), activate(V2)) | |
| length(nil) | → | 0 | length(cons(N, L)) | → | U91(isNatList(activate(L)), activate(L), N) | |
| zeros | → | n__zeros | 0 | → | n__0 | |
| length(X) | → | n__length(X) | s(X) | → | n__s(X) | |
| cons(X1, X2) | → | n__cons(X1, X2) | nil | → | n__nil | |
| activate(n__zeros) | → | zeros | activate(n__0) | → | 0 | |
| activate(n__length(X)) | → | length(activate(X)) | activate(n__s(X)) | → | s(activate(X)) | |
| activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | activate(n__nil) | → | nil | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: isNatIListKind, U94, n__s, activate, isNat, U46, U45, U44, n__0, U61, U43, U93, U42, U92, U41, U91, length, n__nil, U23, n__zeros, U21, cons, U22, isNatIList, n__length, isNatKind, U83, U84, U85, U86, U71, n__cons, 0, s, U51, isNatList, tt, zeros, U82, U81, U52, U11, U12, U13, U31, U32, U33, nil
| U91#(tt, L, N) | → | activate#(L) | U81#(tt, V1, V2) | → | isNatKind#(activate(V1)) | |
| isNatIList#(V) | → | U31#(isNatIListKind(activate(V)), activate(V)) | U12#(tt, V1) | → | U13#(isNatList(activate(V1))) | |
| U51#(tt, V2) | → | U52#(isNatIListKind(activate(V2))) | U83#(tt, V1, V2) | → | activate#(V1) | |
| U92#(tt, L, N) | → | U93#(isNat(activate(N)), activate(L), activate(N)) | activate#(n__cons(X1, X2)) | → | cons#(activate(X1), X2) | |
| U94#(tt, L) | → | s#(length(activate(L))) | U31#(tt, V) | → | isNatIListKind#(activate(V)) | |
| U51#(tt, V2) | → | activate#(V2) | U94#(tt, L) | → | activate#(L) | |
| U91#(tt, L, N) | → | isNatIListKind#(activate(L)) | isNat#(n__length(V1)) | → | activate#(V1) | |
| isNatIListKind#(n__cons(V1, V2)) | → | activate#(V2) | length#(nil) | → | 0# | |
| U44#(tt, V1, V2) | → | isNat#(activate(V1)) | isNatIList#(n__cons(V1, V2)) | → | isNatKind#(activate(V1)) | |
| activate#(n__length(X)) | → | length#(activate(X)) | U92#(tt, L, N) | → | activate#(L) | |
| length#(cons(N, L)) | → | isNatList#(activate(L)) | U82#(tt, V1, V2) | → | activate#(V1) | |
| isNatIList#(n__cons(V1, V2)) | → | U41#(isNatKind(activate(V1)), activate(V1), activate(V2)) | isNatKind#(n__s(V1)) | → | isNatKind#(activate(V1)) | |
| isNatIListKind#(n__cons(V1, V2)) | → | activate#(V1) | isNat#(n__s(V1)) | → | isNatKind#(activate(V1)) | |
| isNatIList#(n__cons(V1, V2)) | → | activate#(V2) | U82#(tt, V1, V2) | → | isNatIListKind#(activate(V2)) | |
| activate#(n__zeros) | → | zeros# | activate#(n__s(X)) | → | activate#(X) | |
| U92#(tt, L, N) | → | activate#(N) | isNatKind#(n__length(V1)) | → | activate#(V1) | |
| U32#(tt, V) | → | isNatList#(activate(V)) | isNatKind#(n__s(V1)) | → | activate#(V1) | |
| isNatList#(n__cons(V1, V2)) | → | isNatKind#(activate(V1)) | U85#(tt, V2) | → | isNatList#(activate(V2)) | |
| U31#(tt, V) | → | activate#(V) | U31#(tt, V) | → | U32#(isNatIListKind(activate(V)), activate(V)) | |
| U32#(tt, V) | → | U33#(isNatList(activate(V))) | zeros# | → | cons#(0, n__zeros) | |
| isNatKind#(n__s(V1)) | → | U71#(isNatKind(activate(V1))) | U21#(tt, V1) | → | activate#(V1) | |
| U81#(tt, V1, V2) | → | activate#(V2) | U32#(tt, V) | → | activate#(V) | |
| U11#(tt, V1) | → | activate#(V1) | U41#(tt, V1, V2) | → | activate#(V2) | |
| U11#(tt, V1) | → | isNatIListKind#(activate(V1)) | U43#(tt, V1, V2) | → | activate#(V2) | |
| U93#(tt, L, N) | → | isNatKind#(activate(N)) | length#(cons(N, L)) | → | U91#(isNatList(activate(L)), activate(L), N) | |
| U44#(tt, V1, V2) | → | activate#(V2) | U21#(tt, V1) | → | U22#(isNatKind(activate(V1)), activate(V1)) | |
| isNatList#(n__cons(V1, V2)) | → | activate#(V1) | U82#(tt, V1, V2) | → | activate#(V2) | |
| U81#(tt, V1, V2) | → | activate#(V1) | isNat#(n__length(V1)) | → | isNatIListKind#(activate(V1)) | |
| activate#(n__s(X)) | → | s#(activate(X)) | U43#(tt, V1, V2) | → | U44#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | |
| U42#(tt, V1, V2) | → | isNatIListKind#(activate(V2)) | U12#(tt, V1) | → | activate#(V1) | |
| U83#(tt, V1, V2) | → | activate#(V2) | zeros# | → | 0# | |
| U21#(tt, V1) | → | isNatKind#(activate(V1)) | U45#(tt, V2) | → | activate#(V2) | |
| U45#(tt, V2) | → | isNatIList#(activate(V2)) | U11#(tt, V1) | → | U12#(isNatIListKind(activate(V1)), activate(V1)) | |
| U44#(tt, V1, V2) | → | U45#(isNat(activate(V1)), activate(V2)) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| U44#(tt, V1, V2) | → | activate#(V1) | U41#(tt, V1, V2) | → | isNatKind#(activate(V1)) | |
| U91#(tt, L, N) | → | activate#(N) | isNat#(n__s(V1)) | → | activate#(V1) | |
| isNatList#(n__cons(V1, V2)) | → | activate#(V2) | isNatIList#(V) | → | isNatIListKind#(activate(V)) | |
| isNatKind#(n__length(V1)) | → | isNatIListKind#(activate(V1)) | isNatIListKind#(n__cons(V1, V2)) | → | isNatKind#(activate(V1)) | |
| U42#(tt, V1, V2) | → | activate#(V1) | U84#(tt, V1, V2) | → | activate#(V2) | |
| U83#(tt, V1, V2) | → | U84#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | U42#(tt, V1, V2) | → | U43#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | |
| U41#(tt, V1, V2) | → | activate#(V1) | isNatKind#(n__length(V1)) | → | U61#(isNatIListKind(activate(V1))) | |
| U42#(tt, V1, V2) | → | activate#(V2) | U85#(tt, V2) | → | U86#(isNatList(activate(V2))) | |
| activate#(n__0) | → | 0# | U22#(tt, V1) | → | activate#(V1) | |
| U12#(tt, V1) | → | isNatList#(activate(V1)) | U83#(tt, V1, V2) | → | isNatIListKind#(activate(V2)) | |
| U94#(tt, L) | → | length#(activate(L)) | U82#(tt, V1, V2) | → | U83#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | |
| isNat#(n__s(V1)) | → | U21#(isNatKind(activate(V1)), activate(V1)) | U22#(tt, V1) | → | U23#(isNat(activate(V1))) | |
| isNatIListKind#(n__cons(V1, V2)) | → | U51#(isNatKind(activate(V1)), activate(V2)) | activate#(n__length(X)) | → | activate#(X) | |
| U22#(tt, V1) | → | isNat#(activate(V1)) | U45#(tt, V2) | → | U46#(isNatIList(activate(V2))) | |
| U93#(tt, L, N) | → | activate#(N) | U51#(tt, V2) | → | isNatIListKind#(activate(V2)) | |
| U81#(tt, V1, V2) | → | U82#(isNatKind(activate(V1)), activate(V1), activate(V2)) | isNatList#(n__cons(V1, V2)) | → | U81#(isNatKind(activate(V1)), activate(V1), activate(V2)) | |
| U84#(tt, V1, V2) | → | isNat#(activate(V1)) | isNatIList#(V) | → | activate#(V) | |
| U84#(tt, V1, V2) | → | activate#(V1) | U41#(tt, V1, V2) | → | U42#(isNatKind(activate(V1)), activate(V1), activate(V2)) | |
| U85#(tt, V2) | → | activate#(V2) | isNat#(n__length(V1)) | → | U11#(isNatIListKind(activate(V1)), activate(V1)) | |
| U43#(tt, V1, V2) | → | activate#(V1) | U84#(tt, V1, V2) | → | U85#(isNat(activate(V1)), activate(V2)) | |
| activate#(n__nil) | → | nil# | U92#(tt, L, N) | → | isNat#(activate(N)) | |
| U43#(tt, V1, V2) | → | isNatIListKind#(activate(V2)) | U91#(tt, L, N) | → | U92#(isNatIListKind(activate(L)), activate(L), activate(N)) | |
| U93#(tt, L, N) | → | activate#(L) | U93#(tt, L, N) | → | U94#(isNatKind(activate(N)), activate(L)) | |
| isNatIList#(n__cons(V1, V2)) | → | activate#(V1) | length#(cons(N, L)) | → | activate#(L) |
| zeros | → | cons(0, n__zeros) | U11(tt, V1) | → | U12(isNatIListKind(activate(V1)), activate(V1)) | |
| U12(tt, V1) | → | U13(isNatList(activate(V1))) | U13(tt) | → | tt | |
| U21(tt, V1) | → | U22(isNatKind(activate(V1)), activate(V1)) | U22(tt, V1) | → | U23(isNat(activate(V1))) | |
| U23(tt) | → | tt | U31(tt, V) | → | U32(isNatIListKind(activate(V)), activate(V)) | |
| U32(tt, V) | → | U33(isNatList(activate(V))) | U33(tt) | → | tt | |
| U41(tt, V1, V2) | → | U42(isNatKind(activate(V1)), activate(V1), activate(V2)) | U42(tt, V1, V2) | → | U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | |
| U43(tt, V1, V2) | → | U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | U44(tt, V1, V2) | → | U45(isNat(activate(V1)), activate(V2)) | |
| U45(tt, V2) | → | U46(isNatIList(activate(V2))) | U46(tt) | → | tt | |
| U51(tt, V2) | → | U52(isNatIListKind(activate(V2))) | U52(tt) | → | tt | |
| U61(tt) | → | tt | U71(tt) | → | tt | |
| U81(tt, V1, V2) | → | U82(isNatKind(activate(V1)), activate(V1), activate(V2)) | U82(tt, V1, V2) | → | U83(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | |
| U83(tt, V1, V2) | → | U84(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | U84(tt, V1, V2) | → | U85(isNat(activate(V1)), activate(V2)) | |
| U85(tt, V2) | → | U86(isNatList(activate(V2))) | U86(tt) | → | tt | |
| U91(tt, L, N) | → | U92(isNatIListKind(activate(L)), activate(L), activate(N)) | U92(tt, L, N) | → | U93(isNat(activate(N)), activate(L), activate(N)) | |
| U93(tt, L, N) | → | U94(isNatKind(activate(N)), activate(L)) | U94(tt, L) | → | s(length(activate(L))) | |
| isNat(n__0) | → | tt | isNat(n__length(V1)) | → | U11(isNatIListKind(activate(V1)), activate(V1)) | |
| isNat(n__s(V1)) | → | U21(isNatKind(activate(V1)), activate(V1)) | isNatIList(V) | → | U31(isNatIListKind(activate(V)), activate(V)) | |
| isNatIList(n__zeros) | → | tt | isNatIList(n__cons(V1, V2)) | → | U41(isNatKind(activate(V1)), activate(V1), activate(V2)) | |
| isNatIListKind(n__nil) | → | tt | isNatIListKind(n__zeros) | → | tt | |
| isNatIListKind(n__cons(V1, V2)) | → | U51(isNatKind(activate(V1)), activate(V2)) | isNatKind(n__0) | → | tt | |
| isNatKind(n__length(V1)) | → | U61(isNatIListKind(activate(V1))) | isNatKind(n__s(V1)) | → | U71(isNatKind(activate(V1))) | |
| isNatList(n__nil) | → | tt | isNatList(n__cons(V1, V2)) | → | U81(isNatKind(activate(V1)), activate(V1), activate(V2)) | |
| length(nil) | → | 0 | length(cons(N, L)) | → | U91(isNatList(activate(L)), activate(L), N) | |
| zeros | → | n__zeros | 0 | → | n__0 | |
| length(X) | → | n__length(X) | s(X) | → | n__s(X) | |
| cons(X1, X2) | → | n__cons(X1, X2) | nil | → | n__nil | |
| activate(n__zeros) | → | zeros | activate(n__0) | → | 0 | |
| activate(n__length(X)) | → | length(activate(X)) | activate(n__s(X)) | → | s(activate(X)) | |
| activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | activate(n__nil) | → | nil | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: isNatIListKind, U94, U46, isNat, activate, n__s, U45, U44, U43, U61, n__0, U42, U93, U92, U41, U91, length, n__nil, U23, n__zeros, U21, cons, U22, isNatIList, n__length, isNatKind, U83, U84, U85, U86, U71, n__cons, 0, isNatList, U51, s, zeros, tt, U82, U52, U81, U11, U12, U31, U13, U32, U33, nil
| U45#(tt, V2) → isNatIList#(activate(V2)) | U44#(tt, V1, V2) → U45#(isNat(activate(V1)), activate(V2)) |
| U42#(tt, V1, V2) → U43#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | isNatIList#(n__cons(V1, V2)) → U41#(isNatKind(activate(V1)), activate(V1), activate(V2)) |
| U43#(tt, V1, V2) → U44#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | U41#(tt, V1, V2) → U42#(isNatKind(activate(V1)), activate(V1), activate(V2)) |
| U91#(tt, L, N) → activate#(L) | U81#(tt, V1, V2) → isNatKind#(activate(V1)) |
| U12#(tt, V1) → activate#(V1) | U83#(tt, V1, V2) → activate#(V2) |
| U83#(tt, V1, V2) → activate#(V1) | U92#(tt, L, N) → U93#(isNat(activate(N)), activate(L), activate(N)) |
| U21#(tt, V1) → isNatKind#(activate(V1)) | U11#(tt, V1) → U12#(isNatIListKind(activate(V1)), activate(V1)) |
| activate#(n__cons(X1, X2)) → activate#(X1) | U51#(tt, V2) → activate#(V2) |
| isNat#(n__s(V1)) → activate#(V1) | U91#(tt, L, N) → isNatIListKind#(activate(L)) |
| U91#(tt, L, N) → activate#(N) | U94#(tt, L) → activate#(L) |
| isNat#(n__length(V1)) → activate#(V1) | isNatIListKind#(n__cons(V1, V2)) → activate#(V2) |
| isNatKind#(n__length(V1)) → isNatIListKind#(activate(V1)) | isNatList#(n__cons(V1, V2)) → activate#(V2) |
| isNatIListKind#(n__cons(V1, V2)) → isNatKind#(activate(V1)) | U84#(tt, V1, V2) → activate#(V2) |
| U83#(tt, V1, V2) → U84#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | activate#(n__length(X)) → length#(activate(X)) |
| U92#(tt, L, N) → activate#(L) | length#(cons(N, L)) → isNatList#(activate(L)) |
| U82#(tt, V1, V2) → activate#(V1) | U22#(tt, V1) → activate#(V1) |
| U12#(tt, V1) → isNatList#(activate(V1)) | U83#(tt, V1, V2) → isNatIListKind#(activate(V2)) |
| U94#(tt, L) → length#(activate(L)) | isNatIListKind#(n__cons(V1, V2)) → activate#(V1) |
| isNatKind#(n__s(V1)) → isNatKind#(activate(V1)) | isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1)) |
| U82#(tt, V1, V2) → U83#(isNatIListKind(activate(V2)), activate(V1), activate(V2)) | isNat#(n__s(V1)) → isNatKind#(activate(V1)) |
| isNatIListKind#(n__cons(V1, V2)) → U51#(isNatKind(activate(V1)), activate(V2)) | U82#(tt, V1, V2) → isNatIListKind#(activate(V2)) |
| activate#(n__length(X)) → activate#(X) | U22#(tt, V1) → isNat#(activate(V1)) |
| activate#(n__s(X)) → activate#(X) | U92#(tt, L, N) → activate#(N) |
| isNatKind#(n__length(V1)) → activate#(V1) | U93#(tt, L, N) → activate#(N) |
| isNatKind#(n__s(V1)) → activate#(V1) | U51#(tt, V2) → isNatIListKind#(activate(V2)) |
| isNatList#(n__cons(V1, V2)) → isNatKind#(activate(V1)) | U85#(tt, V2) → isNatList#(activate(V2)) |
| U81#(tt, V1, V2) → U82#(isNatKind(activate(V1)), activate(V1), activate(V2)) | isNatList#(n__cons(V1, V2)) → U81#(isNatKind(activate(V1)), activate(V1), activate(V2)) |
| U84#(tt, V1, V2) → isNat#(activate(V1)) | U84#(tt, V1, V2) → activate#(V1) |
| U81#(tt, V1, V2) → activate#(V2) | U21#(tt, V1) → activate#(V1) |
| U85#(tt, V2) → activate#(V2) | U11#(tt, V1) → activate#(V1) |
| isNat#(n__length(V1)) → U11#(isNatIListKind(activate(V1)), activate(V1)) | U11#(tt, V1) → isNatIListKind#(activate(V1)) |
| U84#(tt, V1, V2) → U85#(isNat(activate(V1)), activate(V2)) | U92#(tt, L, N) → isNat#(activate(N)) |
| U93#(tt, L, N) → isNatKind#(activate(N)) | length#(cons(N, L)) → U91#(isNatList(activate(L)), activate(L), N) |
| U91#(tt, L, N) → U92#(isNatIListKind(activate(L)), activate(L), activate(N)) | U21#(tt, V1) → U22#(isNatKind(activate(V1)), activate(V1)) |
| isNatList#(n__cons(V1, V2)) → activate#(V1) | U82#(tt, V1, V2) → activate#(V2) |
| U93#(tt, L, N) → activate#(L) | U81#(tt, V1, V2) → activate#(V1) |
| isNat#(n__length(V1)) → isNatIListKind#(activate(V1)) | U93#(tt, L, N) → U94#(isNatKind(activate(N)), activate(L)) |
| length#(cons(N, L)) → activate#(L) |