Termination of the following Term Rewriting System could be proven:

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

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

The replacement map contains the following entries:

and: {1, 2}
tt: empty set
isNatIList: empty set
isNatList: empty set
isNat: empty set
0: empty set
s: {1}
length: {1}
zeros: empty set
cons: {1}
nil: empty set
take: {1, 2}
uTake1: {1}
uTake2: {1}
uLength: {1}


↳ CSR
  ↳ CSDependencyPairsProof

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

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

The replacement map contains the following entries:

and: {1, 2}
tt: empty set
isNatIList: empty set
isNatList: empty set
isNat: empty set
0: empty set
s: {1}
length: {1}
zeros: empty set
cons: {1}
nil: empty set
take: {1, 2}
uTake1: {1}
uTake2: {1}
uLength: {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 {and, s, length, take, uTake1, AND, UTAKE1, TAKE, LENGTH} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength, UTAKE2, ULENGTH} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATLIST, ISNATILIST, ISNAT, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

ISNATILIST(IL) → ISNATLIST(IL)
ISNAT(s(N)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
ISNATILIST(cons(N, IL)) → AND(isNat(N), isNatIList(IL))
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)
ISNATLIST(cons(N, L)) → AND(isNat(N), isNatList(L))
ISNATLIST(cons(N, L)) → ISNAT(N)
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ISNATLIST(take(N, IL)) → AND(isNat(N), isNatIList(IL))
ISNATLIST(take(N, IL)) → ISNAT(N)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
TAKE(0, IL) → UTAKE1(isNatIList(IL))
TAKE(0, IL) → ISNATILIST(IL)
TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
TAKE(s(M), cons(N, IL)) → AND(isNat(M), and(isNat(N), isNatIList(IL)))
TAKE(s(M), cons(N, IL)) → ISNAT(M)
TAKE(s(M), cons(N, IL)) → AND(isNat(N), isNatIList(IL))
TAKE(s(M), cons(N, IL)) → ISNAT(N)
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(L)), L)
LENGTH(cons(N, L)) → AND(isNat(N), isNatList(L))
LENGTH(cons(N, L)) → ISNAT(N)
LENGTH(cons(N, L)) → ISNATLIST(L)
ULENGTH(tt, L) → LENGTH(L)

The collapsing dependency pairs are DPc:

UTAKE2(tt, M, N, IL) → N
ULENGTH(tt, L) → L


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 :

UTAKE2(tt, M, N, IL) → U(N)
ULENGTH(tt, L) → U(L)
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:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

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


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {and, s, length, take, uTake1} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNAT, ISNATLIST, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(N, L)) → ISNAT(N)
ISNAT(s(N)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ISNATLIST(take(N, IL)) → ISNAT(N)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
ISNATILIST(IL) → ISNATLIST(IL)
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

The following rules are not useable and can be deleted:

and(tt, x0) → x0
isNatIList(x0) → isNatList(x0)
isNat(0) → tt
isNat(s(x0)) → isNat(x0)
isNat(length(x0)) → isNatList(x0)
isNatIList(zeros) → tt
isNatIList(cons(x0, x1)) → and(isNat(x0), isNatIList(x1))
isNatList(nil) → tt
isNatList(cons(x0, x1)) → and(isNat(x0), isNatList(x1))
isNatList(take(x0, x1)) → and(isNat(x0), isNatIList(x1))
zeros → cons(0, zeros)
take(0, x0) → uTake1(isNatIList(x0))
uTake1(tt) → nil
take(s(x0), cons(x1, x2)) → uTake2(and(isNat(x0), and(isNat(x1), isNatIList(x2))), x0, x1, x2)
uTake2(tt, x0, x1, x2) → cons(x1, take(x0, x2))
length(cons(x0, x1)) → uLength(and(isNat(x0), isNatList(x1)), x1)
uLength(tt, x0) → s(length(x0))


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, take} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {ISNAT, ISNATLIST, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(N, L)) → ISNAT(N)
ISNAT(s(N)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ISNATLIST(take(N, IL)) → ISNAT(N)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
ISNATILIST(IL) → ISNATLIST(IL)
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)

