Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U111(tt, L, N) → U112(isNatIListKind(L), L, N)
U112(tt, L, N) → U113(isNat(N), L, N)
U113(tt, L, N) → U114(isNatKind(N), L)
U114(tt, L) → s(length(L))
U12(tt, V1) → U13(isNatList(V1))
U121(tt, IL) → U122(isNatIListKind(IL))
U122(tt) → nil
U13(tt) → tt
U131(tt, IL, M, N) → U132(isNatIListKind(IL), IL, M, N)
U132(tt, IL, M, N) → U133(isNat(M), IL, M, N)
U133(tt, IL, M, N) → U134(isNatKind(M), IL, M, N)
U134(tt, IL, M, N) → U135(isNat(N), IL, M, N)
U135(tt, IL, M, N) → U136(isNatKind(N), IL, M, N)
U136(tt, IL, M, N) → cons(N, take(M, IL))
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U111(isNatList(L), L, N)
take(0, IL) → U121(isNatIList(IL), IL)
take(s(M), cons(N, IL)) → U131(isNatIList(IL), IL, M, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U101: {1}
tt: empty set
U102: {1}
isNatKind: empty set
U103: {1}
isNatIListKind: empty set
U104: {1}
U105: {1}
isNat: empty set
U106: {1}
isNatIList: empty set
U11: {1}
U12: {1}
U111: {1}
U112: {1}
U113: {1}
U114: {1}
s: {1}
length: {1}
U13: {1}
isNatList: empty set
U121: {1}
U122: {1}
nil: empty set
U131: {1}
U132: {1}
U133: {1}
U134: {1}
U135: {1}
U136: {1}
take: {1, 2}
U21: {1}
U22: {1}
U23: {1}
U31: {1}
U32: {1}
U33: {1}
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U61: {1}
U62: {1}
U71: {1}
U81: {1}
U91: {1}
U92: {1}
U93: {1}
U94: {1}
U95: {1}
U96: {1}


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U111(tt, L, N) → U112(isNatIListKind(L), L, N)
U112(tt, L, N) → U113(isNat(N), L, N)
U113(tt, L, N) → U114(isNatKind(N), L)
U114(tt, L) → s(length(L))
U12(tt, V1) → U13(isNatList(V1))
U121(tt, IL) → U122(isNatIListKind(IL))
U122(tt) → nil
U13(tt) → tt
U131(tt, IL, M, N) → U132(isNatIListKind(IL), IL, M, N)
U132(tt, IL, M, N) → U133(isNat(M), IL, M, N)
U133(tt, IL, M, N) → U134(isNatKind(M), IL, M, N)
U134(tt, IL, M, N) → U135(isNat(N), IL, M, N)
U135(tt, IL, M, N) → U136(isNatKind(N), IL, M, N)
U136(tt, IL, M, N) → cons(N, take(M, IL))
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U111(isNatList(L), L, N)
take(0, IL) → U121(isNatIList(IL), IL)
take(s(M), cons(N, IL)) → U131(isNatIList(IL), IL, M, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U101: {1}
tt: empty set
U102: {1}
isNatKind: empty set
U103: {1}
isNatIListKind: empty set
U104: {1}
U105: {1}
isNat: empty set
U106: {1}
isNatIList: empty set
U11: {1}
U12: {1}
U111: {1}
U112: {1}
U113: {1}
U114: {1}
s: {1}
length: {1}
U13: {1}
isNatList: empty set
U121: {1}
U122: {1}
nil: empty set
U131: {1}
U132: {1}
U133: {1}
U134: {1}
U135: {1}
U136: {1}
take: {1, 2}
U21: {1}
U22: {1}
U23: {1}
U31: {1}
U32: {1}
U33: {1}
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U61: {1}
U62: {1}
U71: {1}
U81: {1}
U91: {1}
U92: {1}
U93: {1}
U94: {1}
U95: {1}
U96: {1}

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, s, length, U13, U122, take, U23, U33, U46, U52, U62, U71, U81, U96, U1061, LENGTH, U131, U1221, U231, U331, U461, U521, U621, U961, U711, U811, TAKE} are replacing on all positions.
For all symbols f in {cons, U101, U102, U103, U104, U105, U11, U12, U111, U112, U113, U114, U121, U131, U132, U133, U134, U135, U136, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U61, U91, U92, U93, U94, U95, U1021, U1011, U1031, U1041, U1051, U121, U111, U1121, U1111, U1131, U1141, U1211, U1321, U1311, U1331, U1341, U1351, U1361, U221, U211, U321, U311, U421, U411, U431, U441, U451, U511, U611, U921, U911, U931, U941, U951} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, isNat, isNatIList, isNatList, ISNATKIND, ISNATILISTKIND, ISNAT, ISNATILIST, ISNATLIST, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

U1011(tt, V1, V2) → U1021(isNatKind(V1), V1, V2)
U1011(tt, V1, V2) → ISNATKIND(V1)
U1021(tt, V1, V2) → U1031(isNatIListKind(V2), V1, V2)
U1021(tt, V1, V2) → ISNATILISTKIND(V2)
U1031(tt, V1, V2) → U1041(isNatIListKind(V2), V1, V2)
U1031(tt, V1, V2) → ISNATILISTKIND(V2)
U1041(tt, V1, V2) → U1051(isNat(V1), V2)
U1041(tt, V1, V2) → ISNAT(V1)
U1051(tt, V2) → U1061(isNatIList(V2))
U1051(tt, V2) → ISNATILIST(V2)
U111(tt, V1) → U121(isNatIListKind(V1), V1)
U111(tt, V1) → ISNATILISTKIND(V1)
U1111(tt, L, N) → U1121(isNatIListKind(L), L, N)
U1111(tt, L, N) → ISNATILISTKIND(L)
U1121(tt, L, N) → U1131(isNat(N), L, N)
U1121(tt, L, N) → ISNAT(N)
U1131(tt, L, N) → U1141(isNatKind(N), L)
U1131(tt, L, N) → ISNATKIND(N)
U1141(tt, L) → LENGTH(L)
U121(tt, V1) → U131(isNatList(V1))
U121(tt, V1) → ISNATLIST(V1)
U1211(tt, IL) → U1221(isNatIListKind(IL))
U1211(tt, IL) → ISNATILISTKIND(IL)
U1311(tt, IL, M, N) → U1321(isNatIListKind(IL), IL, M, N)
U1311(tt, IL, M, N) → ISNATILISTKIND(IL)
U1321(tt, IL, M, N) → U1331(isNat(M), IL, M, N)
U1321(tt, IL, M, N) → ISNAT(M)
U1331(tt, IL, M, N) → U1341(isNatKind(M), IL, M, N)
U1331(tt, IL, M, N) → ISNATKIND(M)
U1341(tt, IL, M, N) → U1351(isNat(N), IL, M, N)
U1341(tt, IL, M, N) → ISNAT(N)
U1351(tt, IL, M, N) → U1361(isNatKind(N), IL, M, N)
U1351(tt, IL, M, N) → ISNATKIND(N)
U211(tt, V1) → U221(isNatKind(V1), V1)
U211(tt, V1) → ISNATKIND(V1)
U221(tt, V1) → U231(isNat(V1))
U221(tt, V1) → ISNAT(V1)
U311(tt, V) → U321(isNatIListKind(V), V)
U311(tt, V) → ISNATILISTKIND(V)
U321(tt, V) → U331(isNatList(V))
U321(tt, V) → ISNATLIST(V)
U411(tt, V1, V2) → U421(isNatKind(V1), V1, V2)
U411(tt, V1, V2) → ISNATKIND(V1)
U421(tt, V1, V2) → U431(isNatIListKind(V2), V1, V2)
U421(tt, V1, V2) → ISNATILISTKIND(V2)
U431(tt, V1, V2) → U441(isNatIListKind(V2), V1, V2)
U431(tt, V1, V2) → ISNATILISTKIND(V2)
U441(tt, V1, V2) → U451(isNat(V1), V2)
U441(tt, V1, V2) → ISNAT(V1)
U451(tt, V2) → U461(isNatIList(V2))
U451(tt, V2) → ISNATILIST(V2)
U511(tt, V2) → U521(isNatIListKind(V2))
U511(tt, V2) → ISNATILISTKIND(V2)
U611(tt, V2) → U621(isNatIListKind(V2))
U611(tt, V2) → ISNATILISTKIND(V2)
U911(tt, V1, V2) → U921(isNatKind(V1), V1, V2)
U911(tt, V1, V2) → ISNATKIND(V1)
U921(tt, V1, V2) → U931(isNatIListKind(V2), V1, V2)
U921(tt, V1, V2) → ISNATILISTKIND(V2)
U931(tt, V1, V2) → U941(isNatIListKind(V2), V1, V2)
U931(tt, V1, V2) → ISNATILISTKIND(V2)
U941(tt, V1, V2) → U951(isNat(V1), V2)
U941(tt, V1, V2) → ISNAT(V1)
U951(tt, V2) → U961(isNatList(V2))
U951(tt, V2) → ISNATLIST(V2)
ISNAT(length(V1)) → U111(isNatIListKind(V1), V1)
ISNAT(length(V1)) → ISNATILISTKIND(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
ISNAT(s(V1)) → ISNATKIND(V1)
ISNATILIST(V) → U311(isNatIListKind(V), V)
ISNATILIST(V) → ISNATILISTKIND(V)
ISNATILIST(cons(V1, V2)) → U411(isNatKind(V1), V1, V2)
ISNATILIST(cons(V1, V2)) → ISNATKIND(V1)
ISNATILISTKIND(cons(V1, V2)) → U511(isNatKind(V1), V2)
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATILISTKIND(take(V1, V2)) → U611(isNatKind(V1), V2)
ISNATILISTKIND(take(V1, V2)) → ISNATKIND(V1)
ISNATKIND(length(V1)) → U711(isNatIListKind(V1))
ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
ISNATKIND(s(V1)) → U811(isNatKind(V1))
ISNATKIND(s(V1)) → ISNATKIND(V1)
ISNATLIST(cons(V1, V2)) → U911(isNatKind(V1), V1, V2)
ISNATLIST(cons(V1, V2)) → ISNATKIND(V1)
ISNATLIST(take(V1, V2)) → U1011(isNatKind(V1), V1, V2)
ISNATLIST(take(V1, V2)) → ISNATKIND(V1)
LENGTH(cons(N, L)) → U1111(isNatList(L), L, N)
LENGTH(cons(N, L)) → ISNATLIST(L)
TAKE(0, IL) → U1211(isNatIList(IL), IL)
TAKE(0, IL) → ISNATILIST(IL)
TAKE(s(M), cons(N, IL)) → U1311(isNatIList(IL), IL, M, N)
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)

The collapsing dependency pairs are DPc:

U1141(tt, L) → L
U1361(tt, IL, M, N) → N


The hidden terms of R are:

zeros
take(M, IL)

Every hiding context is built from:

take on positions {1, 2}

Hence, the new unhiding pairs DPu are :

U1141(tt, L) → U(L)
U1361(tt, IL, M, N) → U(N)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(zeros) → ZEROS
U(take(M, IL)) → TAKE(M, IL)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U111(tt, L, N) → U112(isNatIListKind(L), L, N)
U112(tt, L, N) → U113(isNat(N), L, N)
U113(tt, L, N) → U114(isNatKind(N), L)
U114(tt, L) → s(length(L))
U12(tt, V1) → U13(isNatList(V1))
U121(tt, IL) → U122(isNatIListKind(IL))
U122(tt) → nil
U13(tt) → tt
U131(tt, IL, M, N) → U132(isNatIListKind(IL), IL, M, N)
U132(tt, IL, M, N) → U133(isNat(M), IL, M, N)
U133(tt, IL, M, N) → U134(isNatKind(M), IL, M, N)
U134(tt, IL, M, N) → U135(isNat(N), IL, M, N)
U135(tt, IL, M, N) → U136(isNatKind(N), IL, M, N)
U136(tt, IL, M, N) → cons(N, take(M, IL))
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U111(isNatList(L), L, N)
take(0, IL) → U121(isNatIList(IL), IL)
take(s(M), cons(N, IL)) → U131(isNatIList(IL), IL, M, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 4 SCCs with 44 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, s, length, U13, U122, take, U23, U33, U46, U52, U62, U71, U81, U96} are replacing on all positions.
For all symbols f in {cons, U101, U102, U103, U104, U105, U11, U12, U111, U112, U113, U114, U121, U131, U132, U133, U134, U135, U136, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U61, U91, U92, U93, U94, U95, U511, U611} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, isNat, isNatIList, isNatList, ISNATILISTKIND, ISNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
ISNATILISTKIND(cons(V1, V2)) → U511(isNatKind(V1), V2)
U511(tt, V2) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
ISNATILISTKIND(take(V1, V2)) → U611(isNatKind(V1), V2)
U611(tt, V2) → ISNATILISTKIND(V2)
ISNATILISTKIND(take(V1, V2)) → ISNATKIND(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U111(tt, L, N) → U112(isNatIListKind(L), L, N)
U112(tt, L, N) → U113(isNat(N), L, N)
U113(tt, L, N) → U114(isNatKind(N), L)
U114(tt, L) → s(length(L))
U12(tt, V1) → U13(isNatList(V1))
U121(tt, IL) → U122(isNatIListKind(IL))
U122(tt) → nil
U13(tt) → tt
U131(tt, IL, M, N) → U132(isNatIListKind(IL), IL, M, N)
U132(tt, IL, M, N) → U133(isNat(M), IL, M, N)
U133(tt, IL, M, N) → U134(isNatKind(M), IL, M, N)
U134(tt, IL, M, N) → U135(isNat(N), IL, M, N)
U135(tt, IL, M, N) → U136(isNatKind(N), IL, M, N)
U136(tt, IL, M, N) → cons(N, take(M, IL))
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U111(isNatList(L), L, N)
take(0, IL) → U121(isNatIList(IL), IL)
take(s(M), cons(N, IL)) → U131(isNatIList(IL), IL, M, N)

Q is empty.

The following rules are not useable and can be deleted:

zeros → cons(0, zeros)
U101(tt, x0, x1) → U102(isNatKind(x0), x0, x1)
U102(tt, x0, x1) → U103(isNatIListKind(x1), x0, x1)
U103(tt, x0, x1) → U104(isNatIListKind(x1), x0, x1)
U104(tt, x0, x1) → U105(isNat(x0), x1)
U105(tt, x0) → U106(isNatIList(x0))
U106(tt) → tt
U11(tt, x0) → U12(isNatIListKind(x0), x0)
U111(tt, x0, x1) → U112(isNatIListKind(x0), x0, x1)
U112(tt, x0, x1) → U113(isNat(x1), x0, x1)
U113(tt, x0, x1) → U114(isNatKind(x1), x0)
U114(tt, x0) → s(length(x0))
U12(tt, x0) → U13(isNatList(x0))
U121(tt, x0) → U122(isNatIListKind(x0))
U122(tt) → nil
U13(tt) → tt
U131(tt, x0, x1, x2) → U132(isNatIListKind(x0), x0, x1, x2)
U132(tt, x0, x1, x2) → U133(isNat(x1), x0, x1, x2)
U133(tt, x0, x1, x2) → U134(isNatKind(x1), x0, x1, x2)
U134(tt, x0, x1, x2) → U135(isNat(x2), x0, x1, x2)
U135(tt, x0, x1, x2) → U136(isNatKind(x2), x0, x1, x2)
U136(tt, x0, x1, x2) → cons(x2, take(x1, x0))
U21(tt, x0) → U22(isNatKind(x0), x0)
U22(tt, x0) → U23(isNat(x0))
U23(tt) → tt
U31(tt, x0) → U32(isNatIListKind(x0), x0)
U32(tt, x0) → U33(isNatList(x0))
U33(tt) → tt
U41(tt, x0, x1) → U42(isNatKind(x0), x0, x1)
U42(tt, x0, x1) → U43(isNatIListKind(x1), x0, x1)
U43(tt, x0, x1) → U44(isNatIListKind(x1), x0, x1)
U44(tt, x0, x1) → U45(isNat(x0), x1)
U45(tt, x0) → U46(isNatIList(x0))
U46(tt) → tt
U91(tt, x0, x1) → U92(isNatKind(x0), x0, x1)
U92(tt, x0, x1) → U93(isNatIListKind(x1), x0, x1)
U93(tt, x0, x1) → U94(isNatIListKind(x1), x0, x1)
U94(tt, x0, x1) → U95(isNat(x0), x1)
U95(tt, x0) → U96(isNatList(x0))
U96(tt) → tt
isNat(0) → tt
isNat(length(x0)) → U11(isNatIListKind(x0), x0)
isNat(s(x0)) → U21(isNatKind(x0), x0)
isNatIList(x0) → U31(isNatIListKind(x0), x0)
isNatIList(zeros) → tt
isNatIList(cons(x0, x1)) → U41(isNatKind(x0), x0, x1)
isNatList(nil) → tt
isNatList(cons(x0, x1)) → U91(isNatKind(x0), x0, x1)
isNatList(take(x0, x1)) → U101(isNatKind(x0), x0, x1)
length(nil) → 0
length(cons(x0, x1)) → U111(isNatList(x1), x1, x0)
take(0, x0) → U121(isNatIList(x0), x0)
take(s(x0), cons(x1, x2)) → U131(isNatIList(x2), x2, x0, x1)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U71, s, U81, U52, take, U62} are replacing on all positions.
For all symbols f in {cons, U51, U61, U511, U611} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, ISNATILISTKIND, ISNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
ISNATILISTKIND(cons(V1, V2)) → U511(isNatKind(V1), V2)
U511(tt, V2) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
ISNATILISTKIND(take(V1, V2)) → U611(isNatKind(V1), V2)
U611(tt, V2) → ISNATILISTKIND(V2)
ISNATILISTKIND(take(V1, V2)) → ISNATKIND(V1)

The TRS R consists of the following rules:

isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(s(V1)) → U81(isNatKind(V1))
U81(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U52(tt) → tt
U71(tt) → tt

Q is empty.

Using the order
Polynomial interpretation with max and min functions [25]:

POL(0) = 1   
POL(ISNATILISTKIND(x1)) = 1 + x1   
POL(ISNATKIND(x1)) = x1   
POL(U51(x1, x2)) = 1   
POL(U511(x1, x2)) = 1 + x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2)) = 1   
POL(U611(x1, x2)) = 1 + x2   
POL(U62(x1)) = x1   
POL(U71(x1)) = 1 + x1   
POL(U81(x1)) = 1   
POL(cons(x1, x2)) = 1 + x1 + x2   
POL(isNatIListKind(x1)) = 1   
POL(isNatKind(x1)) = 1 + x1   
POL(length(x1)) = 1 + x1   
POL(nil) = 0   
POL(s(x1)) = 1 + x1   
POL(take(x1, x2)) = 1 + x1 + x2   
POL(tt) = 1   
POL(zeros) = 0   

