TIMEOUT

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

The following DP Processors were used


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

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

a__U51#(tt, V1, V2) → a__isNat#(V1)mark#(U11(X1, X2)) → mark#(X1)
mark#(take(X1, X2)) → mark#(X1)mark#(isNatIListKind(X)) → a__isNatIListKind#(X)
a__length#(cons(N, L)) → a__and#(a__isNatList(L), isNatIListKind(L))mark#(isNatIList(X)) → a__isNatIList#(X)
a__take#(s(M), cons(N, IL)) → a__and#(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))))a__isNatList#(take(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
a__isNatKind#(length(V1)) → a__isNatIListKind#(V1)a__isNatList#(take(V1, V2)) → a__isNatKind#(V1)
mark#(U81(X)) → mark#(X)a__U71#(tt, L) → a__length#(mark(L))
a__and#(tt, X) → mark#(X)a__U52#(tt, V2) → a__isNatList#(V2)
mark#(U31(X1, X2)) → mark#(X1)mark#(s(X)) → mark#(X)
mark#(U71(X1, X2)) → a__U71#(mark(X1), X2)a__take#(0, IL) → a__isNatIList#(IL)
a__U21#(tt, V1) → a__isNat#(V1)mark#(U53(X)) → mark#(X)
a__isNatList#(cons(V1, V2)) → a__isNatKind#(V1)mark#(U42(X1, X2)) → a__U42#(mark(X1), X2)
a__U61#(tt, V1, V2) → a__isNat#(V1)a__isNatIList#(V) → a__U31#(a__isNatIListKind(V), V)
mark#(cons(X1, X2)) → mark#(X1)a__isNatIListKind#(take(V1, V2)) → a__isNatKind#(V1)
a__isNat#(s(V1)) → a__isNatKind#(V1)mark#(U71(X1, X2)) → mark#(X1)
mark#(isNatList(X)) → a__isNatList#(X)a__isNatIList#(cons(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
mark#(and(X1, X2)) → mark#(X1)mark#(and(X1, X2)) → a__and#(mark(X1), X2)
mark#(U41(X1, X2, X3)) → mark#(X1)a__isNatIListKind#(cons(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
mark#(U63(X)) → mark#(X)a__isNatIList#(cons(V1, V2)) → a__U41#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__U51#(tt, V1, V2) → a__U52#(a__isNat(V1), V2)a__length#(cons(N, L)) → a__U71#(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
mark#(isNat(X)) → a__isNat#(X)a__isNat#(length(V1)) → a__isNatIListKind#(V1)
a__take#(s(M), cons(N, IL)) → a__and#(a__isNatIList(IL), isNatIListKind(IL))a__isNatIListKind#(take(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
a__U41#(tt, V1, V2) → a__isNat#(V1)mark#(U61(X1, X2, X3)) → mark#(X1)
a__isNatIList#(V) → a__isNatIListKind#(V)a__isNatIListKind#(cons(V1, V2)) → a__isNatKind#(V1)
mark#(U32(X)) → mark#(X)mark#(U21(X1, X2)) → mark#(X1)
mark#(U62(X1, X2)) → a__U62#(mark(X1), X2)mark#(U62(X1, X2)) → mark#(X1)
mark#(U41(X1, X2, X3)) → a__U41#(mark(X1), X2, X3)mark#(U31(X1, X2)) → a__U31#(mark(X1), X2)
a__isNatKind#(s(V1)) → a__isNatKind#(V1)mark#(length(X)) → a__length#(mark(X))
a__take#(s(M), cons(N, IL)) → a__isNatIList#(IL)mark#(U51(X1, X2, X3)) → mark#(X1)
a__isNatIList#(cons(V1, V2)) → a__isNatKind#(V1)mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)
mark#(length(X)) → mark#(X)mark#(U61(X1, X2, X3)) → a__U61#(mark(X1), X2, X3)
a__length#(cons(N, L)) → a__isNatList#(L)a__U91#(tt, IL, M, N) → mark#(N)
a__U11#(tt, V1) → a__isNatList#(V1)a__U71#(tt, L) → mark#(L)
mark#(U12(X)) → mark#(X)mark#(U42(X1, X2)) → mark#(X1)
a__U61#(tt, V1, V2) → a__U62#(a__isNat(V1), V2)mark#(U52(X1, X2)) → mark#(X1)
a__isNatList#(take(V1, V2)) → a__U61#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)a__isNat#(length(V1)) → a__U11#(a__isNatIListKind(V1), V1)
a__U42#(tt, V2) → a__isNatIList#(V2)a__take#(s(M), cons(N, IL)) → a__U91#(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)
a__isNatList#(cons(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))mark#(U91(X1, X2, X3, X4)) → mark#(X1)
mark#(U51(X1, X2, X3)) → a__U51#(mark(X1), X2, X3)mark#(U43(X)) → mark#(X)
a__length#(cons(N, L)) → a__and#(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))mark#(U22(X)) → mark#(X)
a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1)mark#(U21(X1, X2)) → a__U21#(mark(X1), X2)
mark#(take(X1, X2)) → a__take#(mark(X1), mark(X2))a__U31#(tt, V) → a__isNatList#(V)
mark#(isNatKind(X)) → a__isNatKind#(X)a__U41#(tt, V1, V2) → a__U42#(a__isNat(V1), V2)
a__isNatList#(cons(V1, V2)) → a__U51#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)mark#(take(X1, X2)) → mark#(X2)
mark#(U11(X1, X2)) → a__U11#(mark(X1), X2)mark#(U91(X1, X2, X3, X4)) → a__U91#(mark(X1), X2, X3, X4)
a__U62#(tt, V2) → a__isNatIList#(V2)a__take#(0, IL) → a__and#(a__isNatIList(IL), isNatIListKind(IL))

