TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60017 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (7790ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (4270ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (4344ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

take#(s(M), cons(N, IL)) → isNatIList#(activate(IL))and#(tt, X) → activate#(X)
U11#(tt, V1) → isNatList#(activate(V1))isNatIList#(V) → U31#(isNatIListKind(activate(V)), activate(V))
U51#(tt, V1, V2) → activate#(V1)isNatList#(n__take(V1, V2)) → activate#(V1)
length#(cons(N, L)) → and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N)))isNatIListKind#(n__take(V1, V2)) → activate#(V1)
U91#(tt, IL, M, N) → activate#(M)isNatList#(n__take(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatIList#(n__cons(V1, V2)) → U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))isNat#(n__s(V1)) → activate#(V1)
isNat#(n__length(V1)) → activate#(V1)isNatIListKind#(n__cons(V1, V2)) → activate#(V2)
activate#(n__isNatIListKind(X)) → isNatIListKind#(X)U52#(tt, V2) → activate#(V2)
length#(cons(N, L)) → and#(isNatList(activate(L)), n__isNatIListKind(activate(L)))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))isNatList#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
U62#(tt, V2) → isNatIList#(activate(V2))isNatIList#(n__cons(V1, V2)) → isNatKind#(activate(V1))
U91#(tt, IL, M, N) → activate#(N)U61#(tt, V1, V2) → U62#(isNat(activate(V1)), activate(V2))
U41#(tt, V1, V2) → activate#(V1)length#(cons(N, L)) → isNatList#(activate(L))
activate#(n__isNatKind(X)) → isNatKind#(X)isNatList#(n__take(V1, V2)) → activate#(V2)
isNatIList#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))U61#(tt, V1, V2) → isNat#(activate(V1))
U41#(tt, V1, V2) → U42#(isNat(activate(V1)), activate(V2))take#(s(M), cons(N, IL)) → activate#(IL)
isNatKind#(n__s(V1)) → isNatKind#(activate(V1))isNatIListKind#(n__cons(V1, V2)) → activate#(V1)
isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))isNat#(n__s(V1)) → isNatKind#(activate(V1))
isNatIListKind#(n__take(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))isNatIList#(n__cons(V1, V2)) → activate#(V2)
length#(cons(N, L)) → isNat#(N)U51#(tt, V1, V2) → isNat#(activate(V1))
U51#(tt, V1, V2) → activate#(V2)U62#(tt, V2) → activate#(V2)
U52#(tt, V2) → isNatList#(activate(V2))U51#(tt, V1, V2) → U52#(isNat(activate(V1)), activate(V2))
isNatKind#(n__length(V1)) → activate#(V1)take#(0, IL) → and#(isNatIList(IL), n__isNatIListKind(IL))
isNatKind#(n__s(V1)) → activate#(V1)take#(s(M), cons(N, IL)) → and#(isNatIList(activate(IL)), n__isNatIListKind(activate(IL)))
U71#(tt, L) → activate#(L)isNatList#(n__cons(V1, V2)) → isNatKind#(activate(V1))
isNatList#(n__take(V1, V2)) → isNatKind#(activate(V1))U31#(tt, V) → activate#(V)
length#(cons(N, L)) → U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))take#(s(M), cons(N, IL)) → isNat#(N)
U42#(tt, V2) → activate#(V2)isNatIListKind#(n__take(V1, V2)) → activate#(V2)
isNatIList#(V) → activate#(V)take#(s(M), cons(N, IL)) → and#(isNat(M), n__isNatKind(M))
U71#(tt, L) → length#(activate(L))U91#(tt, IL, M, N) → activate#(IL)
U42#(tt, V2) → isNatIList#(activate(V2))isNatList#(n__cons(V1, V2)) → U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
U41#(tt, V1, V2) → isNat#(activate(V1))U21#(tt, V1) → activate#(V1)
U31#(tt, V) → isNatList#(activate(V))take#(s(M), cons(N, IL)) → and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))))
U61#(tt, V1, V2) → activate#(V1)U11#(tt, V1) → activate#(V1)
isNat#(n__length(V1)) → U11#(isNatIListKind(activate(V1)), activate(V1))U41#(tt, V1, V2) → activate#(V2)
isNatIListKind#(n__take(V1, V2)) → isNatKind#(activate(V1))activate#(n__length(X)) → length#(X)
U61#(tt, V1, V2) → activate#(V2)isNatIListKind#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatList#(n__cons(V1, V2)) → activate#(V1)activate#(n__take(X1, X2)) → take#(X1, X2)
isNat#(n__length(V1)) → isNatIListKind#(activate(V1))isNatList#(n__take(V1, V2)) → U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
U21#(tt, V1) → isNat#(activate(V1))take#(0, IL) → isNatIList#(IL)
activate#(n__and(X1, X2)) → and#(X1, X2)isNatIList#(n__cons(V1, V2)) → activate#(V1)
take#(s(M), cons(N, IL)) → isNat#(M)take#(s(M), cons(N, IL)) → U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)
length#(cons(N, L)) → activate#(L)

Rewrite Rules

zeros → cons(0, n__zeros)U11(tt, V1) → U12(isNatList(activate(V1)))
U12(tt) → ttU21(tt, V1) → U22(isNat(activate(V1)))
U22(tt) → ttU31(tt, V) → U32(isNatList(activate(V)))
U32(tt) → ttU41(tt, V1, V2) → U42(isNat(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNatIList(activate(V2)))U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(activate(V1)), activate(V2))U52(tt, V2) → U53(isNatList(activate(V2)))
U53(tt) → ttU61(tt, V1, V2) → U62(isNat(activate(V1)), activate(V2))
U62(tt, V2) → U63(isNatIList(activate(V2)))U63(tt) → tt
U71(tt, L) → s(length(activate(L)))U81(tt) → nil
U91(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))and(tt, X) → activate(X)
isNat(n__0) → ttisNat(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) → ttisNatIList(n__cons(V1, V2)) → U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
isNatIListKind(n__nil) → ttisNatIListKind(n__zeros) → tt
isNatIListKind(n__cons(V1, V2)) → and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))isNatIListKind(n__take(V1, V2)) → and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatKind(n__0) → ttisNatKind(n__length(V1)) → isNatIListKind(activate(V1))
isNatKind(n__s(V1)) → isNatKind(activate(V1))isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))isNatList(n__take(V1, V2)) → U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
length(nil) → 0length(cons(N, L)) → U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))
take(0, IL) → U81(and(isNatIList(IL), n__isNatIListKind(IL)))take(s(M), cons(N, IL)) → U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)
zeros → n__zerostake(X1, X2) → n__take(X1, X2)
0 → n__0length(X) → n__length(X)
s(X) → n__s(X)cons(X1, X2) → n__cons(X1, X2)
isNatIListKind(X) → n__isNatIListKind(X)nil → n__nil
and(X1, X2) → n__and(X1, X2)isNatKind(X) → n__isNatKind(X)
activate(n__zeros) → zerosactivate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIListKind(X)) → isNatIListKind(X)activate(n__nil) → nil
activate(n__and(X1, X2)) → and(X1, X2)activate(n__isNatKind(X)) → isNatKind(X)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: n__isNatIListKind, isNatIListKind, n__s, isNat, activate, U63, U62, n__0, U43, U61, U42, U41, U91, length, n__nil, n__zeros, U21, U22, cons, isNatIList, n__length, isNatKind, n__take, and, U71, n__and, n__cons, 0, isNatList, U51, s, tt, zeros, take, U53, U81, U52, U11, U12, U31, U32, n__isNatKind, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