the following usable rules

isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
U71(tt) → tt
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U81(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNATILISTKIND(cons(V1, V2)) → U511(isNatKind(V1), V2)
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
ISNATILISTKIND(take(V1, V2)) → U611(isNatKind(V1), V2)
ISNATILISTKIND(take(V1, V2)) → ISNATKIND(V1)

could be oriented strictly and thus removed.
The pairs

ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
U511(tt, V2) → ISNATILISTKIND(V2)
U611(tt, V2) → ISNATILISTKIND(V2)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U71, s, U81, U52, take, U62} are replacing on all positions.
For all symbols f in {cons, U51, U61, U511, U611} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, ISNATILISTKIND, ISNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
U511(tt, V2) → ISNATILISTKIND(V2)
U611(tt, V2) → ISNATILISTKIND(V2)

The TRS R consists of the following rules:

isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(s(V1)) → U81(isNatKind(V1))
U81(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U52(tt) → tt
U71(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, s, length, U13, U122, take, U23, U33, U46, U52, U62, U71, U81, U96} are replacing on all positions.
For all symbols f in {cons, U101, U102, U103, U104, U105, U11, U12, U111, U112, U113, U114, U121, U131, U132, U133, U134, U135, U136, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U61, U91, U92, U93, U94, U95, U1031, U1021, U1041, U1051, U311, U321, U911, U921, U931, U941, U951, U1011, U111, U121, U211, U221, U411, U421, U431, U441, U451} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, isNat, isNatIList, isNatList, ISNATILIST, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

U1021(tt, V1, V2) → U1031(isNatIListKind(V2), V1, V2)
U1031(tt, V1, V2) → U1041(isNatIListKind(V2), V1, V2)
U1041(tt, V1, V2) → U1051(isNat(V1), V2)
U1051(tt, V2) → ISNATILIST(V2)
ISNATILIST(V) → U311(isNatIListKind(V), V)
U311(tt, V) → U321(isNatIListKind(V), V)
U321(tt, V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → U911(isNatKind(V1), V1, V2)
U911(tt, V1, V2) → U921(isNatKind(V1), V1, V2)
U921(tt, V1, V2) → U931(isNatIListKind(V2), V1, V2)
U931(tt, V1, V2) → U941(isNatIListKind(V2), V1, V2)
U941(tt, V1, V2) → U951(isNat(V1), V2)
U951(tt, V2) → ISNATLIST(V2)
ISNATLIST(take(V1, V2)) → U1011(isNatKind(V1), V1, V2)
U1011(tt, V1, V2) → U1021(isNatKind(V1), V1, V2)
U941(tt, V1, V2) → ISNAT(V1)
ISNAT(length(V1)) → U111(isNatIListKind(V1), V1)
U111(tt, V1) → U121(isNatIListKind(V1), V1)
U121(tt, V1) → ISNATLIST(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U211(tt, V1) → U221(isNatKind(V1), V1)
U221(tt, V1) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → U411(isNatKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isNatKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isNatIListKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isNatIListKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isNat(V1), V2)
U451(tt, V2) → ISNATILIST(V2)
U441(tt, V1, V2) → ISNAT(V1)
U1041(tt, V1, V2) → ISNAT(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U111(tt, L, N) → U112(isNatIListKind(L), L, N)
U112(tt, L, N) → U113(isNat(N), L, N)
U113(tt, L, N) → U114(isNatKind(N), L)
U114(tt, L) → s(length(L))
U12(tt, V1) → U13(isNatList(V1))
U121(tt, IL) → U122(isNatIListKind(IL))
U122(tt) → nil
U13(tt) → tt
U131(tt, IL, M, N) → U132(isNatIListKind(IL), IL, M, N)
U132(tt, IL, M, N) → U133(isNat(M), IL, M, N)
U133(tt, IL, M, N) → U134(isNatKind(M), IL, M, N)
U134(tt, IL, M, N) → U135(isNat(N), IL, M, N)
U135(tt, IL, M, N) → U136(isNatKind(N), IL, M, N)
U136(tt, IL, M, N) → cons(N, take(M, IL))
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U111(isNatList(L), L, N)
take(0, IL) → U121(isNatIList(IL), IL)
take(s(M), cons(N, IL)) → U131(isNatIList(IL), IL, M, N)

Q is empty.

The following rules are not useable and can be deleted:

zeros → cons(0, zeros)
U111(tt, x0, x1) → U112(isNatIListKind(x0), x0, x1)
U112(tt, x0, x1) → U113(isNat(x1), x0, x1)
U113(tt, x0, x1) → U114(isNatKind(x1), x0)
U114(tt, x0) → s(length(x0))
U121(tt, x0) → U122(isNatIListKind(x0))
U122(tt) → nil
U131(tt, x0, x1, x2) → U132(isNatIListKind(x0), x0, x1, x2)
U132(tt, x0, x1, x2) → U133(isNat(x1), x0, x1, x2)
U133(tt, x0, x1, x2) → U134(isNatKind(x1), x0, x1, x2)
U134(tt, x0, x1, x2) → U135(isNat(x2), x0, x1, x2)
U135(tt, x0, x1, x2) → U136(isNatKind(x2), x0, x1, x2)
U136(tt, x0, x1, x2) → cons(x2, take(x1, x0))
length(nil) → 0
length(cons(x0, x1)) → U111(isNatList(x1), x1, x0)
take(0, x0) → U121(isNatIList(x0), x0)
take(s(x0), cons(x1, x2)) → U131(isNatIList(x2), x2, x0, x1)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U71, take, s, U81, U62, U52, U13, U23, U96, U106, U33, U46} are replacing on all positions.
For all symbols f in {cons, U51, U61, U11, U12, U91, U92, U93, U94, U95, U21, U22, U101, U102, U103, U104, U105, U31, U32, U41, U42, U43, U44, U45, U1031, U1021, U1041, U1051, U311, U321, U911, U921, U931, U941, U951, U1011, U111, U121, U211, U221, U411, U421, U431, U441, U451} we have µ(f) = {1}.
The symbols in {isNatIListKind, isNatKind, isNat, isNatList, isNatIList, ISNATILIST, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

U1021(tt, V1, V2) → U1031(isNatIListKind(V2), V1, V2)
U1031(tt, V1, V2) → U1041(isNatIListKind(V2), V1, V2)
U1041(tt, V1, V2) → U1051(isNat(V1), V2)
U1051(tt, V2) → ISNATILIST(V2)
ISNATILIST(V) → U311(isNatIListKind(V), V)
U311(tt, V) → U321(isNatIListKind(V), V)
U321(tt, V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → U911(isNatKind(V1), V1, V2)
U911(tt, V1, V2) → U921(isNatKind(V1), V1, V2)
U921(tt, V1, V2) → U931(isNatIListKind(V2), V1, V2)
U931(tt, V1, V2) → U941(isNatIListKind(V2), V1, V2)
U941(tt, V1, V2) → U951(isNat(V1), V2)
U951(tt, V2) → ISNATLIST(V2)
ISNATLIST(take(V1, V2)) → U1011(isNatKind(V1), V1, V2)
U1011(tt, V1, V2) → U1021(isNatKind(V1), V1, V2)
U941(tt, V1, V2) → ISNAT(V1)
ISNAT(length(V1)) → U111(isNatIListKind(V1), V1)
U111(tt, V1) → U121(isNatIListKind(V1), V1)
U121(tt, V1) → ISNATLIST(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U211(tt, V1) → U221(isNatKind(V1), V1)
U221(tt, V1) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → U411(isNatKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isNatKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isNatIListKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isNatIListKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isNat(V1), V2)
U451(tt, V2) → ISNATILIST(V2)
U441(tt, V1, V2) → ISNAT(V1)
U1041(tt, V1, V2) → ISNAT(V1)

The TRS R consists of the following rules:

isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(s(V1)) → U81(isNatKind(V1))
U81(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U95(tt, V2) → U96(isNatList(V2))
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
isNatIList(V) → U31(isNatIListKind(V), V)
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U106(tt) → tt
U96(tt) → tt
U13(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 1   
POL(ISNAT(x1)) = x1   
POL(ISNATILIST(x1)) = 1 + x1   
POL(ISNATLIST(x1)) = 1 + x1   
POL(U101(x1, x2, x3)) = 0   
POL(U1011(x1, x2, x3)) = 2 + 2·x2 + x3   
POL(U102(x1, x2, x3)) = 0   
POL(U1021(x1, x2, x3)) = 1 + 2·x2 + x3   
POL(U103(x1, x2, x3)) = 0   
POL(U1031(x1, x2, x3)) = 1 + 2·x2 + x3   
POL(U104(x1, x2, x3)) = 2·x1   
POL(U1041(x1, x2, x3)) = 1 + 2·x2 + x3   
POL(U105(x1, x2)) = 0   
POL(U1051(x1, x2)) = 1 + x2   
POL(U106(x1)) = 0   
POL(U11(x1, x2)) = 2·x1   
POL(U111(x1, x2)) = 1 + 2·x2   
POL(U12(x1, x2)) = 2·x1   
POL(U121(x1, x2)) = 1 + 2·x2   
POL(U13(x1)) = 2·x1   
POL(U21(x1, x2)) = 2·x1   
POL(U211(x1, x2)) = 1 + 2·x2   
POL(U22(x1, x2)) = 2·x1   
POL(U221(x1, x2)) = 1 + 2·x2   
POL(U23(x1)) = x1   
POL(U31(x1, x2)) = 1 + 2·x1   
POL(U311(x1, x2)) = 1 + x2   
POL(U32(x1, x2)) = 0   
POL(U321(x1, x2)) = 1 + x2   
POL(U33(x1)) = x1   
POL(U41(x1, x2, x3)) = 2   
POL(U411(x1, x2, x3)) = 2 + x2 + 2·x3   
POL(U42(x1, x2, x3)) = 2 + 2·x1   
POL(U421(x1, x2, x3)) = 2 + x2 + x3   
POL(U43(x1, x2, x3)) = 0   
POL(U431(x1, x2, x3)) = 2 + x2 + x3   
POL(U44(x1, x2, x3)) = 2·x1   
POL(U441(x1, x2, x3)) = 1 + x2 + x3   
POL(U45(x1, x2)) = 2·x1   
POL(U451(x1, x2)) = 1 + x2   
POL(U46(x1)) = 0   
POL(U51(x1, x2)) = 0   
POL(U52(x1)) = x1   
POL(U61(x1, x2)) = 0   
POL(U62(x1)) = 2·x1   
POL(U71(x1)) = x1   
POL(U81(x1)) = 2·x1   
POL(U91(x1, x2, x3)) = 2·x1   
POL(U911(x1, x2, x3)) = 2 + x2 + 2·x3   
POL(U92(x1, x2, x3)) = 0   
POL(U921(x1, x2, x3)) = 2 + x2 + 2·x3   
POL(U93(x1, x2, x3)) = 0   
POL(U931(x1, x2, x3)) = 1 + x2 + x3   
POL(U94(x1, x2, x3)) = x1   
POL(U941(x1, x2, x3)) = 1 + x2 + x3   
POL(U95(x1, x2)) = x1   
POL(U951(x1, x2)) = 1 + x2   
POL(U96(x1)) = x1   
POL(cons(x1, x2)) = 1 + x1 + 2·x2   
POL(isNat(x1)) = 0   
POL(isNatIList(x1)) = 2   
POL(isNatIListKind(x1)) = 0   
POL(isNatKind(x1)) = 0   
POL(isNatList(x1)) = 0   
POL(length(x1)) = 2 + 2·x1   
POL(nil) = 0   
POL(s(x1)) = 2 + 2·x1   
POL(take(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(tt) = 0   
POL(zeros) = 2   

the following usable rules

isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
U71(tt) → tt
U81(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

U921(tt, V1, V2) → U931(isNatIListKind(V2), V1, V2)
ISNATLIST(take(V1, V2)) → U1011(isNatKind(V1), V1, V2)
U1011(tt, V1, V2) → U1021(isNatKind(V1), V1, V2)
U941(tt, V1, V2) → ISNAT(V1)
ISNAT(length(V1)) → U111(isNatIListKind(V1), V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U221(tt, V1) → ISNAT(V1)
U431(tt, V1, V2) → U441(isNatIListKind(V2), V1, V2)
U441(tt, V1, V2) → ISNAT(V1)
U1041(tt, V1, V2) → ISNAT(V1)

could be oriented strictly and thus removed.
The pairs

U1021(tt, V1, V2) → U1031(isNatIListKind(V2), V1, V2)
U1031(tt, V1, V2) → U1041(isNatIListKind(V2), V1, V2)
U1041(tt, V1, V2) → U1051(isNat(V1), V2)
U1051(tt, V2) → ISNATILIST(V2)
ISNATILIST(V) → U311(isNatIListKind(V), V)
U311(tt, V) → U321(isNatIListKind(V), V)
U321(tt, V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → U911(isNatKind(V1), V1, V2)
U911(tt, V1, V2) → U921(isNatKind(V1), V1, V2)
U931(tt, V1, V2) → U941(isNatIListKind(V2), V1, V2)
U941(tt, V1, V2) → U951(isNat(V1), V2)
U951(tt, V2) → ISNATLIST(V2)
U111(tt, V1) → U121(isNatIListKind(V1), V1)
U121(tt, V1) → ISNATLIST(V1)
U211(tt, V1) → U221(isNatKind(V1), V1)
ISNATILIST(cons(V1, V2)) → U411(isNatKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isNatKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isNatIListKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isNat(V1), V2)
U451(tt, V2) → ISNATILIST(V2)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U71, take, s, U81, U62, U52, U13, U23, U96, U106, U33, U46} are replacing on all positions.
For all symbols f in {cons, U51, U61, U11, U12, U91, U92, U93, U94, U95, U21, U22, U101, U102, U103, U104, U105, U31, U32, U41, U42, U43, U44, U45, U1031, U1021, U1041, U1051, U311, U321, U911, U921, U941, U931, U951, U121, U111, U221, U211, U411, U421, U431, U451, U441} we have µ(f) = {1}.
The symbols in {isNatIListKind, isNatKind, isNat, isNatList, isNatIList, ISNATILIST, ISNATLIST} are not replacing on any position.

The TRS P consists of the following rules:

U1021(tt, V1, V2) → U1031(isNatIListKind(V2), V1, V2)
U1031(tt, V1, V2) → U1041(isNatIListKind(V2), V1, V2)
U1041(tt, V1, V2) → U1051(isNat(V1), V2)
U1051(tt, V2) → ISNATILIST(V2)
ISNATILIST(V) → U311(isNatIListKind(V), V)
U311(tt, V) → U321(isNatIListKind(V), V)
U321(tt, V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → U911(isNatKind(V1), V1, V2)
U911(tt, V1, V2) → U921(isNatKind(V1), V1, V2)
U931(tt, V1, V2) → U941(isNatIListKind(V2), V1, V2)
U941(tt, V1, V2) → U951(isNat(V1), V2)
U951(tt, V2) → ISNATLIST(V2)
U111(tt, V1) → U121(isNatIListKind(V1), V1)
U121(tt, V1) → ISNATLIST(V1)
U211(tt, V1) → U221(isNatKind(V1), V1)
ISNATILIST(cons(V1, V2)) → U411(isNatKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isNatKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isNatIListKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isNat(V1), V2)
U451(tt, V2) → ISNATILIST(V2)

The TRS R consists of the following rules:

isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(s(V1)) → U81(isNatKind(V1))
U81(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U95(tt, V2) → U96(isNatList(V2))
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
isNatIList(V) → U31(isNatIListKind(V), V)
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U106(tt) → tt
U96(tt) → tt
U13(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 19 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, s, length, U13, U122, take, U23, U33, U46, U52, U62, U71, U81, U96, TAKE} are replacing on all positions.
For all symbols f in {cons, U101, U102, U103, U104, U105, U11, U12, U111, U112, U113, U114, U121, U131, U132, U133, U134, U135, U136, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U61, U91, U92, U93, U94, U95, U1331, U1321, U1341, U1351, U1361, U1311} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, isNat, isNatIList, isNatList, U} are not replacing on any position.

The TRS P consists of the following rules:

U1321(tt, IL, M, N) → U1331(isNat(M), IL, M, N)
U1331(tt, IL, M, N) → U1341(isNatKind(M), IL, M, N)
U1341(tt, IL, M, N) → U1351(isNat(N), IL, M, N)
U1351(tt, IL, M, N) → U1361(isNatKind(N), IL, M, N)
U1361(tt, IL, M, N) → U(N)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(take(M, IL)) → TAKE(M, IL)
TAKE(s(M), cons(N, IL)) → U1311(isNatIList(IL), IL, M, N)
U1311(tt, IL, M, N) → U1321(isNatIListKind(IL), IL, M, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U111(tt, L, N) → U112(isNatIListKind(L), L, N)
U112(tt, L, N) → U113(isNat(N), L, N)
U113(tt, L, N) → U114(isNatKind(N), L)
U114(tt, L) → s(length(L))
U12(tt, V1) → U13(isNatList(V1))
U121(tt, IL) → U122(isNatIListKind(IL))
U122(tt) → nil
U13(tt) → tt
U131(tt, IL, M, N) → U132(isNatIListKind(IL), IL, M, N)
U132(tt, IL, M, N) → U133(isNat(M), IL, M, N)
U133(tt, IL, M, N) → U134(isNatKind(M), IL, M, N)
U134(tt, IL, M, N) → U135(isNat(N), IL, M, N)
U135(tt, IL, M, N) → U136(isNatKind(N), IL, M, N)
U136(tt, IL, M, N) → cons(N, take(M, IL))
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U111(isNatList(L), L, N)
take(0, IL) → U121(isNatIList(IL), IL)
take(s(M), cons(N, IL)) → U131(isNatIList(IL), IL, M, N)

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(take(M, IL)) → TAKE(M, IL)
TAKE(s(M), cons(N, IL)) → U1311(isNatIList(IL), IL, M, N)
The remaining pairs can at least be oriented weakly.

U1321(tt, IL, M, N) → U1331(isNat(M), IL, M, N)
U1331(tt, IL, M, N) → U1341(isNatKind(M), IL, M, N)
U1341(tt, IL, M, N) → U1351(isNat(N), IL, M, N)
U1351(tt, IL, M, N) → U1361(isNatKind(N), IL, M, N)
U1361(tt, IL, M, N) → U(N)
U1311(tt, IL, M, N) → U1321(isNatIListKind(IL), IL, M, N)
Used ordering: Combined order from the following AFS and order.
U1331(x1, x2, x3, x4)  =  x4
U1321(x1, x2, x3, x4)  =  x4
U1341(x1, x2, x3, x4)  =  x4
U1351(x1, x2, x3, x4)  =  x4
U1361(x1, x2, x3, x4)  =  x4
U(x1)  =  x1
TAKE(x1, x2)  =  x2
U1311(x1, x2, x3, x4)  =  x4

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, s, length, U13, U122, take, U23, U33, U46, U52, U62, U71, U81, U96} are replacing on all positions.
For all symbols f in {cons, U101, U102, U103, U104, U105, U11, U12, U111, U112, U113, U114, U121, U131, U132, U133, U134, U135, U136, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U61, U91, U92, U93, U94, U95, U1331, U1321, U1341, U1351, U1361, U1311} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, isNat, isNatIList, isNatList, U} are not replacing on any position.

The TRS P consists of the following rules:

U1321(tt, IL, M, N) → U1331(isNat(M), IL, M, N)
U1331(tt, IL, M, N) → U1341(isNatKind(M), IL, M, N)
U1341(tt, IL, M, N) → U1351(isNat(N), IL, M, N)
U1351(tt, IL, M, N) → U1361(isNatKind(N), IL, M, N)
U1361(tt, IL, M, N) → U(N)
U1311(tt, IL, M, N) → U1321(isNatIListKind(IL), IL, M, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U111(tt, L, N) → U112(isNatIListKind(L), L, N)
U112(tt, L, N) → U113(isNat(N), L, N)
U113(tt, L, N) → U114(isNatKind(N), L)
U114(tt, L) → s(length(L))
U12(tt, V1) → U13(isNatList(V1))
U121(tt, IL) → U122(isNatIListKind(IL))
U122(tt) → nil
U13(tt) → tt
U131(tt, IL, M, N) → U132(isNatIListKind(IL), IL, M, N)
U132(tt, IL, M, N) → U133(isNat(M), IL, M, N)
U133(tt, IL, M, N) → U134(isNatKind(M), IL, M, N)
U134(tt, IL, M, N) → U135(isNat(N), IL, M, N)
U135(tt, IL, M, N) → U136(isNatKind(N), IL, M, N)
U136(tt, IL, M, N) → cons(N, take(M, IL))
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U111(isNatList(L), L, N)
take(0, IL) → U121(isNatIList(IL), IL)
take(s(M), cons(N, IL)) → U131(isNatIList(IL), IL, M, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 6 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, s, length, U13, U122, take, U23, U33, U46, U52, U62, U71, U81, U96, LENGTH} are replacing on all positions.
For all symbols f in {cons, U101, U102, U103, U104, U105, U11, U12, U111, U112, U113, U114, U121, U131, U132, U133, U134, U135, U136, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U61, U91, U92, U93, U94, U95, U1131, U1121, U1141, U1111} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, isNat, isNatIList, isNatList} are not replacing on any position.

The TRS P consists of the following rules:

U1121(tt, L, N) → U1131(isNat(N), L, N)
U1131(tt, L, N) → U1141(isNatKind(N), L)
U1141(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → U1111(isNatList(L), L, N)
U1111(tt, L, N) → U1121(isNatIListKind(L), L, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U111(tt, L, N) → U112(isNatIListKind(L), L, N)
U112(tt, L, N) → U113(isNat(N), L, N)
U113(tt, L, N) → U114(isNatKind(N), L)
U114(tt, L) → s(length(L))
U12(tt, V1) → U13(isNatList(V1))
U121(tt, IL) → U122(isNatIListKind(IL))
U122(tt) → nil
U13(tt) → tt
U131(tt, IL, M, N) → U132(isNatIListKind(IL), IL, M, N)
U132(tt, IL, M, N) → U133(isNat(M), IL, M, N)
U133(tt, IL, M, N) → U134(isNatKind(M), IL, M, N)
U134(tt, IL, M, N) → U135(isNat(N), IL, M, N)
U135(tt, IL, M, N) → U136(isNatKind(N), IL, M, N)
U136(tt, IL, M, N) → cons(N, take(M, IL))
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U111(isNatList(L), L, N)
take(0, IL) → U121(isNatIList(IL), IL)
take(s(M), cons(N, IL)) → U131(isNatIList(IL), IL, M, N)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 2   
POL(LENGTH(x1)) = 1 + 2·x1   
POL(U101(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U102(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U103(x1, x2, x3)) = 2·x2   
POL(U104(x1, x2, x3)) = 2·x2   
POL(U105(x1, x2)) = x1   
POL(U106(x1)) = 2   
POL(U11(x1, x2)) = 2·x2   
POL(U111(x1, x2, x3)) = 2·x2   
POL(U1111(x1, x2, x3)) = x1 + 2·x2   
POL(U112(x1, x2, x3)) = 2·x2   
POL(U1121(x1, x2, x3)) = 1 + 2·x2   
POL(U113(x1, x2, x3)) = 2·x2   
POL(U1131(x1, x2, x3)) = 1 + 2·x2   
POL(U114(x1, x2)) = 2·x2   
POL(U1141(x1, x2)) = 1 + 2·x2   
POL(U12(x1, x2)) = 2·x2   
POL(U121(x1, x2)) = 2 + x2   
POL(U122(x1)) = 2   
POL(U13(x1)) = x1   
POL(U131(x1, x2, x3, x4)) = 2·x2 + 2·x3   
POL(U132(x1, x2, x3, x4)) = 2·x2 + 2·x3   
POL(U133(x1, x2, x3, x4)) = 2·x2 + 2·x3   
POL(U134(x1, x2, x3, x4)) = 2·x2 + 2·x3   
POL(U135(x1, x2, x3, x4)) = 2·x2 + 2·x3   
POL(U136(x1, x2, x3, x4)) = 2·x2 + 2·x3   
POL(U21(x1, x2)) = 2·x2   
POL(U22(x1, x2)) = 2·x2   
POL(U23(x1)) = x1   
POL(U31(x1, x2)) = 2   
POL(U32(x1, x2)) = 2   
POL(U33(x1)) = 2   
POL(U41(x1, x2, x3)) = 2   
POL(U42(x1, x2, x3)) = 2   
POL(U43(x1, x2, x3)) = x1   
POL(U44(x1, x2, x3)) = 2   
POL(U45(x1, x2)) = 2   
POL(U46(x1)) = 2   
POL(U51(x1, x2)) = 2   
POL(U52(x1)) = x1   
POL(U61(x1, x2)) = 2   
POL(U62(x1)) = 2   
POL(U71(x1)) = 2   
POL(U81(x1)) = 2   
POL(U91(x1, x2, x3)) = 2·x3   
POL(U92(x1, x2, x3)) = 2·x3   
POL(U93(x1, x2, x3)) = 2·x3   
POL(U94(x1, x2, x3)) = 2·x3   
POL(U95(x1, x2)) = 2·x2   
POL(U96(x1)) = x1   
POL(cons(x1, x2)) = 2·x2   
POL(isNat(x1)) = 2·x1   
POL(isNatIList(x1)) = 2   
POL(isNatIListKind(x1)) = 2   
POL(isNatKind(x1)) = 2   
POL(isNatList(x1)) = 2·x1   
POL(length(x1)) = x1   
POL(nil) = 2   
POL(s(x1)) = 2·x1   
POL(take(x1, x2)) = x1 + x2   
POL(tt) = 2   
POL(zeros) = 0   

the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
length(nil) → 0
length(cons(N, L)) → U111(isNatList(L), L, N)
U111(tt, L, N) → U112(isNatIListKind(L), L, N)
U112(tt, L, N) → U113(isNat(N), L, N)
U113(tt, L, N) → U114(isNatKind(N), L)
U114(tt, L) → s(length(L))
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
U71(tt) → tt
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
zeros → cons(0, zeros)
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
take(0, IL) → U121(isNatIList(IL), IL)
take(s(M), cons(N, IL)) → U131(isNatIList(IL), IL, M, N)
U121(tt, IL) → U122(isNatIListKind(IL))
U122(tt) → nil
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U131(tt, IL, M, N) → U132(isNatIListKind(IL), IL, M, N)
U132(tt, IL, M, N) → U133(isNat(M), IL, M, N)
U133(tt, IL, M, N) → U134(isNatKind(M), IL, M, N)
U134(tt, IL, M, N) → U135(isNat(N), IL, M, N)
U135(tt, IL, M, N) → U136(isNatKind(N), IL, M, N)
U136(tt, IL, M, N) → cons(N, take(M, IL))
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U81(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt

could all be oriented weakly.
Furthermore, the pairs

LENGTH(cons(N, L)) → U1111(isNatList(L), L, N)
U1111(tt, L, N) → U1121(isNatIListKind(L), L, N)

could be oriented strictly and thus removed.
The pairs

U1121(tt, L, N) → U1131(isNat(N), L, N)
U1131(tt, L, N) → U1141(isNatKind(N), L)
U1141(tt, L) → LENGTH(L)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPReductionPairProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, s, length, U13, U122, take, U23, U33, U46, U52, U62, U71, U81, U96, LENGTH} are replacing on all positions.
For all symbols f in {cons, U101, U102, U103, U104, U105, U11, U12, U111, U112, U113, U114, U121, U131, U132, U133, U134, U135, U136, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U61, U91, U92, U93, U94, U95, U1131, U1121, U1141} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, isNat, isNatIList, isNatList} are not replacing on any position.

The TRS P consists of the following rules:

U1121(tt, L, N) → U1131(isNat(N), L, N)
U1131(tt, L, N) → U1141(isNatKind(N), L)
U1141(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U101(tt, V1, V2) → U102(isNatKind(V1), V1, V2)
U102(tt, V1, V2) → U103(isNatIListKind(V2), V1, V2)
U103(tt, V1, V2) → U104(isNatIListKind(V2), V1, V2)
U104(tt, V1, V2) → U105(isNat(V1), V2)
U105(tt, V2) → U106(isNatIList(V2))
U106(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U111(tt, L, N) → U112(isNatIListKind(L), L, N)
U112(tt, L, N) → U113(isNat(N), L, N)
U113(tt, L, N) → U114(isNatKind(N), L)
U114(tt, L) → s(length(L))
U12(tt, V1) → U13(isNatList(V1))
U121(tt, IL) → U122(isNatIListKind(IL))
U122(tt) → nil
U13(tt) → tt
U131(tt, IL, M, N) → U132(isNatIListKind(IL), IL, M, N)
U132(tt, IL, M, N) → U133(isNat(M), IL, M, N)
U133(tt, IL, M, N) → U134(isNatKind(M), IL, M, N)
U134(tt, IL, M, N) → U135(isNat(N), IL, M, N)
U135(tt, IL, M, N) → U136(isNatKind(N), IL, M, N)
U136(tt, IL, M, N) → cons(N, take(M, IL))
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIListKind(V2))
U62(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt, V1, V2) → U92(isNatKind(V1), V1, V2)
U92(tt, V1, V2) → U93(isNatIListKind(V2), V1, V2)
U93(tt, V1, V2) → U94(isNatIListKind(V2), V1, V2)
U94(tt, V1, V2) → U95(isNat(V1), V2)
U95(tt, V2) → U96(isNatList(V2))
U96(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatIListKind(take(V1, V2)) → U61(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U71(isNatIListKind(V1))
isNatKind(s(V1)) → U81(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U91(isNatKind(V1), V1, V2)
isNatList(take(V1, V2)) → U101(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U111(isNatList(L), L, N)
take(0, IL) → U121(isNatIList(IL), IL)
take(s(M), cons(N, IL)) → U131(isNatIList(IL), IL, M, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 3 less nodes.