Rewrite Rules

a__zeros → cons(0, zeros)a__U11(tt, V1) → a__U12(a__isNatList(V1))
a__U12(tt) → tta__U21(tt, V1) → a__U22(a__isNat(V1))
a__U22(tt) → tta__U31(tt, V) → a__U32(a__isNatList(V))
a__U32(tt) → tta__U41(tt, V1, V2) → a__U42(a__isNat(V1), V2)
a__U42(tt, V2) → a__U43(a__isNatIList(V2))a__U43(tt) → tt
a__U51(tt, V1, V2) → a__U52(a__isNat(V1), V2)a__U52(tt, V2) → a__U53(a__isNatList(V2))
a__U53(tt) → tta__U61(tt, V1, V2) → a__U62(a__isNat(V1), V2)
a__U62(tt, V2) → a__U63(a__isNatIList(V2))a__U63(tt) → tt
a__U71(tt, L) → s(a__length(mark(L)))a__U81(tt) → nil
a__U91(tt, IL, M, N) → cons(mark(N), take(M, IL))a__and(tt, X) → mark(X)
a__isNat(0) → tta__isNat(length(V1)) → a__U11(a__isNatIListKind(V1), V1)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatIList(V) → a__U31(a__isNatIListKind(V), V)
a__isNatIList(zeros) → tta__isNatIList(cons(V1, V2)) → a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__isNatIListKind(nil) → tta__isNatIListKind(zeros) → tt
a__isNatIListKind(cons(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))a__isNatIListKind(take(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))
a__isNatKind(0) → tta__isNatKind(length(V1)) → a__isNatIListKind(V1)
a__isNatKind(s(V1)) → a__isNatKind(V1)a__isNatList(nil) → tt
a__isNatList(cons(V1, V2)) → a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)a__isNatList(take(V1, V2)) → a__U61(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__length(nil) → 0a__length(cons(N, L)) → a__U71(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
a__take(0, IL) → a__U81(a__and(a__isNatIList(IL), isNatIListKind(IL)))a__take(s(M), cons(N, IL)) → a__U91(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)
mark(zeros) → a__zerosmark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X)) → a__U12(mark(X))mark(isNatList(X)) → a__isNatList(X)
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X)) → a__U22(mark(X))
mark(isNat(X)) → a__isNat(X)mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)
mark(U42(X1, X2)) → a__U42(mark(X1), X2)mark(U43(X)) → a__U43(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)mark(U53(X)) → a__U53(mark(X))
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(U63(X)) → a__U63(mark(X))mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(length(X)) → a__length(mark(X))mark(U81(X)) → a__U81(mark(X))
mark(U91(X1, X2, X3, X4)) → a__U91(mark(X1), X2, X3, X4)mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)mark(isNatIListKind(X)) → a__isNatIListKind(X)
mark(isNatKind(X)) → a__isNatKind(X)mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0mark(tt) → tt
mark(s(X)) → s(mark(X))mark(nil) → nil
a__zeros → zerosa__U11(X1, X2) → U11(X1, X2)
a__U12(X) → U12(X)a__isNatList(X) → isNatList(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X) → U22(X)
a__isNat(X) → isNat(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X1, X2, X3) → U41(X1, X2, X3)
a__U42(X1, X2) → U42(X1, X2)a__U43(X) → U43(X)
a__isNatIList(X) → isNatIList(X)a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__U52(X1, X2) → U52(X1, X2)a__U53(X) → U53(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2) → U62(X1, X2)
a__U63(X) → U63(X)a__U71(X1, X2) → U71(X1, X2)
a__length(X) → length(X)a__U81(X) → U81(X)
a__U91(X1, X2, X3, X4) → U91(X1, X2, X3, X4)a__take(X1, X2) → take(X1, X2)
a__and(X1, X2) → and(X1, X2)a__isNatIListKind(X) → isNatIListKind(X)
a__isNatKind(X) → isNatKind(X)