take#(s(M), cons(N, IL)) → isNatIList#(activate(IL))and#(tt, X) → activate#(X)
U11#(tt, V1) → isNatList#(activate(V1))isNatIList#(V) → U31#(isNatIListKind(activate(V)), activate(V))
isNatList#(n__take(V1, V2)) → activate#(V1)length#(cons(N, L)) → and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N)))
isNatIListKind#(n__take(V1, V2)) → activate#(V1)U42#(tt, V2) → U43#(isNatIList(activate(V2)))
isNat#(n__length(V1)) → activate#(V1)isNatIListKind#(n__cons(V1, V2)) → activate#(V2)
length#(nil) → 0#U81#(tt) → nil#
U52#(tt, V2) → activate#(V2)isNatList#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatIList#(n__cons(V1, V2)) → isNatKind#(activate(V1))U11#(tt, V1) → U12#(isNatList(activate(V1)))
length#(cons(N, L)) → isNatList#(activate(L))isNatList#(n__take(V1, V2)) → activate#(V2)
isNatIList#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))U61#(tt, V1, V2) → isNat#(activate(V1))
U62#(tt, V2) → U63#(isNatIList(activate(V2)))take#(s(M), cons(N, IL)) → activate#(IL)
isNatIListKind#(n__cons(V1, V2)) → activate#(V1)isNatKind#(n__s(V1)) → isNatKind#(activate(V1))
isNat#(n__s(V1)) → isNatKind#(activate(V1))activate#(n__zeros) → zeros#
isNatIList#(n__cons(V1, V2)) → activate#(V2)length#(cons(N, L)) → isNat#(N)
isNatKind#(n__length(V1)) → activate#(V1)U51#(tt, V1, V2) → U52#(isNat(activate(V1)), activate(V2))
take#(0, IL) → and#(isNatIList(IL), n__isNatIListKind(IL))isNatKind#(n__s(V1)) → activate#(V1)
take#(s(M), cons(N, IL)) → and#(isNatIList(activate(IL)), n__isNatIListKind(activate(IL)))U71#(tt, L) → activate#(L)
isNatList#(n__cons(V1, V2)) → isNatKind#(activate(V1))isNatList#(n__take(V1, V2)) → isNatKind#(activate(V1))
length#(cons(N, L)) → U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))U31#(tt, V) → activate#(V)
take#(s(M), cons(N, IL)) → isNat#(N)U91#(tt, IL, M, N) → activate#(IL)
isNatList#(n__cons(V1, V2)) → U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))U42#(tt, V2) → isNatIList#(activate(V2))
U41#(tt, V1, V2) → isNat#(activate(V1))zeros# → cons#(0, n__zeros)
U21#(tt, V1) → activate#(V1)take#(s(M), cons(N, IL)) → and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))))
U61#(tt, V1, V2) → activate#(V1)U11#(tt, V1) → activate#(V1)
U41#(tt, V1, V2) → activate#(V2)U52#(tt, V2) → U53#(isNatList(activate(V2)))
U31#(tt, V) → U32#(isNatList(activate(V)))isNatIListKind#(n__take(V1, V2)) → isNatKind#(activate(V1))
U61#(tt, V1, V2) → activate#(V2)isNatList#(n__cons(V1, V2)) → activate#(V1)
activate#(n__take(X1, X2)) → take#(X1, X2)isNat#(n__length(V1)) → isNatIListKind#(activate(V1))
take#(0, IL) → isNatIList#(IL)activate#(n__and(X1, X2)) → and#(X1, X2)
take#(s(M), cons(N, IL)) → U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)U51#(tt, V1, V2) → activate#(V1)
zeros# → 0#U21#(tt, V1) → U22#(isNat(activate(V1)))
U91#(tt, IL, M, N) → activate#(M)isNatList#(n__take(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatIList#(n__cons(V1, V2)) → U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))isNat#(n__s(V1)) → activate#(V1)
activate#(n__isNatIListKind(X)) → isNatIListKind#(X)length#(cons(N, L)) → and#(isNatList(activate(L)), n__isNatIListKind(activate(L)))
isNatIList#(V) → isNatIListKind#(activate(V))isNatKind#(n__length(V1)) → isNatIListKind#(activate(V1))
isNatList#(n__cons(V1, V2)) → activate#(V2)isNatIListKind#(n__cons(V1, V2)) → isNatKind#(activate(V1))
U62#(tt, V2) → isNatIList#(activate(V2))U91#(tt, IL, M, N) → activate#(N)
U71#(tt, L) → s#(length(activate(L)))U61#(tt, V1, V2) → U62#(isNat(activate(V1)), activate(V2))
U41#(tt, V1, V2) → activate#(V1)activate#(n__isNatKind(X)) → isNatKind#(X)
activate#(n__0) → 0#U41#(tt, V1, V2) → U42#(isNat(activate(V1)), activate(V2))
isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))isNatIListKind#(n__take(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
U51#(tt, V1, V2) → isNat#(activate(V1))U51#(tt, V1, V2) → activate#(V2)
U62#(tt, V2) → activate#(V2)U52#(tt, V2) → isNatList#(activate(V2))
take#(0, IL) → U81#(and(isNatIList(IL), n__isNatIListKind(IL)))U91#(tt, IL, M, N) → cons#(activate(N), n__take(activate(M), activate(IL)))
U42#(tt, V2) → activate#(V2)isNatIListKind#(n__take(V1, V2)) → activate#(V2)
isNatIList#(V) → activate#(V)take#(s(M), cons(N, IL)) → and#(isNat(M), n__isNatKind(M))
activate#(n__cons(X1, X2)) → cons#(X1, X2)U71#(tt, L) → length#(activate(L))
U31#(tt, V) → isNatList#(activate(V))isNat#(n__length(V1)) → U11#(isNatIListKind(activate(V1)), activate(V1))
activate#(n__s(X)) → s#(X)activate#(n__length(X)) → length#(X)
activate#(n__nil) → nil#isNatIListKind#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatList#(n__take(V1, V2)) → U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))U21#(tt, V1) → isNat#(activate(V1))
isNatIList#(n__cons(V1, V2)) → activate#(V1)take#(s(M), cons(N, IL)) → isNat#(M)
length#(cons(N, L)) → activate#(L)