R is empty.
Q is empty.

Using the order
Polynomial interpretation [25]:

POL(ISNAT(x1)) = x1   
POL(ISNATILIST(x1)) = 1 + 2·x1   
POL(ISNATLIST(x1)) = 2·x1   
POL(cons(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(length(x1)) = 2 + 2·x1   
POL(s(x1)) = 2 + 2·x1   
POL(take(x1, x2)) = 1 + x1 + 2·x2   

the following usable rules
none

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

ISNATLIST(cons(N, L)) → ISNAT(N)
ISNAT(s(N)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ISNATLIST(take(N, IL)) → ISNAT(N)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
ISNATILIST(IL) → ISNATLIST(IL)
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)

could be oriented strictly and thus removed.
All pairs have been removed.


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

Q-restricted context-sensitive dependency pair problem:

The TRS P consists of the following rules:
none

R is empty.
Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

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

Q-restricted context-sensitive dependency pair problem:
The symbols in {and, s, length, take, uTake1, TAKE} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength, UTAKE2} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, U} are not replacing on any position.

The TRS P consists of the following rules:

TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
UTAKE2(tt, M, N, IL) → 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)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
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)
The remaining pairs can at least be oriented weakly.

UTAKE2(tt, M, N, IL) → U(N)
Used ordering: Combined order from the following AFS and order.
UTAKE2(x1, x2, x3, x4)  =  x3
TAKE(x1, x2)  =  x2
U(x1)  =  x1

Subterm Order


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {and, s, length, take, uTake1} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength, UTAKE2} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, U} are not replacing on any position.

The TRS P consists of the following rules:

UTAKE2(tt, M, N, IL) → U(N)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

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


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {and, s, length, take, uTake1, LENGTH} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength, ULENGTH} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

ULENGTH(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(L)), L)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

Using the order
Matrix interpretation [3]:
Non-tuple symbols:
M( and(x1, x2) ) =
/0\
\0/
+
/00\
\00/
·x1+
/10\
\01/
·x2

M( take(x1, x2) ) =
/0\
\1/
+
/01\
\00/
·x1+
/10\
\01/
·x2

M( 0 ) =
/1\
\0/

M( cons(x1, x2) ) =
/0\
\0/
+
/00\
\00/
·x1+
/11\
\01/
·x2

M( uTake2(x1, ..., x4) ) =
/1\
\1/
+
/00\
\00/
·x1+
/01\
\00/
·x2+
/00\
\00/
·x3+
/11\
\01/
·x4

M( tt ) =
/1\
\0/

M( isNatList(x1) ) =
/0\
\0/
+
/01\
\00/
·x1

M( zeros ) =
/0\
\0/

M( isNatIList(x1) ) =
/1\
\0/
+
/01\
\00/
·x1

M( uTake1(x1) ) =
/0\
\1/
+
/00\
\00/
·x1

M( s(x1) ) =
/0\
\1/
+
/10\
\01/
·x1

M( isNat(x1) ) =
/0\
\0/
+
/10\
\00/
·x1

M( length(x1) ) =
/0\
\0/
+
/01\
\11/
·x1

M( nil ) =
/0\
\1/

M( uLength(x1, x2) ) =
/0\
\0/
+
/00\
\10/
·x1+
/01\
\11/
·x2

Tuple symbols:
M( LENGTH(x1) ) = 1+
[1,1]
·x1

M( ULENGTH(x1, x2) ) = 0+
[1,0]
·x1+
[1,1]
·x2


Matrix type:
We used a basic matrix type which is not further parametrizeable.


the following usable rules

and(tt, T) → T
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
take(0, IL) → uTake1(isNatIList(IL))
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake1(tt) → nil
isNatIList(IL) → isNatList(IL)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))

could all be oriented weakly.
Furthermore, the pairs

LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(L)), L)

could be oriented strictly and thus removed.
The pairs

ULENGTH(tt, L) → LENGTH(L)

could only be oriented weakly and must be analyzed further.


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {and, s, length, take, uTake1, LENGTH} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength, ULENGTH} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

ULENGTH(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

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