Original Signature

Termination of terms over the following signature is verified: U63, U62, U61, a__U41, a__U43, a__U42, a__U71, U21, U22, isNatIList, isNatKind, mark, U71, and, 0, a__isNatIList, zeros, a__isNat, a__U32, a__U31, a__U81, U31, U32, a__U51, a__U52, a__U53, a__take, isNatIListKind, a__isNatIListKind, a__and, isNat, a__isNatList, U43, a__U91, U42, U41, U91, length, a__U22, a__U21, cons, a__U62, a__zeros, a__U63, a__length, U51, s, isNatList, tt, U53, take, U81, U52, U11, a__U12, U12, a__U11, a__U61, nil, a__isNatKind

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a__U51#(tt, V1, V2) → a__isNat#(V1)mark#(U11(X1, X2)) → mark#(X1)
a__length#(cons(N, L)) → a__and#(a__isNatList(L), isNatIListKind(L))mark#(isNatIList(X)) → a__isNatIList#(X)
a__isNatList#(take(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))a__isNatList#(take(V1, V2)) → a__isNatKind#(V1)
a__and#(tt, X) → mark#(X)a__U52#(tt, V2) → a__isNatList#(V2)
mark#(s(X)) → mark#(X)a__U21#(tt, V1) → a__isNat#(V1)
mark#(U53(X)) → mark#(X)a__isNatIList#(V) → a__U31#(a__isNatIListKind(V), V)
mark#(cons(X1, X2)) → mark#(X1)mark#(and(X1, X2)) → mark#(X1)
mark#(and(X1, X2)) → a__and#(mark(X1), X2)mark#(U41(X1, X2, X3)) → mark#(X1)
mark#(U63(X)) → mark#(X)a__isNatIList#(cons(V1, V2)) → a__U41#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
mark#(U43(X)) → a__U43#(mark(X))a__U62#(tt, V2) → a__U63#(a__isNatIList(V2))
a__length#(cons(N, L)) → a__U71#(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)mark#(isNat(X)) → a__isNat#(X)
a__isNat#(length(V1)) → a__isNatIListKind#(V1)a__U41#(tt, V1, V2) → a__isNat#(V1)
a__take#(s(M), cons(N, IL)) → a__and#(a__isNatIList(IL), isNatIListKind(IL))mark#(U32(X)) → a__U32#(mark(X))
mark#(zeros) → a__zeros#mark#(U63(X)) → a__U63#(mark(X))
a__isNatIListKind#(cons(V1, V2)) → a__isNatKind#(V1)mark#(U32(X)) → mark#(X)
mark#(U62(X1, X2)) → mark#(X1)mark#(U41(X1, X2, X3)) → a__U41#(mark(X1), X2, X3)
a__isNatKind#(s(V1)) → a__isNatKind#(V1)mark#(length(X)) → a__length#(mark(X))
a__take#(s(M), cons(N, IL)) → a__isNatIList#(IL)a__U21#(tt, V1) → a__U22#(a__isNat(V1))
mark#(U51(X1, X2, X3)) → mark#(X1)a__U11#(tt, V1) → a__U12#(a__isNatList(V1))
mark#(U22(X)) → a__U22#(mark(X))mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)
mark#(length(X)) → mark#(X)mark#(U61(X1, X2, X3)) → a__U61#(mark(X1), X2, X3)
a__length#(cons(N, L)) → a__isNatList#(L)a__U11#(tt, V1) → a__isNatList#(V1)
a__U71#(tt, L) → mark#(L)mark#(U42(X1, X2)) → mark#(X1)
a__isNatList#(take(V1, V2)) → a__U61#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)a__isNat#(length(V1)) → a__U11#(a__isNatIListKind(V1), V1)
a__U42#(tt, V2) → a__isNatIList#(V2)a__U52#(tt, V2) → a__U53#(a__isNatList(V2))
mark#(U51(X1, X2, X3)) → a__U51#(mark(X1), X2, X3)mark#(U22(X)) → mark#(X)
mark#(U43(X)) → mark#(X)a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1)
a__U31#(tt, V) → a__isNatList#(V)mark#(take(X1, X2)) → a__take#(mark(X1), mark(X2))
a__isNatList#(cons(V1, V2)) → a__U51#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)mark#(U91(X1, X2, X3, X4)) → a__U91#(mark(X1), X2, X3, X4)
a__take#(0, IL) → a__and#(a__isNatIList(IL), isNatIListKind(IL))mark#(isNatIListKind(X)) → a__isNatIListKind#(X)
mark#(take(X1, X2)) → mark#(X1)a__take#(s(M), cons(N, IL)) → a__and#(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))))
a__isNatKind#(length(V1)) → a__isNatIListKind#(V1)a__take#(0, IL) → a__U81#(a__and(a__isNatIList(IL), isNatIListKind(IL)))
mark#(U53(X)) → a__U53#(mark(X))mark#(U81(X)) → mark#(X)
a__U71#(tt, L) → a__length#(mark(L))mark#(U31(X1, X2)) → mark#(X1)
mark#(U71(X1, X2)) → a__U71#(mark(X1), X2)a__U31#(tt, V) → a__U32#(a__isNatList(V))
a__take#(0, IL) → a__isNatIList#(IL)a__isNatList#(cons(V1, V2)) → a__isNatKind#(V1)
a__U61#(tt, V1, V2) → a__isNat#(V1)mark#(U42(X1, X2)) → a__U42#(mark(X1), X2)
a__isNatIListKind#(take(V1, V2)) → a__isNatKind#(V1)a__isNat#(s(V1)) → a__isNatKind#(V1)
mark#(U71(X1, X2)) → mark#(X1)a__isNatIList#(cons(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
mark#(isNatList(X)) → a__isNatList#(X)a__isNatIListKind#(cons(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
a__U51#(tt, V1, V2) → a__U52#(a__isNat(V1), V2)a__isNatIListKind#(take(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
a__U42#(tt, V2) → a__U43#(a__isNatIList(V2))a__isNatIList#(V) → a__isNatIListKind#(V)
mark#(U61(X1, X2, X3)) → mark#(X1)mark#(U21(X1, X2)) → mark#(X1)
mark#(U62(X1, X2)) → a__U62#(mark(X1), X2)mark#(U31(X1, X2)) → a__U31#(mark(X1), X2)
a__isNatIList#(cons(V1, V2)) → a__isNatKind#(V1)a__U91#(tt, IL, M, N) → mark#(N)
mark#(U12(X)) → mark#(X)a__U61#(tt, V1, V2) → a__U62#(a__isNat(V1), V2)
mark#(U52(X1, X2)) → mark#(X1)mark#(U12(X)) → a__U12#(mark(X))
a__take#(s(M), cons(N, IL)) → a__U91#(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)a__isNatList#(cons(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
mark#(U91(X1, X2, X3, X4)) → mark#(X1)a__length#(cons(N, L)) → a__and#(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))
mark#(U21(X1, X2)) → a__U21#(mark(X1), X2)a__U41#(tt, V1, V2) → a__U42#(a__isNat(V1), V2)
mark#(isNatKind(X)) → a__isNatKind#(X)mark#(U11(X1, X2)) → a__U11#(mark(X1), X2)
mark#(take(X1, X2)) → mark#(X2)mark#(U81(X)) → a__U81#(mark(X))
a__U62#(tt, V2) → a__isNatIList#(V2)