Rewrite Rules

zeros → cons(0, n__zeros)U11(tt, V1) → U12(isNatList(activate(V1)))
U12(tt) → ttU21(tt, V1) → U22(isNat(activate(V1)))
U22(tt) → ttU31(tt, V) → U32(isNatList(activate(V)))
U32(tt) → ttU41(tt, V1, V2) → U42(isNat(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNatIList(activate(V2)))U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(activate(V1)), activate(V2))U52(tt, V2) → U53(isNatList(activate(V2)))
U53(tt) → ttU61(tt, V1, V2) → U62(isNat(activate(V1)), activate(V2))
U62(tt, V2) → U63(isNatIList(activate(V2)))U63(tt) → tt
U71(tt, L) → s(length(activate(L)))U81(tt) → nil
U91(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))and(tt, X) → activate(X)
isNat(n__0) → ttisNat(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) → ttisNatIList(n__cons(V1, V2)) → U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
isNatIListKind(n__nil) → ttisNatIListKind(n__zeros) → tt
isNatIListKind(n__cons(V1, V2)) → and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))isNatIListKind(n__take(V1, V2)) → and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatKind(n__0) → ttisNatKind(n__length(V1)) → isNatIListKind(activate(V1))
isNatKind(n__s(V1)) → isNatKind(activate(V1))isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))isNatList(n__take(V1, V2)) → U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
length(nil) → 0length(cons(N, L)) → U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))
take(0, IL) → U81(and(isNatIList(IL), n__isNatIListKind(IL)))take(s(M), cons(N, IL)) → U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)
zeros → n__zerostake(X1, X2) → n__take(X1, X2)
0 → n__0length(X) → n__length(X)
s(X) → n__s(X)cons(X1, X2) → n__cons(X1, X2)
isNatIListKind(X) → n__isNatIListKind(X)nil → n__nil
and(X1, X2) → n__and(X1, X2)isNatKind(X) → n__isNatKind(X)
activate(n__zeros) → zerosactivate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIListKind(X)) → isNatIListKind(X)activate(n__nil) → nil
activate(n__and(X1, X2)) → and(X1, X2)activate(n__isNatKind(X)) → isNatKind(X)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: n__isNatIListKind, isNatIListKind, activate, isNat, n__s, U63, U62, U61, U43, n__0, U42, U41, U91, length, n__nil, n__zeros, U21, U22, cons, isNatIList, n__length, isNatKind, n__take, and, U71, n__cons, n__and, 0, s, U51, isNatList, zeros, tt, U53, take, U52, U81, U11, U12, U31, U32, nil, n__isNatKind

