TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (9079ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (5327ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (5053ms), 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)activate#(n__and(X1, X2)) → and#(activate(X1), X2)
isNatList#(n__take(V1, V2)) → activate#(V1)activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2))
isNatIListKind#(n__take(V1, V2)) → activate#(V1)U91#(tt, IL, M, N) → activate#(M)
activate#(n__cons(X1, X2)) → activate#(X1)isNatList#(n__take(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
activate#(n__isNat(X)) → isNat#(X)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)
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)))
isNatIList#(V) → isNatIListKind#(activate(V))isNatList#(n__cons(V1, V2)) → activate#(V2)
isNatKind#(n__length(V1)) → isNatIListKind#(activate(V1))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)))
take#(s(M), cons(N, IL)) → and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))))U91#(tt, IL, M, N) → activate#(N)
isNatIList#(n__cons(V1, V2)) → isNatKind#(activate(V1))activate#(n__length(X)) → length#(activate(X))
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)))
length#(cons(N, L)) → and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N)))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)
take#(s(M), cons(N, IL)) → U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N)U51#(tt, V1, V2) → isNat#(activate(V1))
activate#(n__and(X1, X2)) → activate#(X1)U51#(tt, V1, V2) → activate#(V2)
activate#(n__length(X)) → activate#(X)activate#(n__s(X)) → activate#(X)
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)
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))
U31#(tt, V) → activate#(V)isNatIListKind#(n__take(V1, V2)) → activate#(V2)
U42#(tt, V2) → activate#(V2)isNatIList#(V) → activate#(V)
activate#(n__take(X1, X2)) → activate#(X2)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))
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))U61#(tt, V1, V2) → activate#(V2)
activate#(n__take(X1, X2)) → activate#(X1)isNatIListKind#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatList#(n__cons(V1, V2)) → activate#(V1)isNat#(n__length(V1)) → isNatIListKind#(activate(V1))
U21#(tt, V1) → isNat#(activate(V1))take#(0, IL) → isNatIList#(IL)
isNatList#(n__take(V1, V2)) → U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))length#(cons(N, L)) → U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L))
isNatIList#(n__cons(V1, V2)) → activate#(V1)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(n__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(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__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)isNat(X) → n__isNat(X)
isNatKind(X) → n__isNatKind(X)activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))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__isNatIListKind(X)) → isNatIListKind(X)
activate(n__nil) → nilactivate(n__and(X1, X2)) → and(activate(X1), X2)
activate(n__isNat(X)) → isNat(X)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__isNat, 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))
activate#(n__and(X1, X2)) → and#(activate(X1), X2)isNatList#(n__take(V1, V2)) → activate#(V1)
isNatIListKind#(n__take(V1, V2)) → activate#(V1)activate#(n__cons(X1, X2)) → cons#(activate(X1), X2)
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)))activate#(n__length(X)) → length#(activate(X))
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)))length#(cons(N, L)) → and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N)))
U61#(tt, V1, V2) → isNat#(activate(V1))U62#(tt, V2) → U63#(isNatIList(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)) → isNatKind#(activate(V1))
activate#(n__zeros) → zeros#isNatIList#(n__cons(V1, V2)) → activate#(V2)
activate#(n__s(X)) → activate#(X)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))U31#(tt, V) → activate#(V)
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)
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)activate#(n__take(X1, X2)) → activate#(X1)
isNatList#(n__cons(V1, V2)) → activate#(V1)isNat#(n__length(V1)) → isNatIListKind#(activate(V1))
activate#(n__s(X)) → s#(activate(X))take#(0, IL) → isNatIList#(IL)
U51#(tt, V1, V2) → activate#(V1)zeros# → 0#
activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2))U21#(tt, V1) → U22#(isNat(activate(V1)))
U91#(tt, IL, M, N) → activate#(M)activate#(n__cons(X1, X2)) → activate#(X1)
isNatList#(n__take(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))activate#(n__isNat(X)) → isNat#(X)
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))take#(s(M), cons(N, IL)) → and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))))
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)))activate#(n__and(X1, X2)) → activate#(X1)
U51#(tt, V1, V2) → isNat#(activate(V1))take#(s(M), cons(N, IL)) → U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N)
activate#(n__length(X)) → activate#(X)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)
activate#(n__take(X1, X2)) → activate#(X2)isNatIList#(V) → activate#(V)
U71#(tt, L) → length#(activate(L))U31#(tt, V) → isNatList#(activate(V))
isNat#(n__length(V1)) → U11#(isNatIListKind(activate(V1)), activate(V1))activate#(n__nil) → nil#
isNatIListKind#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))length#(cons(N, L)) → U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L))
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)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(n__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(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__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)isNat(X) → n__isNat(X)
isNatKind(X) → n__isNatKind(X)activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))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__isNatIListKind(X)) → isNatIListKind(X)
activate(n__nil) → nilactivate(n__and(X1, X2)) → and(activate(X1), X2)
activate(n__isNat(X)) → isNat(X)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__isNat, n__take, U71, and, 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)activate#(n__and(X1, X2)) → and#(activate(X1), X2)
isNatList#(n__take(V1, V2)) → activate#(V1)activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2))
isNatIListKind#(n__take(V1, V2)) → activate#(V1)U91#(tt, IL, M, N) → activate#(M)
activate#(n__cons(X1, X2)) → activate#(X1)isNatList#(n__take(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
activate#(n__isNat(X)) → isNat#(X)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)
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))isNatList#(n__cons(V1, V2)) → activate#(V2)
isNatIList#(V) → isNatIListKind#(activate(V))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))
take#(s(M), cons(N, IL)) → and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))))isNatIList#(n__cons(V1, V2)) → isNatKind#(activate(V1))
U91#(tt, IL, M, N) → activate#(N)activate#(n__length(X)) → length#(activate(X))
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)length#(cons(N, L)) → and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N)))
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)
activate#(n__and(X1, X2)) → activate#(X1)U51#(tt, V1, V2) → isNat#(activate(V1))
take#(s(M), cons(N, IL)) → U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N)activate#(n__length(X)) → activate#(X)
U51#(tt, V1, V2) → activate#(V2)activate#(n__s(X)) → activate#(X)
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)
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)U42#(tt, V2) → activate#(V2)
isNatIListKind#(n__take(V1, V2)) → activate#(V2)activate#(n__take(X1, X2)) → activate#(X2)
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)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))U61#(tt, V1, V2) → activate#(V2)
activate#(n__take(X1, X2)) → activate#(X1)isNatIListKind#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
isNatList#(n__cons(V1, V2)) → activate#(V1)isNat#(n__length(V1)) → isNatIListKind#(activate(V1))
length#(cons(N, L)) → U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L))isNatList#(n__take(V1, V2)) → U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))
take#(0, IL) → isNatIList#(IL)U21#(tt, V1) → isNat#(activate(V1))
isNatIList#(n__cons(V1, V2)) → activate#(V1)length#(cons(N, L)) → activate#(L)