Rewrite Rules

a__zeros → cons(0, zeros)a__U11(tt, V1) → a__U12(a__isNatList(V1))
a__U12(tt) → tta__U21(tt, V1) → a__U22(a__isNat(V1))
a__U22(tt) → tta__U31(tt, V) → a__U32(a__isNatList(V))
a__U32(tt) → tta__U41(tt, V1, V2) → a__U42(a__isNat(V1), V2)
a__U42(tt, V2) → a__U43(a__isNatIList(V2))a__U43(tt) → tt
a__U51(tt, V1, V2) → a__U52(a__isNat(V1), V2)a__U52(tt, V2) → a__U53(a__isNatList(V2))
a__U53(tt) → tta__U61(tt, V1, V2) → a__U62(a__isNat(V1), V2)
a__U62(tt, V2) → a__U63(a__isNatIList(V2))a__U63(tt) → tt
a__U71(tt, L) → s(a__length(mark(L)))a__U81(tt) → nil
a__U91(tt, IL, M, N) → cons(mark(N), take(M, IL))a__and(tt, X) → mark(X)
a__isNat(0) → tta__isNat(length(V1)) → a__U11(a__isNatIListKind(V1), V1)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatIList(V) → a__U31(a__isNatIListKind(V), V)
a__isNatIList(zeros) → tta__isNatIList(cons(V1, V2)) → a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__isNatIListKind(nil) → tta__isNatIListKind(zeros) → tt
a__isNatIListKind(cons(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))a__isNatIListKind(take(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))
a__isNatKind(0) → tta__isNatKind(length(V1)) → a__isNatIListKind(V1)
a__isNatKind(s(V1)) → a__isNatKind(V1)a__isNatList(nil) → tt
a__isNatList(cons(V1, V2)) → a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)a__isNatList(take(V1, V2)) → a__U61(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__length(nil) → 0a__length(cons(N, L)) → a__U71(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
a__take(0, IL) → a__U81(a__and(a__isNatIList(IL), isNatIListKind(IL)))a__take(s(M), cons(N, IL)) → a__U91(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)
mark(zeros) → a__zerosmark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X)) → a__U12(mark(X))mark(isNatList(X)) → a__isNatList(X)
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X)) → a__U22(mark(X))
mark(isNat(X)) → a__isNat(X)mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)
mark(U42(X1, X2)) → a__U42(mark(X1), X2)mark(U43(X)) → a__U43(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)mark(U53(X)) → a__U53(mark(X))
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(U63(X)) → a__U63(mark(X))mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(length(X)) → a__length(mark(X))mark(U81(X)) → a__U81(mark(X))
mark(U91(X1, X2, X3, X4)) → a__U91(mark(X1), X2, X3, X4)mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)mark(isNatIListKind(X)) → a__isNatIListKind(X)
mark(isNatKind(X)) → a__isNatKind(X)mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0mark(tt) → tt
mark(s(X)) → s(mark(X))mark(nil) → nil
a__zeros → zerosa__U11(X1, X2) → U11(X1, X2)
a__U12(X) → U12(X)a__isNatList(X) → isNatList(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X) → U22(X)
a__isNat(X) → isNat(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X1, X2, X3) → U41(X1, X2, X3)
a__U42(X1, X2) → U42(X1, X2)a__U43(X) → U43(X)
a__isNatIList(X) → isNatIList(X)a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__U52(X1, X2) → U52(X1, X2)a__U53(X) → U53(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2) → U62(X1, X2)
a__U63(X) → U63(X)a__U71(X1, X2) → U71(X1, X2)
a__length(X) → length(X)a__U81(X) → U81(X)
a__U91(X1, X2, X3, X4) → U91(X1, X2, X3, X4)a__take(X1, X2) → take(X1, X2)
a__and(X1, X2) → and(X1, X2)a__isNatIListKind(X) → isNatIListKind(X)
a__isNatKind(X) → isNatKind(X)