Strategy

The following SCCs where found

take#(s(M), cons(N, IL)) → isNatIList#(activate(IL))and#(tt, X) → activate#(X)
U11#(tt, V1) → isNatList#(activate(V1))isNatIList#(V) → U31#(isNatIListKind(activate(V)), activate(V))
U51#(tt, V1, V2) → activate#(V1)isNatList#(n__take(V1, V2)) → activate#(V1)
length#(cons(N, L)) → and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N)))isNatIListKind#(n__take(V1, V2)) → activate#(V1)
U91#(tt, IL, M, N) → activate#(M)isNatList#(n__take(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatIList#(n__cons(V1, V2)) → U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))isNat#(n__length(V1)) → activate#(V1)
isNat#(n__s(V1)) → activate#(V1)activate#(n__isNatIListKind(X)) → isNatIListKind#(X)
isNatIListKind#(n__cons(V1, V2)) → activate#(V2)length#(cons(N, L)) → and#(isNatList(activate(L)), n__isNatIListKind(activate(L)))
U52#(tt, V2) → activate#(V2)isNatKind#(n__length(V1)) → isNatIListKind#(activate(V1))
isNatIList#(V) → isNatIListKind#(activate(V))isNatList#(n__cons(V1, V2)) → activate#(V2)
isNatIListKind#(n__cons(V1, V2)) → isNatKind#(activate(V1))U62#(tt, V2) → isNatIList#(activate(V2))
isNatList#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))U91#(tt, IL, M, N) → activate#(N)
isNatIList#(n__cons(V1, V2)) → isNatKind#(activate(V1))U41#(tt, V1, V2) → activate#(V1)
U61#(tt, V1, V2) → U62#(isNat(activate(V1)), activate(V2))length#(cons(N, L)) → isNatList#(activate(L))
activate#(n__isNatKind(X)) → isNatKind#(X)isNatList#(n__take(V1, V2)) → activate#(V2)
isNatIList#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))U61#(tt, V1, V2) → isNat#(activate(V1))
U41#(tt, V1, V2) → U42#(isNat(activate(V1)), activate(V2))take#(s(M), cons(N, IL)) → activate#(IL)
isNatIListKind#(n__cons(V1, V2)) → activate#(V1)isNatKind#(n__s(V1)) → isNatKind#(activate(V1))
isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))isNat#(n__s(V1)) → isNatKind#(activate(V1))
isNatIListKind#(n__take(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))isNatIList#(n__cons(V1, V2)) → activate#(V2)
length#(cons(N, L)) → isNat#(N)U51#(tt, V1, V2) → isNat#(activate(V1))
U51#(tt, V1, V2) → activate#(V2)isNatKind#(n__length(V1)) → activate#(V1)
U51#(tt, V1, V2) → U52#(isNat(activate(V1)), activate(V2))U52#(tt, V2) → isNatList#(activate(V2))
U62#(tt, V2) → activate#(V2)isNatKind#(n__s(V1)) → activate#(V1)
take#(0, IL) → and#(isNatIList(IL), n__isNatIListKind(IL))take#(s(M), cons(N, IL)) → and#(isNatIList(activate(IL)), n__isNatIListKind(activate(IL)))
U71#(tt, L) → activate#(L)isNatList#(n__cons(V1, V2)) → isNatKind#(activate(V1))
isNatList#(n__take(V1, V2)) → isNatKind#(activate(V1))length#(cons(N, L)) → U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))
U31#(tt, V) → activate#(V)take#(s(M), cons(N, IL)) → isNat#(N)
isNatIListKind#(n__take(V1, V2)) → activate#(V2)U42#(tt, V2) → activate#(V2)
take#(s(M), cons(N, IL)) → and#(isNat(M), n__isNatKind(M))isNatIList#(V) → activate#(V)
U71#(tt, L) → length#(activate(L))U91#(tt, IL, M, N) → activate#(IL)
isNatList#(n__cons(V1, V2)) → U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))U42#(tt, V2) → isNatIList#(activate(V2))
U41#(tt, V1, V2) → isNat#(activate(V1))U21#(tt, V1) → activate#(V1)
take#(s(M), cons(N, IL)) → and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))))U31#(tt, V) → isNatList#(activate(V))
U61#(tt, V1, V2) → activate#(V1)isNat#(n__length(V1)) → U11#(isNatIListKind(activate(V1)), activate(V1))
U11#(tt, V1) → activate#(V1)U41#(tt, V1, V2) → activate#(V2)
isNatIListKind#(n__take(V1, V2)) → isNatKind#(activate(V1))activate#(n__length(X)) → length#(X)
U61#(tt, V1, V2) → activate#(V2)isNatIListKind#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatList#(n__cons(V1, V2)) → activate#(V1)activate#(n__take(X1, X2)) → take#(X1, X2)
isNat#(n__length(V1)) → isNatIListKind#(activate(V1))take#(0, IL) → isNatIList#(IL)
U21#(tt, V1) → isNat#(activate(V1))isNatList#(n__take(V1, V2)) → U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
isNatIList#(n__cons(V1, V2)) → activate#(V1)activate#(n__and(X1, X2)) → and#(X1, X2)
take#(s(M), cons(N, IL)) → isNat#(M)length#(cons(N, L)) → activate#(L)
take#(s(M), cons(N, IL)) → U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)