Original Signature

Termination of terms over the following signature is verified: U63, U62, U61, a__U41, a__U43, a__U42, a__U71, U21, U22, isNatIList, isNatKind, mark, and, U71, 0, a__isNatIList, zeros, a__isNat, a__U32, a__U31, a__U81, U31, U32, a__U51, a__U52, a__U53, a__take, isNatIListKind, a__isNatIListKind, a__and, isNat, a__isNatList, U43, a__U91, U42, U41, U91, length, a__U22, a__U21, cons, a__U62, a__zeros, a__U63, a__length, U51, s, isNatList, tt, take, U53, U52, U81, U11, U12, a__U12, a__U11, a__U61, a__isNatKind, nil

Strategy

The following SCCs where found

a__U51#(tt, V1, V2) → a__isNat#(V1)mark#(U11(X1, X2)) → mark#(X1)
a__length#(cons(N, L)) → a__and#(a__isNatList(L), isNatIListKind(L))mark#(isNatIListKind(X)) → a__isNatIListKind#(X)
mark#(take(X1, X2)) → mark#(X1)mark#(isNatIList(X)) → a__isNatIList#(X)
a__take#(s(M), cons(N, IL)) → a__and#(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))))a__isNatList#(take(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
a__isNatKind#(length(V1)) → a__isNatIListKind#(V1)a__isNatList#(take(V1, V2)) → a__isNatKind#(V1)
mark#(U81(X)) → mark#(X)a__and#(tt, X) → mark#(X)
a__U71#(tt, L) → a__length#(mark(L))a__U52#(tt, V2) → a__isNatList#(V2)
mark#(U31(X1, X2)) → mark#(X1)mark#(s(X)) → mark#(X)
mark#(U71(X1, X2)) → a__U71#(mark(X1), X2)a__take#(0, IL) → a__isNatIList#(IL)
a__U21#(tt, V1) → a__isNat#(V1)mark#(U53(X)) → mark#(X)
a__isNatList#(cons(V1, V2)) → a__isNatKind#(V1)a__isNatIList#(V) → a__U31#(a__isNatIListKind(V), V)
a__U61#(tt, V1, V2) → a__isNat#(V1)mark#(U42(X1, X2)) → a__U42#(mark(X1), X2)
mark#(cons(X1, X2)) → mark#(X1)a__isNatIListKind#(take(V1, V2)) → a__isNatKind#(V1)
a__isNat#(s(V1)) → a__isNatKind#(V1)mark#(U71(X1, X2)) → mark#(X1)
a__isNatIList#(cons(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))mark#(isNatList(X)) → a__isNatList#(X)
mark#(and(X1, X2)) → mark#(X1)a__isNatIListKind#(cons(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
mark#(U41(X1, X2, X3)) → mark#(X1)mark#(and(X1, X2)) → a__and#(mark(X1), X2)
mark#(U63(X)) → mark#(X)a__isNatIList#(cons(V1, V2)) → a__U41#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__U51#(tt, V1, V2) → a__U52#(a__isNat(V1), V2)a__length#(cons(N, L)) → a__U71#(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
mark#(isNat(X)) → a__isNat#(X)a__isNat#(length(V1)) → a__isNatIListKind#(V1)
a__U41#(tt, V1, V2) → a__isNat#(V1)a__isNatIListKind#(take(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))
a__take#(s(M), cons(N, IL)) → a__and#(a__isNatIList(IL), isNatIListKind(IL))a__isNatIListKind#(cons(V1, V2)) → a__isNatKind#(V1)
a__isNatIList#(V) → a__isNatIListKind#(V)mark#(U61(X1, X2, X3)) → mark#(X1)
mark#(U32(X)) → mark#(X)mark#(U62(X1, X2)) → mark#(X1)
mark#(U62(X1, X2)) → a__U62#(mark(X1), X2)mark#(U21(X1, X2)) → mark#(X1)
mark#(U31(X1, X2)) → a__U31#(mark(X1), X2)mark#(U41(X1, X2, X3)) → a__U41#(mark(X1), X2, X3)
a__isNatKind#(s(V1)) → a__isNatKind#(V1)mark#(length(X)) → a__length#(mark(X))
a__take#(s(M), cons(N, IL)) → a__isNatIList#(IL)mark#(U51(X1, X2, X3)) → mark#(X1)
a__isNatIList#(cons(V1, V2)) → a__isNatKind#(V1)mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)
mark#(length(X)) → mark#(X)mark#(U61(X1, X2, X3)) → a__U61#(mark(X1), X2, X3)
a__length#(cons(N, L)) → a__isNatList#(L)a__U11#(tt, V1) → a__isNatList#(V1)
a__U91#(tt, IL, M, N) → mark#(N)a__U71#(tt, L) → mark#(L)
mark#(U12(X)) → mark#(X)a__U61#(tt, V1, V2) → a__U62#(a__isNat(V1), V2)
mark#(U42(X1, X2)) → mark#(X1)a__isNatList#(take(V1, V2)) → a__U61#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
mark#(U52(X1, X2)) → mark#(X1)a__isNat#(length(V1)) → a__U11#(a__isNatIListKind(V1), V1)
a__U42#(tt, V2) → a__isNatIList#(V2)a__take#(s(M), cons(N, IL)) → a__U91#(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)
a__isNatList#(cons(V1, V2)) → a__and#(a__isNatKind(V1), isNatIListKind(V2))mark#(U51(X1, X2, X3)) → a__U51#(mark(X1), X2, X3)
mark#(U91(X1, X2, X3, X4)) → mark#(X1)mark#(U22(X)) → mark#(X)
a__length#(cons(N, L)) → a__and#(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))mark#(U43(X)) → mark#(X)
a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1)mark#(U21(X1, X2)) → a__U21#(mark(X1), X2)
a__U31#(tt, V) → a__isNatList#(V)mark#(take(X1, X2)) → a__take#(mark(X1), mark(X2))
a__isNatList#(cons(V1, V2)) → a__U51#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)a__U41#(tt, V1, V2) → a__U42#(a__isNat(V1), V2)
mark#(isNatKind(X)) → a__isNatKind#(X)mark#(U11(X1, X2)) → a__U11#(mark(X1), X2)
mark#(take(X1, X2)) → mark#(X2)mark#(U91(X1, X2, X3, X4)) → a__U91#(mark(X1), X2, X3, X4)
a__U62#(tt, V2) → a__isNatIList#(V2)a__take#(0, IL) → a__and#(a__isNatIList(IL), isNatIListKind(IL))